Metamath Proof Explorer

Theorem deg1mul3le

Description: Degree of multiplication of a polynomial on the left by a scalar. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses deg1mul3le.d 
|- D = ( deg1 ` R )
deg1mul3le.p 
|- P = ( Poly1 ` R )
deg1mul3le.k 
|- K = ( Base ` R )
deg1mul3le.b 
|- B = ( Base ` P )
deg1mul3le.t 
|- .x. = ( .r ` P )
deg1mul3le.a 
|- A = ( algSc ` P )
Assertion deg1mul3le 
|- ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( D ` ( ( A ` F ) .x. G ) ) <_ ( D ` G ) )

Proof

Step Hyp Ref Expression
1 deg1mul3le.d 
 |-  D = ( deg1 ` R )
2 deg1mul3le.p 
 |-  P = ( Poly1 ` R )
3 deg1mul3le.k 
 |-  K = ( Base ` R )
4 deg1mul3le.b 
 |-  B = ( Base ` P )
5 deg1mul3le.t 
 |-  .x. = ( .r ` P )
6 deg1mul3le.a 
 |-  A = ( algSc ` P )
7 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
8 7 3ad2ant1 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> P e. Ring )
9 2 6 3 4 ply1sclf 
 |-  ( R e. Ring -> A : K --> B )
10 9 3ad2ant1 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> A : K --> B )
11 simp2 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> F e. K )
12 10 11 ffvelrnd 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( A ` F ) e. B )
13 simp3 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> G e. B )
14 4 5 ringcl 
 |-  ( ( P e. Ring /\ ( A ` F ) e. B /\ G e. B ) -> ( ( A ` F ) .x. G ) e. B )
15 8 12 13 14 syl3anc 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( ( A ` F ) .x. G ) e. B )
16 eqid 
 |-  ( coe1 ` ( ( A ` F ) .x. G ) ) = ( coe1 ` ( ( A ` F ) .x. G ) )
17 16 4 2 3 coe1f 
 |-  ( ( ( A ` F ) .x. G ) e. B -> ( coe1 ` ( ( A ` F ) .x. G ) ) : NN0 --> K )
18 15 17 syl 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( coe1 ` ( ( A ` F ) .x. G ) ) : NN0 --> K )
19 eldifi 
 |-  ( a e. ( NN0 \ ( ( coe1 ` G ) supp ( 0g ` R ) ) ) -> a e. NN0 )
20 simpl1 
 |-  ( ( ( R e. Ring /\ F e. K /\ G e. B ) /\ a e. NN0 ) -> R e. Ring )
21 simpl2 
 |-  ( ( ( R e. Ring /\ F e. K /\ G e. B ) /\ a e. NN0 ) -> F e. K )
22 simpl3 
 |-  ( ( ( R e. Ring /\ F e. K /\ G e. B ) /\ a e. NN0 ) -> G e. B )
23 simpr 
 |-  ( ( ( R e. Ring /\ F e. K /\ G e. B ) /\ a e. NN0 ) -> a e. NN0 )
24 eqid 
 |-  ( .r ` R ) = ( .r ` R )
25 2 4 3 6 5 24 coe1sclmulfv 
 |-  ( ( R e. Ring /\ ( F e. K /\ G e. B ) /\ a e. NN0 ) -> ( ( coe1 ` ( ( A ` F ) .x. G ) ) ` a ) = ( F ( .r ` R ) ( ( coe1 ` G ) ` a ) ) )
26 20 21 22 23 25 syl121anc 
 |-  ( ( ( R e. Ring /\ F e. K /\ G e. B ) /\ a e. NN0 ) -> ( ( coe1 ` ( ( A ` F ) .x. G ) ) ` a ) = ( F ( .r ` R ) ( ( coe1 ` G ) ` a ) ) )
27 19 26 sylan2 
 |-  ( ( ( R e. Ring /\ F e. K /\ G e. B ) /\ a e. ( NN0 \ ( ( coe1 ` G ) supp ( 0g ` R ) ) ) ) -> ( ( coe1 ` ( ( A ` F ) .x. G ) ) ` a ) = ( F ( .r ` R ) ( ( coe1 ` G ) ` a ) ) )
28 eqid 
 |-  ( coe1 ` G ) = ( coe1 ` G )
29 28 4 2 3 coe1f 
 |-  ( G e. B -> ( coe1 ` G ) : NN0 --> K )
30 29 3ad2ant3 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( coe1 ` G ) : NN0 --> K )
31 ssidd 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( ( coe1 ` G ) supp ( 0g ` R ) ) C_ ( ( coe1 ` G ) supp ( 0g ` R ) ) )
32 nn0ex 
 |-  NN0 e. _V
