Theorem coeadd

Description: The coefficient function of a sum is the sum of coefficients. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypotheses	coefv0.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
	coeadd.2	⊢ 𝐵 = ( coeff ‘ 𝐺 )
Assertion	coeadd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( 𝐴 ∘f + 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		coefv0.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
2		coeadd.2	⊢ 𝐵 = ( coeff ‘ 𝐺 )
3		eqid	⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
4		eqid	⊢ ( deg ‘ 𝐺 ) = ( deg ‘ 𝐺 )
5	1 2 3 4	coeaddlem	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( 𝐴 ∘f + 𝐵 ) ∧ ( deg ‘ ( 𝐹 ∘f + 𝐺 ) ) ≤ if ( ( deg ‘ 𝐹 ) ≤ ( deg ‘ 𝐺 ) , ( deg ‘ 𝐺 ) , ( deg ‘ 𝐹 ) ) ) )
6	5	simpld	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( 𝐹 ∘f + 𝐺 ) ) = ( 𝐴 ∘f + 𝐵 ) )