This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )