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−fG=A−fB

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 sselid ⊢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 sselid ⊢F∈Poly⁡S∧G∈Poly⁡S→G∈Poly⁡ℂ
12 plymulcl ⊢ℂ×−1∈Poly⁡ℂ∧G∈Poly⁡ℂ→ℂ×−1×fG∈Poly⁡ℂ
13 9 11 12 sylancr ⊢F∈Poly⁡S∧G∈Poly⁡S→ℂ×−1×fG∈Poly⁡ℂ
14 eqid ⊢coeff⁡ℂ×−1×fG=coeff⁡ℂ×−1×fG
15 1 14 coeadd ⊢F∈Poly⁡ℂ∧ℂ×−1×fG∈Poly⁡ℂ→coeff⁡F+fℂ×−1×fG=A+fcoeff⁡ℂ×−1×fG
16 5 13 15 syl2anc ⊢F∈Poly⁡S∧G∈Poly⁡S→coeff⁡F+fℂ×−1×fG=A+fcoeff⁡ℂ×−1×fG
17 coemulc ⊢−1∈ℂ∧G∈Poly⁡ℂ→coeff⁡ℂ×−1×fG=ℕ0×−1×fcoeff⁡G
18 7 11 17 sylancr ⊢F∈Poly⁡S∧G∈Poly⁡S→coeff⁡ℂ×−1×fG=ℕ0×−1×fcoeff⁡G
19 2 oveq2i ⊢ℕ0×−1×fB=ℕ0×−1×fcoeff⁡G
20 18 19 eqtr4di ⊢F∈Poly⁡S∧G∈Poly⁡S→coeff⁡ℂ×−1×fG=ℕ0×−1×fB
21 20 oveq2d ⊢F∈Poly⁡S∧G∈Poly⁡S→A+fcoeff⁡ℂ×−1×fG=A+fℕ0×−1×fB
22 16 21 eqtrd ⊢F∈Poly⁡S∧G∈Poly⁡S→coeff⁡F+fℂ×−1×fG=A+fℕ0×−1×fB
23 cnex ⊢ℂ∈V
24 plyf ⊢F∈Poly⁡S→F:ℂ⟶ℂ
25 plyf ⊢G∈Poly⁡S→G:ℂ⟶ℂ
26 ofnegsub ⊢ℂ∈V∧F:ℂ⟶ℂ∧G:ℂ⟶ℂ→F+fℂ×−1×fG=F−fG
27 23 24 25 26 mp3an3an ⊢F∈Poly⁡S∧G∈Poly⁡S→F+fℂ×−1×fG=F−fG
28 27 fveq2d ⊢F∈Poly⁡S∧G∈Poly⁡S→coeff⁡F+fℂ×−1×fG=coeff⁡F−fG
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×fB=A−fB
33 29 30 31 32 mp3an3an ⊢F∈Poly⁡S∧G∈Poly⁡S→A+fℕ0×−1×fB=A−fB
34 22 28 33 3eqtr3d ⊢F∈Poly⁡S∧G∈Poly⁡S→coeff⁡F−fG=A−fB