Step |
Hyp |
Ref |
Expression |
1 |
|
ply1baspropd.b1 |
|- ( ph -> B = ( Base ` R ) ) |
2 |
|
ply1baspropd.b2 |
|- ( ph -> B = ( Base ` S ) ) |
3 |
|
ply1baspropd.p |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) ) |
4 |
1 2 3
|
psrplusgpropd |
|- ( ph -> ( +g ` ( 1o mPwSer R ) ) = ( +g ` ( 1o mPwSer S ) ) ) |
5 |
|
eqid |
|- ( 1o mPoly R ) = ( 1o mPoly R ) |
6 |
|
eqid |
|- ( 1o mPwSer R ) = ( 1o mPwSer R ) |
7 |
|
eqid |
|- ( +g ` ( 1o mPoly R ) ) = ( +g ` ( 1o mPoly R ) ) |
8 |
5 6 7
|
mplplusg |
|- ( +g ` ( 1o mPoly R ) ) = ( +g ` ( 1o mPwSer R ) ) |
9 |
|
eqid |
|- ( 1o mPoly S ) = ( 1o mPoly S ) |
10 |
|
eqid |
|- ( 1o mPwSer S ) = ( 1o mPwSer S ) |
11 |
|
eqid |
|- ( +g ` ( 1o mPoly S ) ) = ( +g ` ( 1o mPoly S ) ) |
12 |
9 10 11
|
mplplusg |
|- ( +g ` ( 1o mPoly S ) ) = ( +g ` ( 1o mPwSer S ) ) |
13 |
4 8 12
|
3eqtr4g |
|- ( ph -> ( +g ` ( 1o mPoly R ) ) = ( +g ` ( 1o mPoly S ) ) ) |
14 |
|
eqid |
|- ( Poly1 ` R ) = ( Poly1 ` R ) |
15 |
|
eqid |
|- ( +g ` ( Poly1 ` R ) ) = ( +g ` ( Poly1 ` R ) ) |
16 |
14 5 15
|
ply1plusg |
|- ( +g ` ( Poly1 ` R ) ) = ( +g ` ( 1o mPoly R ) ) |
17 |
|
eqid |
|- ( Poly1 ` S ) = ( Poly1 ` S ) |
18 |
|
eqid |
|- ( +g ` ( Poly1 ` S ) ) = ( +g ` ( Poly1 ` S ) ) |
19 |
17 9 18
|
ply1plusg |
|- ( +g ` ( Poly1 ` S ) ) = ( +g ` ( 1o mPoly S ) ) |
20 |
13 16 19
|
3eqtr4g |
|- ( ph -> ( +g ` ( Poly1 ` R ) ) = ( +g ` ( Poly1 ` S ) ) ) |