Step |
Hyp |
Ref |
Expression |
1 |
|
mdegpropd.b1 |
|- ( ph -> B = ( Base ` R ) ) |
2 |
|
mdegpropd.b2 |
|- ( ph -> B = ( Base ` S ) ) |
3 |
|
mdegpropd.p |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) ) |
4 |
1 2 3
|
mplbaspropd |
|- ( ph -> ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly S ) ) ) |
5 |
1 2 3
|
grpidpropd |
|- ( ph -> ( 0g ` R ) = ( 0g ` S ) ) |
6 |
5
|
oveq2d |
|- ( ph -> ( c supp ( 0g ` R ) ) = ( c supp ( 0g ` S ) ) ) |
7 |
6
|
imaeq2d |
|- ( ph -> ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( c supp ( 0g ` R ) ) ) = ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( c supp ( 0g ` S ) ) ) ) |
8 |
7
|
supeq1d |
|- ( ph -> sup ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( c supp ( 0g ` R ) ) ) , RR* , < ) = sup ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( c supp ( 0g ` S ) ) ) , RR* , < ) ) |
9 |
4 8
|
mpteq12dv |
|- ( ph -> ( c e. ( Base ` ( I mPoly R ) ) |-> sup ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( c supp ( 0g ` R ) ) ) , RR* , < ) ) = ( c e. ( Base ` ( I mPoly S ) ) |-> sup ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( c supp ( 0g ` S ) ) ) , RR* , < ) ) ) |
10 |
|
eqid |
|- ( I mDeg R ) = ( I mDeg R ) |
11 |
|
eqid |
|- ( I mPoly R ) = ( I mPoly R ) |
12 |
|
eqid |
|- ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly R ) ) |
13 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
14 |
|
eqid |
|- { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } = { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |
15 |
|
eqid |
|- ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) = ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) |
16 |
10 11 12 13 14 15
|
mdegfval |
|- ( I mDeg R ) = ( c e. ( Base ` ( I mPoly R ) ) |-> sup ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( c supp ( 0g ` R ) ) ) , RR* , < ) ) |
17 |
|
eqid |
|- ( I mDeg S ) = ( I mDeg S ) |
18 |
|
eqid |
|- ( I mPoly S ) = ( I mPoly S ) |
19 |
|
eqid |
|- ( Base ` ( I mPoly S ) ) = ( Base ` ( I mPoly S ) ) |
20 |
|
eqid |
|- ( 0g ` S ) = ( 0g ` S ) |
21 |
17 18 19 20 14 15
|
mdegfval |
|- ( I mDeg S ) = ( c e. ( Base ` ( I mPoly S ) ) |-> sup ( ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) " ( c supp ( 0g ` S ) ) ) , RR* , < ) ) |
22 |
9 16 21
|
3eqtr4g |
|- ( ph -> ( I mDeg R ) = ( I mDeg S ) ) |