Metamath Proof Explorer


Theorem dgrmul2

Description: The degree of a product of polynomials is at most 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 dgrmul2
|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( 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 eqid
 |-  ( coeff ` F ) = ( coeff ` F )
4 eqid
 |-  ( coeff ` G ) = ( coeff ` G )
5 3 4 1 2 coemullem
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( coeff ` ( F oF x. G ) ) = ( n e. NN0 |-> sum_ k e. ( 0 ... n ) ( ( ( coeff ` F ) ` k ) x. ( ( coeff ` G ) ` ( n - k ) ) ) ) /\ ( deg ` ( F oF x. G ) ) <_ ( M + N ) ) )
6 5 simprd
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` ( F oF x. G ) ) <_ ( M + N ) )