Metamath Proof Explorer


Theorem ply1plusgfvi

Description: Protection compatibility of the univariate polynomial addition. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Assertion ply1plusgfvi
|- ( +g ` ( Poly1 ` R ) ) = ( +g ` ( Poly1 ` ( _I ` R ) ) )

Proof

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 plusgid
 |-  +g = Slot ( +g ` ndx )
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 ) ) )