English
If dist equality conditions hold, then y equals lineMap x z r.
Русский
Если условия равенства расстояний выполняются, то y равна lineMap x z r.
LaTeX
$$eq_lineMap_of_dist_eq_mul_of_dist_eq_mul$$
Lean4
theorem eq_lineMap_of_dist_eq_mul_of_dist_eq_mul (hxy : dist x y = r * dist x z) (hyz : dist y z = (1 - r) * dist x z) :
y = AffineMap.lineMap x z r :=
by
have : y -ᵥ x ∈ [(0 : E) -[ℝ] z -ᵥ x] := by
rw [mem_segment_iff_wbtw, ← dist_add_dist_eq_iff, dist_zero, dist_vsub_cancel_right, ← dist_eq_norm_vsub', ←
dist_eq_norm_vsub', hxy, hyz, ← add_mul, add_sub_cancel, one_mul]
obtain rfl | hne := eq_or_ne x z
· obtain rfl : y = x := by simpa
simp
· rw [← dist_ne_zero] at hne
obtain ⟨a, b, _, hb, _, H⟩ := this
rw [smul_zero, zero_add] at H
have H' := congr_arg norm H
rw [norm_smul, Real.norm_of_nonneg hb, ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy, mul_left_inj' hne] at H'
rw [AffineMap.lineMap_apply, ← H', H, vsub_vadd]
