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 sseldi ⊢ ( ( 𝐹 ∈ ( 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 sseldi ⊢ ( ( 𝐹 ∈ ( 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 − 𝐵 ) )