Step |
Hyp |
Ref |
Expression |
1 |
|
cnnvg.6 |
|- U = <. <. + , x. >. , abs >. |
2 |
|
eqid |
|- ( +v ` U ) = ( +v ` U ) |
3 |
2
|
vafval |
|- ( +v ` U ) = ( 1st ` ( 1st ` U ) ) |
4 |
1
|
fveq2i |
|- ( 1st ` U ) = ( 1st ` <. <. + , x. >. , abs >. ) |
5 |
|
opex |
|- <. + , x. >. e. _V |
6 |
|
absf |
|- abs : CC --> RR |
7 |
|
cnex |
|- CC e. _V |
8 |
|
fex |
|- ( ( abs : CC --> RR /\ CC e. _V ) -> abs e. _V ) |
9 |
6 7 8
|
mp2an |
|- abs e. _V |
10 |
5 9
|
op1st |
|- ( 1st ` <. <. + , x. >. , abs >. ) = <. + , x. >. |
11 |
4 10
|
eqtri |
|- ( 1st ` U ) = <. + , x. >. |
12 |
11
|
fveq2i |
|- ( 1st ` ( 1st ` U ) ) = ( 1st ` <. + , x. >. ) |
13 |
|
addex |
|- + e. _V |
14 |
|
mulex |
|- x. e. _V |
15 |
13 14
|
op1st |
|- ( 1st ` <. + , x. >. ) = + |
16 |
3 12 15
|
3eqtrri |
|- + = ( +v ` U ) |