α : Type ?u.17388
V : Type u_3
P : Type u_1
W : Type ?u.17397
Q : Type ?u.17400
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₁ c₂ : 𝕜
⊢ dist (↑(lineMap p₁ p₂) c₁) (↑(lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₂ p₁
α : Type ?u.17388
V : Type u_3
P : Type u_1
W : Type ?u.17397
Q : Type ?u.17400
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₁ c₂ : 𝕜
⊢ dist (↑(lineMap p₁ p₂) c₁) (↑(lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₁ p₂
rw [dist_comm p₁ p₂]
no goals
α : Type ?u.17388
V : Type u_3
P : Type u_1
W : Type ?u.17397
Q : Type ?u.17400
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₁ c₂ : 𝕜
⊢ dist (↑(lineMap p₁ p₂) c₁) (↑(lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₂ p₁
rw [lineMap_apply, lineMap_apply, dist_eq_norm_vsub V, vadd_vsub_vadd_cancel_right,
  ← sub_smul, norm_smul, ← vsub_eq_sub, ← dist_eq_norm_vsub V, ← dist_eq_norm_vsub 𝕜]