English
If the angle equality holds and the angle at x,y is not π, then the norms of x and y are equal.
Русский
Если равенство углов выполнено и угол x y не равен π, то нормы векторов x и y равны.
LaTeX
$$$\angle x (x-y) = \angle y (y-x) \land \angle x y \neq \pi \Rightarrow \|x\| = \|y\|$$$
Lean4
/-- **Converse of pons asinorum**, vector angle form. -/
theorem norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi {x y : V} (h : angle x (x - y) = angle y (y - x))
(hpi : angle x y ≠ π) : ‖x‖ = ‖y‖ :=
by
replace h :=
Real.arccos_injOn (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x (x - y)))
(abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one y (y - x))) h
by_cases hxy : x = y
· rw [hxy]
· rw [← norm_neg (y - x), neg_sub, mul_comm, mul_comm ‖y‖, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev, mul_inv_rev, ←
mul_assoc, ← mul_assoc] at h
replace h := mul_right_cancel₀ (inv_ne_zero fun hz => hxy (eq_of_sub_eq_zero (norm_eq_zero.1 hz))) h
rw [inner_sub_right, inner_sub_right, real_inner_comm x y, real_inner_self_eq_norm_mul_norm,
real_inner_self_eq_norm_mul_norm, mul_sub_right_distrib, mul_sub_right_distrib, mul_self_mul_inv,
mul_self_mul_inv, sub_eq_sub_iff_sub_eq_sub, ← mul_sub_left_distrib] at h
by_cases hx0 : x = 0
· rw [hx0, norm_zero, inner_zero_left, zero_mul, zero_sub, neg_eq_zero] at h
rw [hx0, norm_zero, h]
· by_cases hy0 : y = 0
· rw [hy0, norm_zero, inner_zero_right, zero_mul, sub_zero] at h
rw [hy0, norm_zero, h]
· rw [inv_sub_inv (fun hz => hx0 (norm_eq_zero.1 hz)) fun hz => hy0 (norm_eq_zero.1 hz), ← neg_sub, ←
mul_div_assoc, mul_comm, mul_div_assoc, ← mul_neg_one] at h
symm
by_contra hyx
replace h := (mul_left_cancel₀ (sub_ne_zero_of_ne hyx) h).symm
rw [real_inner_div_norm_mul_norm_eq_neg_one_iff, ← angle_eq_pi_iff] at h
exact hpi h
