Normed affine spaces over an inner product space

theorem inner_vsub_left_eq_zero_symm {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [MetricSpace P] [NormedAddTorsor V P] {a b : P} {v : V} : inner 𝕜 (a -ᵥ b) v = 0 ↔ inner 𝕜 (b -ᵥ a) v = 0

theorem inner_vsub_right_eq_zero_symm {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [RCLike 𝕜] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [MetricSpace P] [NormedAddTorsor V P] {v : V} {a b : P} : inner 𝕜 v (a -ᵥ b) = 0 ↔ inner 𝕜 v (b -ᵥ a) = 0

In this section, the first left/right indicates where the common argument to vsub is, and the section refers to the argument of inner that ends up in the dist.

The lemma shapes are such that the relevant argument of inner remains unchanged, and that the other vsub preserves the position of the unchanging argument.

theorem inner_vsub_vsub_left_eq_dist_sq_left_iff {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c : P} : inner ℝ (a -ᵥ b) (a -ᵥ c) = dist a b ^ 2 ↔ inner ℝ (a -ᵥ b) (b -ᵥ c) = 0

theorem inner_vsub_vsub_left_eq_dist_sq_right_iff {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c : P} : inner ℝ (a -ᵥ b) (a -ᵥ c) = dist a c ^ 2 ↔ inner ℝ (c -ᵥ b) (a -ᵥ c) = 0

theorem inner_vsub_vsub_right_eq_dist_sq_left_iff {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c : P} : inner ℝ (a -ᵥ c) (b -ᵥ c) = dist a c ^ 2 ↔ inner ℝ (a -ᵥ c) (b -ᵥ a) = 0

theorem inner_vsub_vsub_right_eq_dist_sq_right_iff {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c : P} : inner ℝ (a -ᵥ c) (b -ᵥ c) = dist b c ^ 2 ↔ inner ℝ (a -ᵥ b) (b -ᵥ c) = 0