𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.3787210
E : Type u_3
Eₗ : Type ?u.3787216
F : Type u_4
Fₗ : Type ?u.3787222
G : Type ?u.3787225
Gₗ : Type ?u.3787228
𝓕 : Type ?u.3787231
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
inst✝⁷ : NontriviallyNormedField 𝕜₃
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝³ : RingHomInvPair σ₂₁ σ₁₂
inst✝² : RingHomIsometric σ₂₁
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 1 ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖↑e‖
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.3787210
E : Type u_3
Eₗ : Type ?u.3787216
F : Type u_4
Fₗ : Type ?u.3787222
G : Type ?u.3787225
Gₗ : Type ?u.3787228
𝓕 : Type ?u.3787231
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
inst✝⁷ : NontriviallyNormedField 𝕜₃
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝³ : RingHomInvPair σ₂₁ σ₁₂
inst✝² : RingHomIsometric σ₂₁
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 1 ≤ ‖↑e‖ * ‖↑(ContinuousLinearEquiv.symm e)‖
rw [mul_comm]
case h.e'_3
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.3787210
E : Type u_3
Eₗ : Type ?u.3787216
F : Type u_4
Fₗ : Type ?u.3787222
G : Type ?u.3787225
Gₗ : Type ?u.3787228
𝓕 : Type ?u.3787231
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
inst✝⁷ : NontriviallyNormedField 𝕜₃
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝³ : RingHomInvPair σ₂₁ σ₁₂
inst✝² : RingHomIsometric σ₂₁
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 1 = ‖comp ↑(ContinuousLinearEquiv.symm e) ↑e‖
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.3787210
E : Type u_3
Eₗ : Type ?u.3787216
F : Type u_4
Fₗ : Type ?u.3787222
G : Type ?u.3787225
Gₗ : Type ?u.3787228
𝓕 : Type ?u.3787231
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
inst✝⁷ : NontriviallyNormedField 𝕜₃
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝³ : RingHomInvPair σ₂₁ σ₁₂
inst✝² : RingHomIsometric σ₂₁
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 1 ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖↑e‖
convert(e.symm : F →SL[σ₂₁] E).op_norm_comp_le (e : E →SL[σ₁₂] F)
no goals
case h.e'_3
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.3787210
E : Type u_3
Eₗ : Type ?u.3787216
F : Type u_4
Fₗ : Type ?u.3787222
G : Type ?u.3787225
Gₗ : Type ?u.3787228
𝓕 : Type ?u.3787231
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
inst✝⁷ : NontriviallyNormedField 𝕜₃
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝⁴ : RingHomInvPair σ₁₂ σ₂₁
inst✝³ : RingHomInvPair σ₂₁ σ₁₂
inst✝² : RingHomIsometric σ₂₁
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : Nontrivial E
e : E ≃SL[σ₁₂] F
⊢ 1 = ‖comp ↑(ContinuousLinearEquiv.symm e) ↑e‖
rw [e.coe_symm_comp_coe, ContinuousLinearMap.norm_id]