𝕜 : Type u_2
𝕜₂ : Type ?u.418441
𝕜₃ : Type ?u.418444
E : Type u_1
Eₗ : Type ?u.418450
F : Type ?u.418453
Fₗ : Type ?u.418456
G : Type ?u.418459
Gₗ : Type ?u.418462
𝓕 : Type ?u.418465
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h✝ : F →SL[σ₂₃] G
x✝ : E
h : ∃ x, ‖x‖ ≠ 0
x : E
hx : ‖x‖ ≠ 0
⊢ 1 ≤ ‖id 𝕜 E‖
𝕜 : Type u_2
𝕜₂ : Type ?u.418441
𝕜₃ : Type ?u.418444
E : Type u_1
Eₗ : Type ?u.418450
F : Type ?u.418453
Fₗ : Type ?u.418456
G : Type ?u.418459
Gₗ : Type ?u.418462
𝓕 : Type ?u.418465
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h✝ : F →SL[σ₂₃] G
x : E
h : ∃ x, ‖x‖ ≠ 0
⊢ 1 ≤ ‖id 𝕜 E‖
let ⟨x, hx⟩ := h
𝕜 : Type u_2
𝕜₂ : Type ?u.418441
𝕜₃ : Type ?u.418444
E : Type u_1
Eₗ : Type ?u.418450
F : Type ?u.418453
Fₗ : Type ?u.418456
G : Type ?u.418459
Gₗ : Type ?u.418462
𝓕 : Type ?u.418465
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h✝ : F →SL[σ₂₃] G
x✝ : E
h : ∃ x, ‖x‖ ≠ 0
x : E
hx : ‖x‖ ≠ 0
this : ‖↑(id 𝕜 E) x‖ / ‖x‖ ≤ ‖id 𝕜 E‖
⊢ 1 ≤ ‖id 𝕜 E‖
𝕜 : Type u_2
𝕜₂ : Type ?u.418441
𝕜₃ : Type ?u.418444
E : Type u_1
Eₗ : Type ?u.418450
F : Type ?u.418453
Fₗ : Type ?u.418456
G : Type ?u.418459
Gₗ : Type ?u.418462
𝓕 : Type ?u.418465
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h✝ : F →SL[σ₂₃] G
x✝ : E
h : ∃ x, ‖x‖ ≠ 0
x : E
hx : ‖x‖ ≠ 0
⊢ 1 ≤ ‖id 𝕜 E‖
have := (id 𝕜 E).ratio_le_op_norm x
no goals
𝕜 : Type u_2
𝕜₂ : Type ?u.418441
𝕜₃ : Type ?u.418444
E : Type u_1
Eₗ : Type ?u.418450
F : Type ?u.418453
Fₗ : Type ?u.418456
G : Type ?u.418459
Gₗ : Type ?u.418462
𝓕 : Type ?u.418465
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h✝ : F →SL[σ₂₃] G
x✝ : E
h : ∃ x, ‖x‖ ≠ 0
x : E
hx : ‖x‖ ≠ 0
this : ‖↑(id 𝕜 E) x‖ / ‖x‖ ≤ ‖id 𝕜 E‖
⊢ 1 ≤ ‖id 𝕜 E‖
rwa [id_apply, div_self hx] at this