English
The inner product identity relating a vertex, another vertex, and the altitude foot yields height squared: ⟪p_i-p_j, p_i-foot_i⟫ = height_i^2.
Русский
Внутреннее произведение между векторами p_i−p_j и p_i−foot_i равно квадратнои высоте: ⟪p_i−p_j, p_i−foot_i⟫ = height_i^2.
LaTeX
$$$\\langle s.\\text{points}(i)-s.\\text{points}(j),\\, s.\\text{points}(i)-s.\\text{altitudeFoot}(i)\\rangle = (s.\\text{height}(i))^2$$$
Lean4
/-- The inner product of an edge from `j` to `i` and the vector from the foot of `i` to `i`
is the square of the height. -/
theorem inner_vsub_vsub_altitudeFoot_eq_height_sq [NeZero n] {i j : Fin (n + 1)} (h : i ≠ j) :
⟪s.points i -ᵥ s.points j, s.points i -ᵥ s.altitudeFoot i⟫ = s.height i ^ 2 :=
by
suffices ⟪s.points j -ᵥ s.altitudeFoot i, s.points i -ᵥ s.altitudeFoot i⟫ = 0 by
rwa [height, inner_vsub_vsub_left_eq_dist_sq_right_iff, inner_vsub_left_eq_zero_symm]
refine
Submodule.inner_right_of_mem_orthogonal (K := vectorSpan ℝ (s.points '' { i }ᶜ))
(vsub_mem_vectorSpan_of_mem_affineSpan_of_mem_affineSpan (s.mem_affineSpan_image_iff.2 h.symm)
(altitudeFoot_mem_affineSpan_image_compl _ _))
?_
rw [← direction_affineSpan, ← range_faceOpposite_points]
exact vsub_orthogonalProjection_mem_direction_orthogonal _ _
