𝕜 : Type u_2
𝕜₂ : Type ?u.3824025
𝕜₃ : Type ?u.3824028
E : Type u_1
Eₗ : Type ?u.3824034
F : Type ?u.3824037
Fₗ : Type ?u.3824040
G : Type ?u.3824043
Gₗ : Type ?u.3824046
𝓕 : Type ?u.3824049
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 σ₂₁
x : E
h : x ≠ 0
hx : 0 < ‖x‖
⊢ ‖coord 𝕜 x h‖ = ‖x‖⁻¹
𝕜 : Type u_2
𝕜₂ : Type ?u.3824025
𝕜₃ : Type ?u.3824028
E : Type u_1
Eₗ : Type ?u.3824034
F : Type ?u.3824037
Fₗ : Type ?u.3824040
G : Type ?u.3824043
Gₗ : Type ?u.3824046
𝓕 : Type ?u.3824049
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 σ₂₁
x : E
h : x ≠ 0
⊢ ‖coord 𝕜 x h‖ = ‖x‖⁻¹
have hx : 0 < ‖x‖ := norm_pos_iff.mpr h
𝕜 : Type u_2
𝕜₂ : Type ?u.3824025
𝕜₃ : Type ?u.3824028
E : Type u_1
Eₗ : Type ?u.3824034
F : Type ?u.3824037
Fₗ : Type ?u.3824040
G : Type ?u.3824043
Gₗ : Type ?u.3824046
𝓕 : Type ?u.3824049
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 σ₂₁
x : E
h : x ≠ 0
hx : 0 < ‖x‖
this : Nontrivial { x_1 // x_1 ∈ Submodule.span 𝕜 {x} }
⊢ ‖coord 𝕜 x h‖ = ‖x‖⁻¹
𝕜 : Type u_2
𝕜₂ : Type ?u.3824025
𝕜₃ : Type ?u.3824028
E : Type u_1
Eₗ : Type ?u.3824034
F : Type ?u.3824037
Fₗ : Type ?u.3824040
G : Type ?u.3824043
Gₗ : Type ?u.3824046
𝓕 : Type ?u.3824049
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 σ₂₁
x : E
h : x ≠ 0
hx : 0 < ‖x‖
⊢ ‖coord 𝕜 x h‖ = ‖x‖⁻¹
haveI : Nontrivial (𝕜 ∙ x) := Submodule.nontrivial_span_singleton h
no goals
𝕜 : Type u_2
𝕜₂ : Type ?u.3824025
𝕜₃ : Type ?u.3824028
E : Type u_1
Eₗ : Type ?u.3824034
F : Type ?u.3824037
Fₗ : Type ?u.3824040
G : Type ?u.3824043
Gₗ : Type ?u.3824046
𝓕 : Type ?u.3824049
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 σ₂₁
x : E
h : x ≠ 0
hx : 0 < ‖x‖
this : Nontrivial { x_1 // x_1 ∈ Submodule.span 𝕜 {x} }
⊢ ‖coord 𝕜 x h‖ = ‖x‖⁻¹
exact ContinuousLinearMap.homothety_norm _ fun y =>
  homothety_inverse _ hx _ (toSpanNonzeroSingleton_homothety 𝕜 x h) _