English
If a,b,c,d are cospherical and p lies on lines AB and CD, then AB and CD satisfy the chord power relation: dist(a,p)dist(b,p) = dist(c,p)dist(d,p).
Русский
Если a,b,c,d кососферны и точка p лежит на прямых AB и CD, то выполняется равенство мощности хорд: dist(a,p)dist(b,p)=dist(c,p)dist(d,p).
LaTeX
$$Cospherical({a,b,c,d}) ∧ p∈line(a,b) ∧ p∈line(c,d) ⇒ dist(a,p)dist(b,p)=dist(c,p)dist(d,p)$$
Lean4
/-- If `P` is a point on the line `AB` and `Q` is equidistant from `A` and `B`, then
`AP * BP = abs (BQ ^ 2 - PQ ^ 2)`. -/
theorem mul_dist_eq_abs_sub_sq_dist {a b p q : P} (hp : p ∈ line[ℝ, a, b]) (hq : dist a q = dist b q) :
dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2| :=
by
let m : P := midpoint ℝ a b
have h1 := vsub_sub_vsub_cancel_left a p m
have h1' := vsub_sub_vsub_cancel_left p a m
have h2 := vsub_sub_vsub_cancel_left p q m
have h3 := vsub_sub_vsub_cancel_left a q m
have h : ∀ r, b -ᵥ r = m -ᵥ r + (m -ᵥ a) := fun r => by
rw [midpoint_vsub_left, ← right_vsub_midpoint, add_comm, vsub_add_vsub_cancel]
iterate 4 rw [dist_eq_norm_vsub V]
rw [← h1, ← h2, h, h]
rw [dist_eq_norm_vsub V a q, dist_eq_norm_vsub V b q, ← h3, h] at hq
refine mul_norm_eq_abs_sub_sq_norm ?_ hq
· rw [← vsub_vadd p a, vadd_left_mem_affineSpan_pair] at hp
rcases hp with ⟨r, hr⟩
rw [h, ← h1', eq_sub_iff_add_eq, ← eq_sub_iff_add_eq'] at hr
rw [hr]
use 1 - r * 2
match_scalars
ring
