Metamath Proof Explorer

Theorem deg1mul2

Description: Degree of multiplication of two nonzero polynomials when the first leads with a nonzero-divisor coefficient. (Contributed by Stefan O'Rear, 26-Mar-2015)

Ref Expression
Hypotheses deg1mul2.d 
|- D = ( deg1 ` R )
deg1mul2.p 
|- P = ( Poly1 ` R )
deg1mul2.e 
|- E = ( RLReg ` R )
deg1mul2.b 
|- B = ( Base ` P )
deg1mul2.t 
|- .x. = ( .r ` P )
deg1mul2.z 
|- .0. = ( 0g ` P )
deg1mul2.r 
|- ( ph -> R e. Ring )
deg1mul2.fb 
|- ( ph -> F e. B )
deg1mul2.fz 
|- ( ph -> F =/= .0. )
deg1mul2.fc 
|- ( ph -> ( ( coe1 ` F ) ` ( D ` F ) ) e. E )
deg1mul2.gb 
|- ( ph -> G e. B )
deg1mul2.gz 
|- ( ph -> G =/= .0. )
Assertion deg1mul2 
|- ( ph -> ( D ` ( F .x. G ) ) = ( ( D ` F ) + ( D ` G ) ) )

Proof

Step Hyp Ref Expression
1 deg1mul2.d 
 |-  D = ( deg1 ` R )
2 deg1mul2.p 
 |-  P = ( Poly1 ` R )
3 deg1mul2.e 
 |-  E = ( RLReg ` R )
4 deg1mul2.b 
 |-  B = ( Base ` P )
5 deg1mul2.t 
 |-  .x. = ( .r ` P )
6 deg1mul2.z 
 |-  .0. = ( 0g ` P )
7 deg1mul2.r 
 |-  ( ph -> R e. Ring )
8 deg1mul2.fb 
 |-  ( ph -> F e. B )
9 deg1mul2.fz 
 |-  ( ph -> F =/= .0. )
10 deg1mul2.fc 
 |-  ( ph -> ( ( coe1 ` F ) ` ( D ` F ) ) e. E )
11 deg1mul2.gb 
 |-  ( ph -> G e. B )
12 deg1mul2.gz 
 |-  ( ph -> G =/= .0. )
13 2 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
14 7 13 syl 
 |-  ( ph -> P e. Ring )
15 4 5 ringcl 
 |-  ( ( P e. Ring /\ F e. B /\ G e. B ) -> ( F .x. G ) e. B )
16 14 8 11 15 syl3anc 
 |-  ( ph -> ( F .x. G ) e. B )
17 1 2 4 deg1xrcl 
 |-  ( ( F .x. G ) e. B -> ( D ` ( F .x. G ) ) e. RR* )
18 16 17 syl 
 |-  ( ph -> ( D ` ( F .x. G ) ) e. RR* )
19 1 2 6 4 deg1nn0cl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= .0. ) -> ( D ` F ) e. NN0 )
20 7 8 9 19 syl3anc 
 |-  ( ph -> ( D ` F ) e. NN0 )
21 1 2 6 4 deg1nn0cl 
 |-  ( ( R e. Ring /\ G e. B /\ G =/= .0. ) -> ( D ` G ) e. NN0 )
22 7 11 12 21 syl3anc 
 |-  ( ph -> ( D ` G ) e. NN0 )
23 20 22 nn0addcld 
 |-  ( ph -> ( ( D ` F ) + ( D ` G ) ) e. NN0 )
24 23 nn0red 
 |-  ( ph -> ( ( D ` F ) + ( D ` G ) ) e. RR )
25 24 rexrd 
 |-  ( ph -> ( ( D ` F ) + ( D ` G ) ) e. RR* )
26 20 nn0red 
 |-  ( ph -> ( D ` F ) e. RR )
27 26 leidd 
 |-  ( ph -> ( D ` F ) <_ ( D ` F ) )
28 22 nn0red 
 |-  ( ph -> ( D ` G ) e. RR )
29 28 leidd 
 |-  ( ph -> ( D ` G ) <_ ( D ` G ) )
30 2 1 7 4 5 8 11 20 22 27 29 deg1mulle2 
 |-  ( ph -> ( D ` ( F .x. G ) ) <_ ( ( D ` F ) + ( D ` G ) ) )
31 eqid 
 |-  ( .r ` R ) = ( .r ` R )
32 2 5 31 4 1 6 7 8 9 11 12 coe1mul4 
 |-  ( ph -> ( ( coe1 ` ( F .x. G ) ) ` ( ( D ` F ) + ( D ` G ) ) ) = ( ( ( coe1 ` F ) ` ( D ` F ) ) ( .r ` R ) ( ( coe1 ` G ) ` ( D ` G ) ) ) )
33 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
34 eqid 
 |-  ( coe1 ` G ) = ( coe1 ` G )
35 1 2 6 4 33 34 deg1ldg 
 |-  ( ( R e. Ring /\ G e. B /\ G =/= .0. ) -> ( ( coe1 ` G ) ` ( D ` G ) ) =/= ( 0g ` R ) )
36 7 11 12 35 syl3anc 
 |-  ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) =/= ( 0g ` R ) )
37 eqid 
 |-  ( Base ` R ) = ( Base ` R )
38 34 4 2 37 coe1f 
 |-  ( G e. B -> ( coe1 ` G ) : NN0 --> ( Base ` R ) )
39 11 38 syl 
 |-  ( ph -> ( coe1 ` G ) : NN0 --> ( Base ` R ) )
40 39 22 ffvelcdmd 
 |-  ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) e. ( Base ` R ) )
41 3 37 31 33 rrgeq0i 
 |-  ( ( ( ( coe1 ` F ) ` ( D ` F ) ) e. E /\ ( ( coe1 ` G ) ` ( D ` G ) ) e. ( Base ` R ) ) -> ( ( ( ( coe1 ` F ) ` ( D ` F ) ) ( .r ` R ) ( ( coe1 ` G ) ` ( D ` G ) ) ) = ( 0g ` R ) -> ( ( coe1 ` G ) ` ( D ` G ) ) = ( 0g ` R ) ) )
42 10 40 41 syl2anc 
 |-  ( ph -> ( ( ( ( coe1 ` F ) ` ( D ` F ) ) ( .r ` R ) ( ( coe1 ` G ) ` ( D ` G ) ) ) = ( 0g ` R ) -> ( ( coe1 ` G ) ` ( D ` G ) ) = ( 0g ` R ) ) )
43 42 necon3d 
 |-  ( ph -> ( ( ( coe1 ` G ) ` ( D ` G ) ) =/= ( 0g ` R ) -> ( ( ( coe1 ` F ) ` ( D ` F ) ) ( .r ` R ) ( ( coe1 ` G ) ` ( D ` G ) ) ) =/= ( 0g ` R ) ) )
44 36 43 mpd 
 |-  ( ph -> ( ( ( coe1 ` F ) ` ( D ` F ) ) ( .r ` R ) ( ( coe1 ` G ) ` ( D ` G ) ) ) =/= ( 0g ` R ) )
45 32 44 eqnetrd 
 |-  ( ph -> ( ( coe1 ` ( F .x. G ) ) ` ( ( D ` F ) + ( D ` G ) ) ) =/= ( 0g ` R ) )
46 eqid 
 |-  ( coe1 ` ( F .x. G ) ) = ( coe1 ` ( F .x. G ) )
47 1 2 4 33 46 deg1ge 
 |-  ( ( ( F .x. G ) e. B /\ ( ( D ` F ) + ( D ` G ) ) e. NN0 /\ ( ( coe1 ` ( F .x. G ) ) ` ( ( D ` F ) + ( D ` G ) ) ) =/= ( 0g ` R ) ) -> ( ( D ` F ) + ( D ` G ) ) <_ ( D ` ( F .x. G ) ) )
48 16 23 45 47 syl3anc 
 |-  ( ph -> ( ( D ` F ) + ( D ` G ) ) <_ ( D ` ( F .x. G ) ) )
49 18 25 30 48 xrletrid 
 |-  ( ph -> ( D ` ( F .x. G ) ) = ( ( D ` F ) + ( D ` G ) ) )