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