Metamath Proof Explorer


Theorem nvex

Description: The components of a normed complex vector space are sets. (Contributed by NM, 5-Jun-2008) (Revised by Mario Carneiro, 1-May-2015) (New usage is discouraged.)

Ref Expression
Assertion nvex ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V ) )

Proof

Step Hyp Ref Expression
1 nvvcop ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec → ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD )
2 vcex ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )
3 1 2 syl ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )
4 nvss NrmCVec ⊆ ( CVecOLD × V )
5 4 sseli ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec → ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ ( CVecOLD × V ) )
6 opelxp2 ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ ( CVecOLD × V ) → 𝑁 ∈ V )
7 5 6 syl ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec → 𝑁 ∈ V )
8 df-3an ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V ) ↔ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) ∧ 𝑁 ∈ V ) )
9 3 7 8 sylanbrc ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V ) )