Metamath Proof Explorer

Theorem mdegvscale

Description: The degree of a scalar multiple of a polynomial is at most the degree of the original polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015)

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 )
mdegvscale.b 
|- B = ( Base ` Y )
mdegvscale.k 
|- K = ( Base ` R )
mdegvscale.p 
|- .x. = ( .s ` Y )
mdegvscale.f 
|- ( ph -> F e. K )
mdegvscale.g 
|- ( ph -> G e. B )
Assertion mdegvscale 
|- ( 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 mdegvscale.b 
 |-  B = ( Base ` Y )
6 mdegvscale.k 
 |-  K = ( Base ` R )
7 mdegvscale.p 
 |-  .x. = ( .s ` Y )
8 mdegvscale.f 
 |-  ( ph -> F e. K )
9 mdegvscale.g 
 |-  ( ph -> G e. B )
10 eqid 
 |-  ( .r ` R ) = ( .r ` R )
11 eqid 
 |-  { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } = { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin }
12 8 adantr 
 |-  ( ( ph /\ x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> F e. K )
13 9 adantr 
 |-  ( ( ph /\ x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> G e. B )
14 simpr 
 |-  ( ( ph /\ x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } )
15 1 7 6 5 10 11 12 13 14 mplvscaval 
 |-  ( ( ph /\ x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( F .x. G ) ` x ) = ( F ( .r ` R ) ( G ` x ) ) )
16 15 adantrr 
 |-  ( ( ph /\ ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ ( D ` G ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) ) ) -> ( ( F .x. G ) ` x ) = ( F ( .r ` R ) ( G ` x ) ) )
17 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
18 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 ) )
19 9 adantr 
 |-  ( ( ph /\ ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ ( D ` G ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) ) ) -> G e. B )
20 simprl 
 |-  ( ( ph /\ ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ ( D ` G ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) ) ) -> x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } )
21 simprr 
 |-  ( ( ph /\ ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ ( D ` G ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) ) ) -> ( D ` G ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) )
22 2 1 5 17 11 18 19 20 21 mdeglt 
 |-  ( ( ph /\ ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ ( D ` G ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) ) ) -> ( G ` x ) = ( 0g ` R ) )
23 22 oveq2d 
 |-  ( ( ph /\ ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ ( D ` G ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) ) ) -> ( F ( .r ` R ) ( G ` x ) ) = ( F ( .r ` R ) ( 0g ` R ) ) )
24 6 10 17 ringrz 
 |-  ( ( R e. Ring /\ F e. K ) -> ( F ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
25 4 8 24 syl2anc 
 |-  ( ph -> ( F ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
26 25 adantr 
 |-  ( ( ph /\ ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ ( D ` G ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) ) ) -> ( F ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
27 16 23 26 3eqtrd 
 |-  ( ( ph /\ ( x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } /\ ( D ` G ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) ) ) -> ( ( F .x. G ) ` x ) = ( 0g ` R ) )
28 27 expr 
 |-  ( ( ph /\ x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ) -> ( ( D ` G ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) -> ( ( F .x. G ) ` x ) = ( 0g ` R ) ) )
29 28 ralrimiva 
 |-  ( ph -> A. x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( ( D ` G ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) -> ( ( F .x. G ) ` x ) = ( 0g ` R ) ) )
30 1 mpllmod 
 |-  ( ( I e. V /\ R e. Ring ) -> Y e. LMod )
31 3 4 30 syl2anc 
 |-  ( ph -> Y e. LMod )
32 1 3 4 mplsca 
 |-  ( ph -> R = ( Scalar ` Y ) )
33 32 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` Y ) ) )
34 6 33 syl5eq 
 |-  ( ph -> K = ( Base ` ( Scalar ` Y ) ) )
35 8 34 eleqtrd 
 |-  ( ph -> F e. ( Base ` ( Scalar ` Y ) ) )
36 eqid 
 |-  ( Scalar ` Y ) = ( Scalar ` Y )
37 eqid 
 |-  ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
38 5 36 7 37 lmodvscl 
 |-  ( ( Y e. LMod /\ F e. ( Base ` ( Scalar ` Y ) ) /\ G e. B ) -> ( F .x. G ) e. B )
39 31 35 9 38 syl3anc 
 |-  ( ph -> ( F .x. G ) e. B )
40 2 1 5 mdegxrcl 
 |-  ( G e. B -> ( D ` G ) e. RR* )
41 9 40 syl 
 |-  ( ph -> ( D ` G ) e. RR* )
42 2 1 5 17 11 18 mdegleb 
 |-  ( ( ( F .x. G ) e. B /\ ( D ` G ) e. RR* ) -> ( ( D ` ( F .x. G ) ) <_ ( D ` G ) <-> A. x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( ( D ` G ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) -> ( ( F .x. G ) ` x ) = ( 0g ` R ) ) ) )
43 39 41 42 syl2anc 
 |-  ( ph -> ( ( D ` ( F .x. G ) ) <_ ( D ` G ) <-> A. x e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } ( ( D ` G ) < ( ( b e. { a e. ( NN0 ^m I ) | ( `' a " NN ) e. Fin } |-> ( CCfld gsum b ) ) ` x ) -> ( ( F .x. G ) ` x ) = ( 0g ` R ) ) ) )
44 29 43 mpbird 
 |-  ( ph -> ( D ` ( F .x. G ) ) <_ ( D ` G ) )