Metamath Proof Explorer


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