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	$$⊢⟨W,N⟩\in \mathrm{NrmCVec}\to W\in {CVec}_{\mathrm{OLD}}$$

Proof

Step	Hyp	Ref	Expression
1		nvss	$$⊢\mathrm{NrmCVec}\subseteq {CVec}_{\mathrm{OLD}}\times \mathrm{V}$$
2	1	sseli	$$⊢⟨W,N⟩\in \mathrm{NrmCVec}\to ⟨W,N⟩\in \left({CVec}_{\mathrm{OLD}}\times \mathrm{V}\right)$$
3		opelxp1	$$⊢⟨W,N⟩\in \left({CVec}_{\mathrm{OLD}}\times \mathrm{V}\right)\to W\in {CVec}_{\mathrm{OLD}}$$
4	2 3	syl	$$⊢⟨W,N⟩\in \mathrm{NrmCVec}\to W\in {CVec}_{\mathrm{OLD}}$$