This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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