𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type ?u.201826
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
f✝ : E →ₛₗ[σ] F
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖↑f x‖ = a * ‖x‖
y : F
⊢ ‖↑(LinearEquiv.symm f) y‖ = a⁻¹ * ‖y‖
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type ?u.201826
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
f✝ : E →ₛₗ[σ] F
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
⊢ (∀ (x : E), ‖↑f x‖ = a * ‖x‖) → ∀ (y : F), ‖↑(LinearEquiv.symm f) y‖ = a⁻¹ * ‖y‖
intro hf y
no goals
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type ?u.201826
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
f✝ : E →ₛₗ[σ] F
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖↑f x‖ = a * ‖x‖
y : F
⊢ ‖↑(LinearEquiv.symm f) y‖ = a⁻¹ * ‖y‖
calc
  ‖f.symm y‖ = a⁻¹ * (a * ‖f.symm y‖) := by
    rw [← mul_assoc, inv_mul_cancel (ne_of_lt ha).symm, one_mul]
  _ = a⁻¹ * ‖f (f.symm y)‖ := by rw [hf]
  _ = a⁻¹ * ‖y‖ := by simp
no goals
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type ?u.201826
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
f✝ : E →ₛₗ[σ] F
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖↑f x‖ = a * ‖x‖
y : F
⊢ ‖↑(LinearEquiv.symm f) y‖ = a⁻¹ * (a * ‖↑(LinearEquiv.symm f) y‖)
rw [← mul_assoc, inv_mul_cancel (ne_of_lt ha).symm, one_mul]
no goals
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type ?u.201826
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
f✝ : E →ₛₗ[σ] F
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖↑f x‖ = a * ‖x‖
y : F
⊢ a⁻¹ * (a * ‖↑(LinearEquiv.symm f) y‖) = a⁻¹ * ‖↑f (↑(LinearEquiv.symm f) y)‖
rw [hf]
no goals
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type ?u.201826
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedSpace 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
f✝ : E →ₛₗ[σ] F
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖↑f x‖ = a * ‖x‖
y : F
⊢ a⁻¹ * ‖↑f (↑(LinearEquiv.symm f) y)‖ = a⁻¹ * ‖y‖
simp