Proof of Theorem coesub
Step | Hyp | Ref
| Expression |
1 | | plyssc 23760 |
. . . . 5
⊢
(Poly‘𝑆)
⊆ (Poly‘ℂ) |
2 | | simpl 472 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐹 ∈ (Poly‘𝑆)) |
3 | 1, 2 | sseldi 3566 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐹 ∈
(Poly‘ℂ)) |
4 | | ssid 3587 |
. . . . . 6
⊢ ℂ
⊆ ℂ |
5 | | neg1cn 11001 |
. . . . . 6
⊢ -1 ∈
ℂ |
6 | | plyconst 23766 |
. . . . . 6
⊢ ((ℂ
⊆ ℂ ∧ -1 ∈ ℂ) → (ℂ × {-1}) ∈
(Poly‘ℂ)) |
7 | 4, 5, 6 | mp2an 704 |
. . . . 5
⊢ (ℂ
× {-1}) ∈ (Poly‘ℂ) |
8 | | simpr 476 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐺 ∈ (Poly‘𝑆)) |
9 | 1, 8 | sseldi 3566 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐺 ∈
(Poly‘ℂ)) |
10 | | plymulcl 23781 |
. . . . 5
⊢
(((ℂ × {-1}) ∈ (Poly‘ℂ) ∧ 𝐺 ∈ (Poly‘ℂ))
→ ((ℂ × {-1}) ∘𝑓 · 𝐺) ∈
(Poly‘ℂ)) |
11 | 7, 9, 10 | sylancr 694 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ((ℂ × {-1})
∘𝑓 · 𝐺) ∈
(Poly‘ℂ)) |
12 | | coesub.1 |
. . . . 5
⊢ 𝐴 = (coeff‘𝐹) |
13 | | eqid 2610 |
. . . . 5
⊢
(coeff‘((ℂ × {-1}) ∘𝑓
· 𝐺)) =
(coeff‘((ℂ × {-1}) ∘𝑓 · 𝐺)) |
14 | 12, 13 | coeadd 23811 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℂ)
∧ ((ℂ × {-1}) ∘𝑓 · 𝐺) ∈ (Poly‘ℂ))
→ (coeff‘(𝐹
∘𝑓 + ((ℂ × {-1})
∘𝑓 · 𝐺))) = (𝐴 ∘𝑓 +
(coeff‘((ℂ × {-1}) ∘𝑓 · 𝐺)))) |
15 | 3, 11, 14 | syl2anc 691 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (coeff‘(𝐹 ∘𝑓 + ((ℂ
× {-1}) ∘𝑓 · 𝐺))) = (𝐴 ∘𝑓 +
(coeff‘((ℂ × {-1}) ∘𝑓 · 𝐺)))) |
16 | | coemulc 23815 |
. . . . . 6
⊢ ((-1
∈ ℂ ∧ 𝐺
∈ (Poly‘ℂ)) → (coeff‘((ℂ × {-1})
∘𝑓 · 𝐺)) = ((ℕ0 × {-1})
∘𝑓 · (coeff‘𝐺))) |
17 | 5, 9, 16 | sylancr 694 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (coeff‘((ℂ ×
{-1}) ∘𝑓 · 𝐺)) = ((ℕ0 × {-1})
∘𝑓 · (coeff‘𝐺))) |
18 | | coesub.2 |
. . . . . 6
⊢ 𝐵 = (coeff‘𝐺) |
19 | 18 | oveq2i 6560 |
. . . . 5
⊢
((ℕ0 × {-1}) ∘𝑓 ·
𝐵) = ((ℕ0
× {-1}) ∘𝑓 · (coeff‘𝐺)) |
20 | 17, 19 | syl6eqr 2662 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (coeff‘((ℂ ×
{-1}) ∘𝑓 · 𝐺)) = ((ℕ0 × {-1})
∘𝑓 · 𝐵)) |
21 | 20 | oveq2d 6565 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐴 ∘𝑓 +
(coeff‘((ℂ × {-1}) ∘𝑓 · 𝐺))) = (𝐴 ∘𝑓 +
((ℕ0 × {-1}) ∘𝑓 · 𝐵))) |
22 | 15, 21 | eqtrd 2644 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (coeff‘(𝐹 ∘𝑓 + ((ℂ
× {-1}) ∘𝑓 · 𝐺))) = (𝐴 ∘𝑓 +
((ℕ0 × {-1}) ∘𝑓 · 𝐵))) |
23 | | cnex 9896 |
. . . . 5
⊢ ℂ
∈ V |
24 | 23 | a1i 11 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ℂ ∈ V) |
25 | | plyf 23758 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
26 | 25 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐹:ℂ⟶ℂ) |
27 | | plyf 23758 |
. . . . 5
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐺:ℂ⟶ℂ) |
28 | 27 | adantl 481 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐺:ℂ⟶ℂ) |
29 | | ofnegsub 10895 |
. . . 4
⊢ ((ℂ
∈ V ∧ 𝐹:ℂ⟶ℂ ∧ 𝐺:ℂ⟶ℂ) →
(𝐹
∘𝑓 + ((ℂ × {-1})
∘𝑓 · 𝐺)) = (𝐹 ∘𝑓 − 𝐺)) |
30 | 24, 26, 28, 29 | syl3anc 1318 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐹 ∘𝑓 + ((ℂ
× {-1}) ∘𝑓 · 𝐺)) = (𝐹 ∘𝑓 − 𝐺)) |
31 | 30 | fveq2d 6107 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (coeff‘(𝐹 ∘𝑓 + ((ℂ
× {-1}) ∘𝑓 · 𝐺))) = (coeff‘(𝐹 ∘𝑓 − 𝐺))) |
32 | | nn0ex 11175 |
. . . 4
⊢
ℕ0 ∈ V |
33 | 32 | a1i 11 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → ℕ0 ∈
V) |
34 | 12 | coef3 23792 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ) |
35 | 34 | adantr 480 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐴:ℕ0⟶ℂ) |
36 | 18 | coef3 23792 |
. . . 4
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐵:ℕ0⟶ℂ) |
37 | 36 | adantl 481 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → 𝐵:ℕ0⟶ℂ) |
38 | | ofnegsub 10895 |
. . 3
⊢
((ℕ0 ∈ V ∧ 𝐴:ℕ0⟶ℂ ∧
𝐵:ℕ0⟶ℂ) →
(𝐴
∘𝑓 + ((ℕ0 × {-1})
∘𝑓 · 𝐵)) = (𝐴 ∘𝑓 − 𝐵)) |
39 | 33, 35, 37, 38 | syl3anc 1318 |
. 2
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (𝐴 ∘𝑓 +
((ℕ0 × {-1}) ∘𝑓 · 𝐵)) = (𝐴 ∘𝑓 − 𝐵)) |
40 | 22, 31, 39 | 3eqtr3d 2652 |
1
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐺 ∈ (Poly‘𝑆)) → (coeff‘(𝐹 ∘𝑓 − 𝐺)) = (𝐴 ∘𝑓 − 𝐵)) |