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 >. )