English
Applying secondInter twice with the same direction recovers the original point on the line.
Русский
Повторное применение secondInter дважды вдоль той же вектора возвращает исходную точку на прямой.
LaTeX
$$$s.secondInter(s.secondInter(p,v),v) = p$$$
Lean4
/-- The point given by `secondInter` equals the original point if and only if the line is
orthogonal to the radius vector. -/
theorem secondInter_eq_self_iff {s : Sphere P} {p : P} {v : V} : s.secondInter p v = p ↔ ⟪v, p -ᵥ s.center⟫ = 0 :=
by
refine ⟨fun hp => ?_, fun hp => ?_⟩
· by_cases hv : v = 0
· simp [hv]
rwa [Sphere.secondInter, eq_comm, eq_vadd_iff_vsub_eq, vsub_self, eq_comm, smul_eq_zero, or_iff_left hv,
div_eq_zero_iff, inner_self_eq_zero, or_iff_left hv, mul_eq_zero, or_iff_right (by simp : (-2 : ℝ) ≠ 0)] at hp
· rw [Sphere.secondInter, hp, mul_zero, zero_div, zero_smul, zero_vadd]
