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 𝐴 = ( coeff ‘ 𝐹 )
coesub.2 𝐵 = ( coeff ‘ 𝐺 )
Assertion coesub ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( 𝐹f𝐺 ) ) = ( 𝐴f𝐵 ) )

Proof

Step Hyp Ref Expression
1 coesub.1 𝐴 = ( coeff ‘ 𝐹 )
2 coesub.2 𝐵 = ( coeff ‘ 𝐺 )
3 plyssc ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
4 simpl ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
5 3 4 sselid ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
6 ssid ℂ ⊆ ℂ
7 neg1cn - 1 ∈ ℂ
8 plyconst ( ( ℂ ⊆ ℂ ∧ - 1 ∈ ℂ ) → ( ℂ × { - 1 } ) ∈ ( Poly ‘ ℂ ) )
9 6 7 8 mp2an ( ℂ × { - 1 } ) ∈ ( Poly ‘ ℂ )
10 simpr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
11 3 10 sselid ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐺 ∈ ( Poly ‘ ℂ ) )
12 plymulcl ( ( ( ℂ × { - 1 } ) ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( Poly ‘ ℂ ) ) → ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ∈ ( Poly ‘ ℂ ) )
13 9 11 12 sylancr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ∈ ( Poly ‘ ℂ ) )
14 eqid ( coeff ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = ( coeff ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) )
15 1 14 coeadd ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ∈ ( Poly ‘ ℂ ) ) → ( coeff ‘ ( 𝐹f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) ) = ( 𝐴f + ( coeff ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) ) )
16 5 13 15 syl2anc ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( 𝐹f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) ) = ( 𝐴f + ( coeff ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) ) )
17 coemulc ( ( - 1 ∈ ℂ ∧ 𝐺 ∈ ( Poly ‘ ℂ ) ) → ( coeff ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = ( ( ℕ0 × { - 1 } ) ∘f · ( coeff ‘ 𝐺 ) ) )
18 7 11 17 sylancr ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = ( ( ℕ0 × { - 1 } ) ∘f · ( coeff ‘ 𝐺 ) ) )
19 2 oveq2i ( ( ℕ0 × { - 1 } ) ∘f · 𝐵 ) = ( ( ℕ0 × { - 1 } ) ∘f · ( coeff ‘ 𝐺 ) )
20 18 19 eqtr4di ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = ( ( ℕ0 × { - 1 } ) ∘f · 𝐵 ) )
21 20 oveq2d ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐴f + ( coeff ‘ ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) ) = ( 𝐴f + ( ( ℕ0 × { - 1 } ) ∘f · 𝐵 ) ) )
22 16 21 eqtrd ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( 𝐹f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) ) = ( 𝐴f + ( ( ℕ0 × { - 1 } ) ∘f · 𝐵 ) ) )
23 cnex ℂ ∈ V
24 plyf ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
25 plyf ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 : ℂ ⟶ ℂ )
26 ofnegsub ( ( ℂ ∈ V ∧ 𝐹 : ℂ ⟶ ℂ ∧ 𝐺 : ℂ ⟶ ℂ ) → ( 𝐹f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹f𝐺 ) )
27 23 24 25 26 mp3an3an ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹f𝐺 ) )
28 27 fveq2d ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( 𝐹f + ( ( ℂ × { - 1 } ) ∘f · 𝐺 ) ) ) = ( coeff ‘ ( 𝐹f𝐺 ) ) )
29 nn0ex 0 ∈ V
30 1 coef3 ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
31 2 coef3 ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐵 : ℕ0 ⟶ ℂ )
32 ofnegsub ( ( ℕ0 ∈ V ∧ 𝐴 : ℕ0 ⟶ ℂ ∧ 𝐵 : ℕ0 ⟶ ℂ ) → ( 𝐴f + ( ( ℕ0 × { - 1 } ) ∘f · 𝐵 ) ) = ( 𝐴f𝐵 ) )
33 29 30 31 32 mp3an3an ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐴f + ( ( ℕ0 × { - 1 } ) ∘f · 𝐵 ) ) = ( 𝐴f𝐵 ) )
34 22 28 33 3eqtr3d ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ ( 𝐹f𝐺 ) ) = ( 𝐴f𝐵 ) )