α : Type ?u.5505
V : Type u_2
P : Type u_1
W : Type ?u.5514
Q : Type ?u.5517
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : P
c : 𝕜
⊢ ‖p₁ -ᵥ ↑(c • (AffineMap.id 𝕜 P -ᵥ const 𝕜 P p₁) +ᵥ const 𝕜 P p₁) p₂‖ = ‖c‖ * dist p₁ p₂
α : Type ?u.5505
V : Type u_2
P : Type u_1
W : Type ?u.5514
Q : Type ?u.5517
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : P
c : 𝕜
⊢ dist p₁ (↑(homothety p₁ c) p₂) = ‖c‖ * dist p₁ p₂
rw [homothety_def, dist_eq_norm_vsub V]
no goals
α : Type ?u.5505
V : Type u_2
P : Type u_1
W : Type ?u.5514
Q : Type ?u.5517
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
p₁ p₂ : P
c : 𝕜
⊢ ‖p₁ -ᵥ ↑(c • (AffineMap.id 𝕜 P -ᵥ const 𝕜 P p₁) +ᵥ const 𝕜 P p₁) p₂‖ = ‖c‖ * dist p₁ p₂
simp [norm_smul, ← dist_eq_norm_vsub V, dist_comm]