Theorem dgradd

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

	Ref	Expression
Hypotheses	dgradd.1	|- M = ( deg ` F )
	dgradd.2	|- N = ( deg ` G )
Assertion	dgradd	|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` ( F oF + G ) ) <_ if ( M <_ N , N , M ) )

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	coeaddlem	|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( coeff ` ( F oF + G ) ) = ( ( coeff ` F ) oF + ( coeff ` G ) ) /\ ( deg ` ( F oF + G ) ) <_ if ( M <_ N , N , M ) ) )
6	5	simprd	|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( deg ` ( F oF + G ) ) <_ if ( M <_ N , N , M ) )