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 A = coeff F
coeadd.2 B = coeff G
Assertion coeadd F Poly S G Poly S coeff F + f G = A + f B

Proof

Step Hyp Ref Expression
1 coefv0.1 A = coeff F
2 coeadd.2 B = coeff G
3 eqid deg F = deg F
4 eqid deg G = deg G
5 1 2 3 4 coeaddlem F Poly S G Poly S coeff F + f G = A + f B deg F + f G if deg F deg G deg G deg F
6 5 simpld F Poly S G Poly S coeff F + f G = A + f B