Theorem nvvcop

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

	Ref	Expression
Assertion	nvvcop	⊢ ( ⟨ 𝑊 , 𝑁 ⟩ ∈ NrmCVec → 𝑊 ∈ CVecOLD )

Proof

Step	Hyp	Ref	Expression
1		nvss	⊢ NrmCVec ⊆ ( CVecOLD × V )
2	1	sseli	⊢ ( ⟨ 𝑊 , 𝑁 ⟩ ∈ NrmCVec → ⟨ 𝑊 , 𝑁 ⟩ ∈ ( CVecOLD × V ) )
3		opelxp1	⊢ ( ⟨ 𝑊 , 𝑁 ⟩ ∈ ( CVecOLD × V ) → 𝑊 ∈ CVecOLD )
4	2 3	syl	⊢ ( ⟨ 𝑊 , 𝑁 ⟩ ∈ NrmCVec → 𝑊 ∈ CVecOLD )