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 ) )