Metamath Proof Explorer

Theorem mdegvsca

Description: The degree of a scalar multiple of a polynomial is exactly the degree of the original polynomial when the multiple is a nonzero-divisor. (Contributed by Stefan O'Rear, 28-Mar-2015) (Proof shortened by AV, 27-Jul-2019)

Ref Expression
Hypotheses mdegaddle.y 
|- Y = ( I mPoly R )
mdegaddle.d 
|- D = ( I mDeg R )
mdegaddle.i 
|- ( ph -> I e. V )
mdegaddle.r 
|- ( ph -> R e. Ring )
mdegvsca.b 
|- B = ( Base ` Y )
mdegvsca.e 
|- E = ( RLReg ` R )
mdegvsca.p 
|- .x. = ( .s ` Y )
mdegvsca.f 
|- ( ph -> F e. E )
mdegvsca.g 
|- ( ph -> G e. B )
Assertion mdegvsca 
|- ( ph -> ( D ` ( F .x. G ) ) = ( D ` G ) )

Proof

Step Hyp Ref Expression
1 mdegaddle.y 
 |-  Y = ( I mPoly R )
2 mdegaddle.d 
 |-  D = ( I mDeg R )
3 mdegaddle.i 
 |-  ( ph -> I e. V )
4 mdegaddle.r 
 |-  ( ph -> R e. Ring )
5 mdegvsca.b 
 |-  B = ( Base ` Y )
6 mdegvsca.e 
 |-  E = ( RLReg ` R )
7 mdegvsca.p 
 |-  .x. = ( .s ` Y )
8 mdegvsca.f 
 |-  ( ph -> F e. E )
9 mdegvsca.g 
 |-  ( ph -> G e. B )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 eqid 
 |-  ( .r ` R ) = ( .r ` R )
12 eqid 
 |-  { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } = { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin }
13 6 10 rrgss 
 |-  E C_ ( Base ` R )
14 13 8 sselid 
 |-  ( ph -> F e. ( Base ` R ) )
15 1 7 10 5 11 12 14 9 mplvsca 
 |-  ( ph -> ( F .x. G ) = ( ( { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } X. { F } ) oF ( .r ` R ) G ) )
16 15 oveq1d 
 |-  ( ph -> ( ( F .x. G ) supp ( 0g ` R ) ) = ( ( ( { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } X. { F } ) oF ( .r ` R ) G ) supp ( 0g ` R ) ) )
17 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
18 ovex 
 |-  ( NN0 ^m I ) e. _V
19 18 rabex 
 |-  { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } e. _V
20 19 a1i 
 |-  ( ph -> { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } e. _V )
21 1 10 5 12 9 mplelf 
 |-  ( ph -> G : { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } --> ( Base ` R ) )
22 6 10 11 17 20 4 8 21 rrgsupp 
 |-  ( ph -> ( ( ( { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } X. { F } ) oF ( .r ` R ) G ) supp ( 0g ` R ) ) = ( G supp ( 0g ` R ) ) )
23 16 22 eqtrd 
 |-  ( ph -> ( ( F .x. G ) supp ( 0g ` R ) ) = ( G supp ( 0g ` R ) ) )
24 23 imaeq2d 
 |-  ( ph -> ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( ( F .x. G ) supp ( 0g ` R ) ) ) = ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( G supp ( 0g ` R ) ) ) )
25 24 supeq1d 
 |-  ( ph -> sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( ( F .x. G ) supp ( 0g ` R ) ) ) , RR* , < ) = sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( G supp ( 0g ` R ) ) ) , RR* , < ) )
26 1 3 4 mpllmodd 
 |-  ( ph -> Y e. LMod )
27 1 3 4 mplsca 
 |-  ( ph -> R = ( Scalar ` Y ) )
28 27 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` Y ) ) )
29 14 28 eleqtrd 
 |-  ( ph -> F e. ( Base ` ( Scalar ` Y ) ) )
30 eqid 
 |-  ( Scalar ` Y ) = ( Scalar ` Y )
31 eqid 
 |-  ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
32 5 30 7 31 lmodvscl 
 |-  ( ( Y e. LMod /\ F e. ( Base ` ( Scalar ` Y ) ) /\ G e. B ) -> ( F .x. G ) e. B )
33 26 29 9 32 syl3anc 
 |-  ( ph -> ( F .x. G ) e. B )
34 eqid 
 |-  ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) = ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) )
35 2 1 5 17 12 34 mdegval 
 |-  ( ( F .x. G ) e. B -> ( D ` ( F .x. G ) ) = sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( ( F .x. G ) supp ( 0g ` R ) ) ) , RR* , < ) )
36 33 35 syl 
 |-  ( ph -> ( D ` ( F .x. G ) ) = sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( ( F .x. G ) supp ( 0g ` R ) ) ) , RR* , < ) )
37 2 1 5 17 12 34 mdegval 
 |-  ( G e. B -> ( D ` G ) = sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( G supp ( 0g ` R ) ) ) , RR* , < ) )
38 9 37 syl 
 |-  ( ph -> ( D ` G ) = sup ( ( ( y e. { x e. ( NN0 ^m I ) | ( `' x " NN ) e. Fin } |-> ( CCfld gsum y ) ) " ( G supp ( 0g ` R ) ) ) , RR* , < ) )
39 25 36 38 3eqtr4d 
 |-  ( ph -> ( D ` ( F .x. G ) ) = ( D ` G ) )