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 >. e. NrmCVec -> W e. CVecOLD )

Proof

Step	Hyp	Ref	Expression
1		nvss	|- NrmCVec C_ ( CVecOLD X. _V )
2	1	sseli	|- ( <. W , N >. e. NrmCVec -> <. W , N >. e. ( CVecOLD X. _V ) )
3		opelxp1	|- ( <. W , N >. e. ( CVecOLD X. _V ) -> W e. CVecOLD )
4	2 3	syl	|- ( <. W , N >. e. NrmCVec -> W e. CVecOLD )