This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 → ⟨ 𝐺 , 𝑆 ⟩ ∈ CVec_OLD )
2		vcex	⊢ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVec_OLD → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )
3	1 2	syl	⊢ ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )
4		nvss	⊢ NrmCVec ⊆ ( CVec_OLD × V )
5	4	sseli	⊢ ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec → ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ ( CVec_OLD × V ) )
6		opelxp2	⊢ ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ ( CVec_OLD × 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 ) )