English
Distance between p1 and the reflection of p2 across s equals the distance between the reflection of p1 and p2.
Русский
Расстояние между p1 и отражением p2 через s равно расстоянию между отражением p1 и p2.
LaTeX
$$$$\operatorname{dist}(p_1, \mathrm{reflection}_s(p_2)) = \operatorname{dist}(\mathrm{reflection}_s(p_1), p_2).$$$$
Lean4
/-- Reflecting a point in two subspaces produces the same result if
and only if the point has the same orthogonal projection in each of
those subspaces. -/
theorem reflection_eq_iff_orthogonalProjection_eq (s₁ s₂ : AffineSubspace ℝ P) [Nonempty s₁] [Nonempty s₂]
[s₁.direction.HasOrthogonalProjection] [s₂.direction.HasOrthogonalProjection] (p : P) :
reflection s₁ p = reflection s₂ p ↔ (orthogonalProjection s₁ p : P) = orthogonalProjection s₂ p :=
by
rw [reflection_apply, reflection_apply]
constructor
· intro h
rw [← @vsub_eq_zero_iff_eq V, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_comm, add_sub_assoc,
vsub_sub_vsub_cancel_right, ← two_smul ℝ ((orthogonalProjection s₁ p : P) -ᵥ orthogonalProjection s₂ p),
smul_eq_zero] at h
norm_num at h
exact h
· intro h
rw [h]
