Theorem nvvc

Description: The vector space component of a normed complex vector space. (Contributed by NM, 28-Nov-2006) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	nvvc.1	|- W = ( 1st ` U )
Assertion	nvvc	|- ( U e. NrmCVec -> W e. CVecOLD )

Proof

Step	Hyp	Ref	Expression
1		nvvc.1	|- W = ( 1st ` U )
2		eqid	|- ( +v ` U ) = ( +v ` U )
3		eqid	|- ( .sOLD ` U ) = ( .sOLD ` U )
4	1 2 3	nvvop	|- ( U e. NrmCVec -> W = <. ( +v ` U ) , ( .sOLD ` U ) >. )
5		eqid	|- ( BaseSet ` U ) = ( BaseSet ` U )
6		eqid	|- ( 0vec ` U ) = ( 0vec ` U )
7		eqid	|- ( normCV ` U ) = ( normCV ` U )
8	5 2 3 6 7	nvi	|- ( U e. NrmCVec -> ( <. ( +v ` U ) , ( .sOLD ` U ) >. e. CVecOLD /\ ( normCV ` U ) : ( BaseSet ` U ) --> RR /\ A. x e. ( BaseSet ` U ) ( ( ( ( normCV ` U ) ` x ) = 0 -> x = ( 0vec ` U ) ) /\ A. y e. CC ( ( normCV ` U ) ` ( y ( .sOLD ` U ) x ) ) = ( ( abs ` y ) x. ( ( normCV ` U ) ` x ) ) /\ A. y e. ( BaseSet ` U ) ( ( normCV ` U ) ` ( x ( +v ` U ) y ) ) <_ ( ( ( normCV ` U ) ` x ) + ( ( normCV ` U ) ` y ) ) ) ) )
9	8	simp1d	|- ( U e. NrmCVec -> <. ( +v ` U ) , ( .sOLD ` U ) >. e. CVecOLD )
10	4 9	eqeltrd	|- ( U e. NrmCVec -> W e. CVecOLD )