33 32 a1i 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> NN0 e. _V )
34 fvexd 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( 0g ` R ) e. _V )
35 30 31 33 34 suppssr 
 |-  ( ( ( R e. Ring /\ F e. K /\ G e. B ) /\ a e. ( NN0 \ ( ( coe1 ` G ) supp ( 0g ` R ) ) ) ) -> ( ( coe1 ` G ) ` a ) = ( 0g ` R ) )
36 35 oveq2d 
 |-  ( ( ( R e. Ring /\ F e. K /\ G e. B ) /\ a e. ( NN0 \ ( ( coe1 ` G ) supp ( 0g ` R ) ) ) ) -> ( F ( .r ` R ) ( ( coe1 ` G ) ` a ) ) = ( F ( .r ` R ) ( 0g ` R ) ) )
37 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
38 3 24 37 ringrz 
 |-  ( ( R e. Ring /\ F e. K ) -> ( F ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
39 38 3adant3 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( F ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
40 39 adantr 
 |-  ( ( ( R e. Ring /\ F e. K /\ G e. B ) /\ a e. ( NN0 \ ( ( coe1 ` G ) supp ( 0g ` R ) ) ) ) -> ( F ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
41 27 36 40 3eqtrd 
 |-  ( ( ( R e. Ring /\ F e. K /\ G e. B ) /\ a e. ( NN0 \ ( ( coe1 ` G ) supp ( 0g ` R ) ) ) ) -> ( ( coe1 ` ( ( A ` F ) .x. G ) ) ` a ) = ( 0g ` R ) )
42 18 41 suppss 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( ( coe1 ` ( ( A ` F ) .x. G ) ) supp ( 0g ` R ) ) C_ ( ( coe1 ` G ) supp ( 0g ` R ) ) )
43 suppssdm 
 |-  ( ( coe1 ` G ) supp ( 0g ` R ) ) C_ dom ( coe1 ` G )
44 43 30 fssdm 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( ( coe1 ` G ) supp ( 0g ` R ) ) C_ NN0 )
45 nn0ssre 
 |-  NN0 C_ RR
46 ressxr 
 |-  RR C_ RR*
47 45 46 sstri 
 |-  NN0 C_ RR*
48 44 47 sstrdi 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( ( coe1 ` G ) supp ( 0g ` R ) ) C_ RR* )
49 supxrss 
 |-  ( ( ( ( coe1 ` ( ( A ` F ) .x. G ) ) supp ( 0g ` R ) ) C_ ( ( coe1 ` G ) supp ( 0g ` R ) ) /\ ( ( coe1 ` G ) supp ( 0g ` R ) ) C_ RR* ) -> sup ( ( ( coe1 ` ( ( A ` F ) .x. G ) ) supp ( 0g ` R ) ) , RR* , < ) <_ sup ( ( ( coe1 ` G ) supp ( 0g ` R ) ) , RR* , < ) )
50 42 48 49 syl2anc 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> sup ( ( ( coe1 ` ( ( A ` F ) .x. G ) ) supp ( 0g ` R ) ) , RR* , < ) <_ sup ( ( ( coe1 ` G ) supp ( 0g ` R ) ) , RR* , < ) )
51 1 2 4 37 16 deg1val 
 |-  ( ( ( A ` F ) .x. G ) e. B -> ( D ` ( ( A ` F ) .x. G ) ) = sup ( ( ( coe1 ` ( ( A ` F ) .x. G ) ) supp ( 0g ` R ) ) , RR* , < ) )
52 15 51 syl 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( D ` ( ( A ` F ) .x. G ) ) = sup ( ( ( coe1 ` ( ( A ` F ) .x. G ) ) supp ( 0g ` R ) ) , RR* , < ) )
53 1 2 4 37 28 deg1val 
 |-  ( G e. B -> ( D ` G ) = sup ( ( ( coe1 ` G ) supp ( 0g ` R ) ) , RR* , < ) )
54 53 3ad2ant3 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( D ` G ) = sup ( ( ( coe1 ` G ) supp ( 0g ` R ) ) , RR* , < ) )
55 50 52 54 3brtr4d 
 |-  ( ( R e. Ring /\ F e. K /\ G e. B ) -> ( D ` ( ( A ` F ) .x. G ) ) <_ ( D ` G ) )