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 − 𝐵 ) ) |