English
For any nonzero v, the distance after scaling and translating by rv from p1 to p2 equals the distance between p1 and p2 if and only if r = 0 or r = −2 ⟪v, p1 − p2⟫ / ⟪v,v⟫.
Русский
Для ненулевого v расстояние после масштабирования и переноса по rv от p1 к p2 равно расстоянию между p1 и p2 тогда и только тогда, когда r = 0 или r = −2⟨v, p1−p2⟩/⟨v,v⟩.
LaTeX
$$$ dist(r v + p_1, p_2) = dist(p_1, p_2) \;\Leftrightarrow\; r = 0 \ \text{или}\ \ r = -2 \frac{\langle v, p_1 - p_2\rangle}{\langle v,v\rangle} $$$
Lean4
/-- The condition for two points on a line to be equidistant from
another point. -/
theorem dist_smul_vadd_eq_dist {v : V} (p₁ p₂ : P) (hv : v ≠ 0) (r : ℝ) :
dist (r • v +ᵥ p₁) p₂ = dist p₁ p₂ ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫ :=
by
conv_lhs =>
rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, dist_smul_vadd_sq, mul_assoc, ← sub_eq_zero, add_sub_assoc,
dist_eq_norm_vsub V p₁ p₂, ← real_inner_self_eq_norm_mul_norm, sub_self]
have hvi : ⟪v, v⟫ ≠ 0 := by simpa using hv
have hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫) :=
by
rw [discrim]
ring
rw [quadratic_eq_zero_iff hvi hd, neg_add_cancel, zero_div, neg_mul_eq_neg_mul, ← mul_sub_right_distrib,
sub_eq_add_neg, ← mul_two, mul_assoc, mul_div_assoc, mul_div_mul_left, mul_div_assoc]
simp
