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=\mathrm{coeff}\left(F\right)$$
	coeadd.2	$$⊢B=\mathrm{coeff}\left(G\right)$$
Assertion	coeadd	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge G\in \mathrm{Poly}\left(S\right)\right)\to \mathrm{coeff}\left(F{+}_{f}G\right)=A{+}_{f}B$$

Proof

Step	Hyp	Ref	Expression
1		coefv0.1	$$⊢A=\mathrm{coeff}\left(F\right)$$
2		coeadd.2	$$⊢B=\mathrm{coeff}\left(G\right)$$
3		eqid	$$⊢\mathrm{deg}\left(F\right)=\mathrm{deg}\left(F\right)$$
4		eqid	$$⊢\mathrm{deg}\left(G\right)=\mathrm{deg}\left(G\right)$$
5	1 2 3 4	coeaddlem	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge G\in \mathrm{Poly}\left(S\right)\right)\to \left(\mathrm{coeff}\left(F{+}_{f}G\right)=A{+}_{f}B\wedge \mathrm{deg}\left(F{+}_{f}G\right)\le if\left(\mathrm{deg}\left(F\right)\le \mathrm{deg}\left(G\right),\mathrm{deg}\left(G\right),\mathrm{deg}\left(F\right)\right)\right)$$
6	5	simpld	$$⊢\left(F\in \mathrm{Poly}\left(S\right)\wedge G\in \mathrm{Poly}\left(S\right)\right)\to \mathrm{coeff}\left(F{+}_{f}G\right)=A{+}_{f}B$$