| Step |
Hyp |
Ref |
Expression |
| 1 |
|
fvi |
|- ( R e. _V -> ( _I ` R ) = R ) |
| 2 |
1
|
fveq2d |
|- ( R e. _V -> ( Poly1 ` ( _I ` R ) ) = ( Poly1 ` R ) ) |
| 3 |
2
|
fveq2d |
|- ( R e. _V -> ( +g ` ( Poly1 ` ( _I ` R ) ) ) = ( +g ` ( Poly1 ` R ) ) ) |
| 4 |
|
eqid |
|- ( Poly1 ` (/) ) = ( Poly1 ` (/) ) |
| 5 |
|
eqid |
|- ( 1o mPoly (/) ) = ( 1o mPoly (/) ) |
| 6 |
|
eqid |
|- ( +g ` ( Poly1 ` (/) ) ) = ( +g ` ( Poly1 ` (/) ) ) |
| 7 |
4 5 6
|
ply1plusg |
|- ( +g ` ( Poly1 ` (/) ) ) = ( +g ` ( 1o mPoly (/) ) ) |
| 8 |
|
eqid |
|- ( 1o mPwSer (/) ) = ( 1o mPwSer (/) ) |
| 9 |
|
eqid |
|- ( +g ` ( 1o mPoly (/) ) ) = ( +g ` ( 1o mPoly (/) ) ) |
| 10 |
5 8 9
|
mplplusg |
|- ( +g ` ( 1o mPoly (/) ) ) = ( +g ` ( 1o mPwSer (/) ) ) |
| 11 |
|
base0 |
|- (/) = ( Base ` (/) ) |
| 12 |
|
psr1baslem |
|- ( NN0 ^m 1o ) = { a e. ( NN0 ^m 1o ) | ( `' a " NN ) e. Fin } |
| 13 |
|
eqid |
|- ( Base ` ( 1o mPwSer (/) ) ) = ( Base ` ( 1o mPwSer (/) ) ) |
| 14 |
|
1on |
|- 1o e. On |
| 15 |
14
|
a1i |
|- ( T. -> 1o e. On ) |
| 16 |
8 11 12 13 15
|
psrbas |
|- ( T. -> ( Base ` ( 1o mPwSer (/) ) ) = ( (/) ^m ( NN0 ^m 1o ) ) ) |
| 17 |
16
|
mptru |
|- ( Base ` ( 1o mPwSer (/) ) ) = ( (/) ^m ( NN0 ^m 1o ) ) |
| 18 |
|
0nn0 |
|- 0 e. NN0 |
| 19 |
18
|
fconst6 |
|- ( 1o X. { 0 } ) : 1o --> NN0 |
| 20 |
|
nn0ex |
|- NN0 e. _V |
| 21 |
|
1oex |
|- 1o e. _V |
| 22 |
20 21
|
elmap |
|- ( ( 1o X. { 0 } ) e. ( NN0 ^m 1o ) <-> ( 1o X. { 0 } ) : 1o --> NN0 ) |
| 23 |
19 22
|
mpbir |
|- ( 1o X. { 0 } ) e. ( NN0 ^m 1o ) |
| 24 |
|
ne0i |
|- ( ( 1o X. { 0 } ) e. ( NN0 ^m 1o ) -> ( NN0 ^m 1o ) =/= (/) ) |
| 25 |
|
map0b |
|- ( ( NN0 ^m 1o ) =/= (/) -> ( (/) ^m ( NN0 ^m 1o ) ) = (/) ) |
| 26 |
23 24 25
|
mp2b |
|- ( (/) ^m ( NN0 ^m 1o ) ) = (/) |
| 27 |
17 26
|
eqtr2i |
|- (/) = ( Base ` ( 1o mPwSer (/) ) ) |
| 28 |
|
eqid |
|- ( +g ` (/) ) = ( +g ` (/) ) |
| 29 |
|
eqid |
|- ( +g ` ( 1o mPwSer (/) ) ) = ( +g ` ( 1o mPwSer (/) ) ) |
| 30 |
8 27 28 29
|
psrplusg |
|- ( +g ` ( 1o mPwSer (/) ) ) = ( oF ( +g ` (/) ) |` ( (/) X. (/) ) ) |
| 31 |
|
xp0 |
|- ( (/) X. (/) ) = (/) |
| 32 |
31
|
reseq2i |
|- ( oF ( +g ` (/) ) |` ( (/) X. (/) ) ) = ( oF ( +g ` (/) ) |` (/) ) |
| 33 |
10 30 32
|
3eqtri |
|- ( +g ` ( 1o mPoly (/) ) ) = ( oF ( +g ` (/) ) |` (/) ) |
| 34 |
|
res0 |
|- ( oF ( +g ` (/) ) |` (/) ) = (/) |
| 35 |
|
df-plusg |
|- +g = Slot 2 |
| 36 |
35
|
str0 |
|- (/) = ( +g ` (/) ) |
| 37 |
34 36
|
eqtri |
|- ( oF ( +g ` (/) ) |` (/) ) = ( +g ` (/) ) |
| 38 |
7 33 37
|
3eqtri |
|- ( +g ` ( Poly1 ` (/) ) ) = ( +g ` (/) ) |
| 39 |
|
fvprc |
|- ( -. R e. _V -> ( _I ` R ) = (/) ) |
| 40 |
39
|
fveq2d |
|- ( -. R e. _V -> ( Poly1 ` ( _I ` R ) ) = ( Poly1 ` (/) ) ) |
| 41 |
40
|
fveq2d |
|- ( -. R e. _V -> ( +g ` ( Poly1 ` ( _I ` R ) ) ) = ( +g ` ( Poly1 ` (/) ) ) ) |
| 42 |
|
fvprc |
|- ( -. R e. _V -> ( Poly1 ` R ) = (/) ) |
| 43 |
42
|
fveq2d |
|- ( -. R e. _V -> ( +g ` ( Poly1 ` R ) ) = ( +g ` (/) ) ) |
| 44 |
38 41 43
|
3eqtr4a |
|- ( -. R e. _V -> ( +g ` ( Poly1 ` ( _I ` R ) ) ) = ( +g ` ( Poly1 ` R ) ) ) |
| 45 |
3 44
|
pm2.61i |
|- ( +g ` ( Poly1 ` ( _I ` R ) ) ) = ( +g ` ( Poly1 ` R ) ) |
| 46 |
45
|
eqcomi |
|- ( +g ` ( Poly1 ` R ) ) = ( +g ` ( Poly1 ` ( _I ` R ) ) ) |