Metamath Proof Explorer

Theorem mdegpropd

Description: Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015) (Proof shortened by AV, 27-Jul-2019)

Ref Expression
Hypotheses mdegpropd.b1 
|- ( ph -> B = ( Base ` R ) )
mdegpropd.b2 
|- ( ph -> B = ( Base ` S ) )
mdegpropd.p 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` S ) y ) )
Assertion mdegpropd 
|- ( ph -> ( I mDeg R ) = ( I mDeg S ) )

Proof

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