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