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 ) )