[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ ‖↑f x‖ ≤ ‖↑f 1‖ * ‖x‖
[PROOFSTEP]
conv_lhs => rw [← mul_one x]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
| ‖↑f x‖
[PROOFSTEP]
rw [← mul_one x]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
| ‖↑f x‖
[PROOFSTEP]
rw [← mul_one x]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
| ‖↑f x‖
[PROOFSTEP]
rw [← mul_one x]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ ‖↑f (x * 1)‖ ≤ ‖↑f 1‖ * ‖x‖
[PROOFSTEP]
rw [← smul_eq_mul, f.map_smul, mul_comm]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ ‖x • ↑f 1‖ ≤ ‖x‖ * ‖↑f 1‖
[PROOFSTEP]
exact norm_smul_le _ _
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ 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‖
[PROOFSTEP]
intro hf y
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ 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‖
[PROOFSTEP]
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
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ 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‖)
[PROOFSTEP]
rw [← mul_assoc, inv_mul_cancel (ne_of_lt ha).symm, one_mul]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ 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)‖
[PROOFSTEP]
rw [hf]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ 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‖
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
x : E
c : 𝕜
⊢ ‖↑(LinearMap.toSpanSingleton 𝕜 E x) c‖ = ‖x‖ * ‖c‖
[PROOFSTEP]
rw [mul_comm]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
x : E
c : 𝕜
⊢ ‖↑(LinearMap.toSpanSingleton 𝕜 E x) c‖ = ‖c‖ * ‖x‖
[PROOFSTEP]
exact norm_smul _ _
