Metamath Proof Explorer

Theorem dgrmul

Description: The degree of a product of nonzero polynomials is the sum of degrees. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses dgradd.1 
|- M = ( deg ` F )
dgradd.2 
|- N = ( deg ` G )
Assertion dgrmul 
|- ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( deg ` ( F oF x. G ) ) = ( M + N ) )

Proof

Step Hyp Ref Expression
1 dgradd.1 
 |-  M = ( deg ` F )
2 dgradd.2 
 |-  N = ( deg ` G )
3 1 2 dgrmul2 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` ( F oF x. G ) ) <_ ( M + N ) )
4 3 ad2ant2r 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( deg ` ( F oF x. G ) ) <_ ( M + N ) )
5 plymulcl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF x. G ) e. ( Poly ` CC ) )
6 5 ad2ant2r 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( F oF x. G ) e. ( Poly ` CC ) )
7 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
8 1 7 eqeltrid 
 |-  ( F e. ( Poly ` S ) -> M e. NN0 )
9 8 ad2antrr 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> M e. NN0 )
10 dgrcl 
 |-  ( G e. ( Poly ` S ) -> ( deg ` G ) e. NN0 )
11 2 10 eqeltrid 
 |-  ( G e. ( Poly ` S ) -> N e. NN0 )
12 11 ad2antrl 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> N e. NN0 )
13 9 12 nn0addcld 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( M + N ) e. NN0 )
14 eqid 
 |-  ( coeff ` F ) = ( coeff ` F )
15 eqid 
 |-  ( coeff ` G ) = ( coeff ` G )
16 14 15 1 2 coemulhi 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( coeff ` ( F oF x. G ) ) ` ( M + N ) ) = ( ( ( coeff ` F ) ` M ) x. ( ( coeff ` G ) ` N ) ) )
17 16 ad2ant2r 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( ( coeff ` ( F oF x. G ) ) ` ( M + N ) ) = ( ( ( coeff ` F ) ` M ) x. ( ( coeff ` G ) ` N ) ) )
18 14 coef3 
 |-  ( F e. ( Poly ` S ) -> ( coeff ` F ) : NN0 --> CC )
19 18 ad2antrr 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( coeff ` F ) : NN0 --> CC )
20 19 9 ffvelrnd 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( ( coeff ` F ) ` M ) e. CC )
21 15 coef3 
 |-  ( G e. ( Poly ` S ) -> ( coeff ` G ) : NN0 --> CC )
22 21 ad2antrl 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( coeff ` G ) : NN0 --> CC )
23 22 12 ffvelrnd 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( ( coeff ` G ) ` N ) e. CC )
24 1 14 dgreq0 
 |-  ( F e. ( Poly ` S ) -> ( F = 0p <-> ( ( coeff ` F ) ` M ) = 0 ) )
25 24 necon3bid 
 |-  ( F e. ( Poly ` S ) -> ( F =/= 0p <-> ( ( coeff ` F ) ` M ) =/= 0 ) )
26 25 biimpa 
 |-  ( ( F e. ( Poly ` S ) /\ F =/= 0p ) -> ( ( coeff ` F ) ` M ) =/= 0 )
27 26 adantr 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( ( coeff ` F ) ` M ) =/= 0 )
28 2 15 dgreq0 
 |-  ( G e. ( Poly ` S ) -> ( G = 0p <-> ( ( coeff ` G ) ` N ) = 0 ) )
29 28 necon3bid 
 |-  ( G e. ( Poly ` S ) -> ( G =/= 0p <-> ( ( coeff ` G ) ` N ) =/= 0 ) )
30 29 biimpa 
 |-  ( ( G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( coeff ` G ) ` N ) =/= 0 )
31 30 adantl 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( ( coeff ` G ) ` N ) =/= 0 )
32 20 23 27 31 mulne0d 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( ( ( coeff ` F ) ` M ) x. ( ( coeff ` G ) ` N ) ) =/= 0 )
33 17 32 eqnetrd 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( ( coeff ` ( F oF x. G ) ) ` ( M + N ) ) =/= 0 )
34 eqid 
 |-  ( coeff ` ( F oF x. G ) ) = ( coeff ` ( F oF x. G ) )
35 eqid 
 |-  ( deg ` ( F oF x. G ) ) = ( deg ` ( F oF x. G ) )
36 34 35 dgrub 
 |-  ( ( ( F oF x. G ) e. ( Poly ` CC ) /\ ( M + N ) e. NN0 /\ ( ( coeff ` ( F oF x. G ) ) ` ( M + N ) ) =/= 0 ) -> ( M + N ) <_ ( deg ` ( F oF x. G ) ) )
37 6 13 33 36 syl3anc 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( M + N ) <_ ( deg ` ( F oF x. G ) ) )
38 dgrcl 
 |-  ( ( F oF x. G ) e. ( Poly ` CC ) -> ( deg ` ( F oF x. G ) ) e. NN0 )
39 6 38 syl 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( deg ` ( F oF x. G ) ) e. NN0 )
40 39 nn0red 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( deg ` ( F oF x. G ) ) e. RR )
41 13 nn0red 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( M + N ) e. RR )
42 40 41 letri3d 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( ( deg ` ( F oF x. G ) ) = ( M + N ) <-> ( ( deg ` ( F oF x. G ) ) <_ ( M + N ) /\ ( M + N ) <_ ( deg ` ( F oF x. G ) ) ) ) )
43 4 37 42 mpbir2and 
 |-  ( ( ( F e. ( Poly ` S ) /\ F =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( deg ` ( F oF x. G ) ) = ( M + N ) )