no goals
α : Type ?u.29402
V : Type u_3
P : Type u_1
W : Type ?u.29411
Q : Type ?u.29414
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : P
c : 𝕜
⊢ dist (↑(lineMap p₁ p₂) c) p₁ = ‖c‖ * dist p₁ p₂
rw [← dist_zero_right, ← dist_lineMap_lineMap, lineMap_apply_zero]