English
If ||v|| = ||w||, then reflecting v across the orthogonal complement of span(v − w) maps v to w.
Русский
Если ||v|| = ||w||, то отражение v через (span(v−w))⊥ отправляет v в w.
LaTeX
$$$\|v\| = \|w\| \implies R_{(\mathbb{R}\cdot (v-w))^{\perp}}(v) = w$$$
Lean4
theorem reflection_sub {v w : F} (h : ‖v‖ = ‖w‖) : reflection (ℝ ∙ (v - w))ᗮ v = w :=
by
set R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ v - w)ᗮ
suffices R v + R v = w + w by
apply smul_right_injective F (by simp : (2 : ℝ) ≠ 0)
simpa [two_smul] using this
have h₁ : R (v - w) = -(v - w) := reflection_orthogonalComplement_singleton_eq_neg (v - w)
have h₂ : R (v + w) = v + w := by
apply reflection_mem_subspace_eq_self
rw [Submodule.mem_orthogonal_singleton_iff_inner_left]
rw [real_inner_add_sub_eq_zero_iff]
exact h
convert congr_arg₂ (· + ·) h₂ h₁ using 1
· simp
· abel
