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

Metamath Proof Explorer

Theorem nvvop

Description: The vector space component of a normed complex vector space is an ordered pair of the underlying group and a scalar product. (Contributed by NM, 28-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nvvop.1 
|- W = ( 1st ` U )
nvvop.2 
|- G = ( +v ` U )
nvvop.4 
|- S = ( .sOLD ` U )
Assertion nvvop 
|- ( U e. NrmCVec -> W = <. G , S >. )

Proof

Step Hyp Ref Expression
1 nvvop.1 
 |-  W = ( 1st ` U )
2 nvvop.2 
 |-  G = ( +v ` U )
3 nvvop.4 
 |-  S = ( .sOLD ` U )
4 vcrel 
 |-  Rel CVecOLD
5 nvss 
 |-  NrmCVec C_ ( CVecOLD X. _V )
6 eqid 
 |-  ( normCV ` U ) = ( normCV ` U )
7 1 6 nvop2 
 |-  ( U e. NrmCVec -> U = <. W , ( normCV ` U ) >. )
8 7 eleq1d 
 |-  ( U e. NrmCVec -> ( U e. NrmCVec <-> <. W , ( normCV ` U ) >. e. NrmCVec ) )
9 8 ibi 
 |-  ( U e. NrmCVec -> <. W , ( normCV ` U ) >. e. NrmCVec )
10 5 9 sselid 
 |-  ( U e. NrmCVec -> <. W , ( normCV ` U ) >. e. ( CVecOLD X. _V ) )
11 opelxp1 
 |-  ( <. W , ( normCV ` U ) >. e. ( CVecOLD X. _V ) -> W e. CVecOLD )
12 10 11 syl 
 |-  ( U e. NrmCVec -> W e. CVecOLD )
13 1st2nd 
 |-  ( ( Rel CVecOLD /\ W e. CVecOLD ) -> W = <. ( 1st ` W ) , ( 2nd ` W ) >. )
14 4 12 13 sylancr 
 |-  ( U e. NrmCVec -> W = <. ( 1st ` W ) , ( 2nd ` W ) >. )
15 2 vafval 
 |-  G = ( 1st ` ( 1st ` U ) )
16 1 fveq2i 
 |-  ( 1st ` W ) = ( 1st ` ( 1st ` U ) )
17 15 16 eqtr4i 
 |-  G = ( 1st ` W )
18 3 smfval 
 |-  S = ( 2nd ` ( 1st ` U ) )
19 1 fveq2i 
 |-  ( 2nd ` W ) = ( 2nd ` ( 1st ` U ) )
20 18 19 eqtr4i 
 |-  S = ( 2nd ` W )
21 17 20 opeq12i 
 |-  <. G , S >. = <. ( 1st ` W ) , ( 2nd ` W ) >.
22 14 21 eqtr4di 
 |-  ( U e. NrmCVec -> W = <. G , S >. )