Metamath Proof Explorer

Theorem coesub

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

Ref Expression
Hypotheses coesub.1 ⊢ A = coeff ⁡ F
coesub.2 ⊢ B = coeff ⁡ G
Assertion coesub ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → coeff ⁡ F − f G = A − f B

Proof

Step Hyp Ref Expression
1 coesub.1 ⊢ A = coeff ⁡ F
2 coesub.2 ⊢ B = coeff ⁡ G
3 plyssc ⊢ Poly ⁡ S ⊆ Poly ⁡ ℂ
4 simpl ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → F ∈ Poly ⁡ S
5 3 4 sseldi ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → F ∈ Poly ⁡ ℂ
6 ssid ⊢ ℂ ⊆ ℂ
7 neg1cn ⊢ − 1 ∈ ℂ
8 plyconst ⊢ ℂ ⊆ ℂ ∧ − 1 ∈ ℂ → ℂ × − 1 ∈ Poly ⁡ ℂ
9 6 7 8 mp2an ⊢ ℂ × − 1 ∈ Poly ⁡ ℂ
10 simpr ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → G ∈ Poly ⁡ S
11 3 10 sseldi ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → G ∈ Poly ⁡ ℂ
12 plymulcl ⊢ ℂ × − 1 ∈ Poly ⁡ ℂ ∧ G ∈ Poly ⁡ ℂ → ℂ × − 1 × f G ∈ Poly ⁡ ℂ
13 9 11 12 sylancr ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → ℂ × − 1 × f G ∈ Poly ⁡ ℂ
14 eqid ⊢ coeff ⁡ ℂ × − 1 × f G = coeff ⁡ ℂ × − 1 × f G
15 1 14 coeadd ⊢ F ∈ Poly ⁡ ℂ ∧ ℂ × − 1 × f G ∈ Poly ⁡ ℂ → coeff ⁡ F + f ℂ × − 1 × f G = A + f coeff ⁡ ℂ × − 1 × f G
16 5 13 15 syl2anc ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → coeff ⁡ F + f ℂ × − 1 × f G = A + f coeff ⁡ ℂ × − 1 × f G
17 coemulc ⊢ − 1 ∈ ℂ ∧ G ∈ Poly ⁡ ℂ → coeff ⁡ ℂ × − 1 × f G = ℕ 0 × − 1 × f coeff ⁡ G
18 7 11 17 sylancr ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → coeff ⁡ ℂ × − 1 × f G = ℕ 0 × − 1 × f coeff ⁡ G
19 2 oveq2i ⊢ ℕ 0 × − 1 × f B = ℕ 0 × − 1 × f coeff ⁡ G
20 18 19 eqtr4di ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → coeff ⁡ ℂ × − 1 × f G = ℕ 0 × − 1 × f B
21 20 oveq2d ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → A + f coeff ⁡ ℂ × − 1 × f G = A + f ℕ 0 × − 1 × f B
22 16 21 eqtrd ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → coeff ⁡ F + f ℂ × − 1 × f G = A + f ℕ 0 × − 1 × f B
23 cnex ⊢ ℂ ∈ V
24 plyf ⊢ F ∈ Poly ⁡ S → F : ℂ ⟶ ℂ
25 plyf ⊢ G ∈ Poly ⁡ S → G : ℂ ⟶ ℂ
26 ofnegsub ⊢ ℂ ∈ V ∧ F : ℂ ⟶ ℂ ∧ G : ℂ ⟶ ℂ → F + f ℂ × − 1 × f G = F − f G
27 23 24 25 26 mp3an3an ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → F + f ℂ × − 1 × f G = F − f G
28 27 fveq2d ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → coeff ⁡ F + f ℂ × − 1 × f G = coeff ⁡ F − f G
29 nn0ex ⊢ ℕ 0 ∈ V
30 1 coef3 ⊢ F ∈ Poly ⁡ S → A : ℕ 0 ⟶ ℂ
31 2 coef3 ⊢ G ∈ Poly ⁡ S → B : ℕ 0 ⟶ ℂ
32 ofnegsub ⊢ ℕ 0 ∈ V ∧ A : ℕ 0 ⟶ ℂ ∧ B : ℕ 0 ⟶ ℂ → A + f ℕ 0 × − 1 × f B = A − f B
33 29 30 31 32 mp3an3an ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → A + f ℕ 0 × − 1 × f B = A − f B
34 22 28 33 3eqtr3d ⊢ F ∈ Poly ⁡ S ∧ G ∈ Poly ⁡ S → coeff ⁡ F − f G = A − f B