Step |
Hyp |
Ref |
Expression |
1 |
|
h2h.1 |
|- U = <. <. +h , .h >. , normh >. |
2 |
|
h2h.2 |
|- U e. NrmCVec |
3 |
|
eqid |
|- ( .sOLD ` <. <. +h , .h >. , normh >. ) = ( .sOLD ` <. <. +h , .h >. , normh >. ) |
4 |
3
|
smfval |
|- ( .sOLD ` <. <. +h , .h >. , normh >. ) = ( 2nd ` ( 1st ` <. <. +h , .h >. , normh >. ) ) |
5 |
|
opex |
|- <. +h , .h >. e. _V |
6 |
1 2
|
eqeltrri |
|- <. <. +h , .h >. , normh >. e. NrmCVec |
7 |
|
nvex |
|- ( <. <. +h , .h >. , normh >. e. NrmCVec -> ( +h e. _V /\ .h e. _V /\ normh e. _V ) ) |
8 |
6 7
|
ax-mp |
|- ( +h e. _V /\ .h e. _V /\ normh e. _V ) |
9 |
8
|
simp3i |
|- normh e. _V |
10 |
5 9
|
op1st |
|- ( 1st ` <. <. +h , .h >. , normh >. ) = <. +h , .h >. |
11 |
10
|
fveq2i |
|- ( 2nd ` ( 1st ` <. <. +h , .h >. , normh >. ) ) = ( 2nd ` <. +h , .h >. ) |
12 |
8
|
simp1i |
|- +h e. _V |
13 |
8
|
simp2i |
|- .h e. _V |
14 |
12 13
|
op2nd |
|- ( 2nd ` <. +h , .h >. ) = .h |
15 |
4 11 14
|
3eqtrri |
|- .h = ( .sOLD ` <. <. +h , .h >. , normh >. ) |
16 |
1
|
fveq2i |
|- ( .sOLD ` U ) = ( .sOLD ` <. <. +h , .h >. , normh >. ) |
17 |
15 16
|
eqtr4i |
|- .h = ( .sOLD ` U ) |