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	$⊢ ⟨⟨G, S⟩, N⟩ \in NrmCVec \to (G \in V \land S \in V \land N \in V)$

Proof

Step	Hyp	Ref	Expression
1		nvvcop	$⊢ ⟨⟨G, S⟩, N⟩ \in NrmCVec \to ⟨G, S⟩ \in {CVec}_{OLD}$
2		vcex	$⊢ ⟨G, S⟩ \in {CVec}_{OLD} \to (G \in V \land S \in V)$
3	1 2	syl	$⊢ ⟨⟨G, S⟩, N⟩ \in NrmCVec \to (G \in V \land S \in V)$
4		nvss	$⊢ NrmCVec \subseteq {CVec}_{OLD} \times V$
5	4	sseli	$⊢ ⟨⟨G, S⟩, N⟩ \in NrmCVec \to ⟨⟨G, S⟩, N⟩ \in ({CVec}_{OLD} \times V)$
6		opelxp2	$⊢ ⟨⟨G, S⟩, N⟩ \in ({CVec}_{OLD} \times V) \to N \in V$
7	5 6	syl	$⊢ ⟨⟨G, S⟩, N⟩ \in NrmCVec \to N \in V$
8		df-3an	$⊢ (G \in V \land S \in V \land N \in V) \leftrightarrow ((G \in V \land S \in V) \land N \in V)$
9	3 7 8	sylanbrc	$⊢ ⟨⟨G, S⟩, N⟩ \in NrmCVec \to (G \in V \land S \in V \land N \in V)$