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	⊢ 𝑀 = ( deg ‘ 𝐹 )
	dgradd.2	⊢ 𝑁 = ( deg ‘ 𝐺 )
Assertion	dgradd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		dgradd.1	⊢ 𝑀 = ( deg ‘ 𝐹 )
2		dgradd.2	⊢ 𝑁 = ( deg ‘ 𝐺 )
3		eqid	⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
4		eqid	⊢ ( coeff ‘ 𝐺 ) = ( coeff ‘ 𝐺 )
5	3 4 1 2	coeaddlem	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( ( coeff ‘ 𝐹 ) ∘f + ( coeff ‘ 𝐺 ) ) ∧ ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
6	5	simprd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )