Step | Hyp | Ref
| Expression |
1 | | plyco.2 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) |
2 | | plyf 23758 |
. . . . 5
⊢ (𝐺 ∈ (Poly‘𝑆) → 𝐺:ℂ⟶ℂ) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺:ℂ⟶ℂ) |
4 | 3 | ffvelrnda 6267 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝐺‘𝑧) ∈ ℂ) |
5 | 3 | feqmptd 6159 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ (𝐺‘𝑧))) |
6 | | plyco.1 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
7 | | eqid 2610 |
. . . . 5
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
8 | | eqid 2610 |
. . . . 5
⊢
(deg‘𝐹) =
(deg‘𝐹) |
9 | 7, 8 | coeid 23798 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · (𝑥↑𝑘)))) |
10 | 6, 9 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · (𝑥↑𝑘)))) |
11 | | oveq1 6556 |
. . . . 5
⊢ (𝑥 = (𝐺‘𝑧) → (𝑥↑𝑘) = ((𝐺‘𝑧)↑𝑘)) |
12 | 11 | oveq2d 6565 |
. . . 4
⊢ (𝑥 = (𝐺‘𝑧) → (((coeff‘𝐹)‘𝑘) · (𝑥↑𝑘)) = (((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) |
13 | 12 | sumeq2sdv 14282 |
. . 3
⊢ (𝑥 = (𝐺‘𝑧) → Σ𝑘 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · (𝑥↑𝑘)) = Σ𝑘 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) |
14 | 4, 5, 10, 13 | fmptco 6303 |
. 2
⊢ (𝜑 → (𝐹 ∘ 𝐺) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)))) |
15 | | dgrcl 23793 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
16 | 6, 15 | syl 17 |
. . 3
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) |
17 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 0 → (0...𝑥) = (0...0)) |
18 | 17 | sumeq1d 14279 |
. . . . . . 7
⊢ (𝑥 = 0 → Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) = Σ𝑘 ∈ (0...0)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) |
19 | 18 | mpteq2dv 4673 |
. . . . . 6
⊢ (𝑥 = 0 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈
(0...0)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)))) |
20 | 19 | eleq1d 2672 |
. . . . 5
⊢ (𝑥 = 0 → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈
(0...0)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆))) |
21 | 20 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 0 → ((𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆)) ↔ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈
(0...0)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆)))) |
22 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑑 → (0...𝑥) = (0...𝑑)) |
23 | 22 | sumeq1d 14279 |
. . . . . . 7
⊢ (𝑥 = 𝑑 → Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) = Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) |
24 | 23 | mpteq2dv 4673 |
. . . . . 6
⊢ (𝑥 = 𝑑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)))) |
25 | 24 | eleq1d 2672 |
. . . . 5
⊢ (𝑥 = 𝑑 → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆))) |
26 | 25 | imbi2d 329 |
. . . 4
⊢ (𝑥 = 𝑑 → ((𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆)) ↔ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆)))) |
27 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = (𝑑 + 1) → (0...𝑥) = (0...(𝑑 + 1))) |
28 | 27 | sumeq1d 14279 |
. . . . . . 7
⊢ (𝑥 = (𝑑 + 1) → Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) = Σ𝑘 ∈ (0...(𝑑 + 1))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) |
29 | 28 | mpteq2dv 4673 |
. . . . . 6
⊢ (𝑥 = (𝑑 + 1) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑑 + 1))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)))) |
30 | 29 | eleq1d 2672 |
. . . . 5
⊢ (𝑥 = (𝑑 + 1) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑑 + 1))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆))) |
31 | 30 | imbi2d 329 |
. . . 4
⊢ (𝑥 = (𝑑 + 1) → ((𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆)) ↔ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑑 + 1))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆)))) |
32 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = (deg‘𝐹) → (0...𝑥) = (0...(deg‘𝐹))) |
33 | 32 | sumeq1d 14279 |
. . . . . . 7
⊢ (𝑥 = (deg‘𝐹) → Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) = Σ𝑘 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) |
34 | 33 | mpteq2dv 4673 |
. . . . . 6
⊢ (𝑥 = (deg‘𝐹) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)))) |
35 | 34 | eleq1d 2672 |
. . . . 5
⊢ (𝑥 = (deg‘𝐹) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆))) |
36 | 35 | imbi2d 329 |
. . . 4
⊢ (𝑥 = (deg‘𝐹) → ((𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑥)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆)) ↔ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆)))) |
37 | | 0z 11265 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
38 | 4 | exp0d 12864 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝐺‘𝑧)↑0) = 1) |
39 | 38 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (((coeff‘𝐹)‘0) · ((𝐺‘𝑧)↑0)) = (((coeff‘𝐹)‘0) · 1)) |
40 | | plybss 23754 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ) |
41 | 6, 40 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
42 | | 0cnd 9912 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ∈
ℂ) |
43 | 42 | snssd 4281 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → {0} ⊆
ℂ) |
44 | 41, 43 | unssd 3751 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆 ∪ {0}) ⊆
ℂ) |
45 | 7 | coef 23790 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶(𝑆 ∪ {0})) |
46 | 6, 45 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (coeff‘𝐹):ℕ0⟶(𝑆 ∪ {0})) |
47 | | 0nn0 11184 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℕ0 |
48 | | ffvelrn 6265 |
. . . . . . . . . . . . . . 15
⊢
(((coeff‘𝐹):ℕ0⟶(𝑆 ∪ {0}) ∧ 0 ∈
ℕ0) → ((coeff‘𝐹)‘0) ∈ (𝑆 ∪ {0})) |
49 | 46, 47, 48 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((coeff‘𝐹)‘0) ∈ (𝑆 ∪ {0})) |
50 | 44, 49 | sseldd 3569 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((coeff‘𝐹)‘0) ∈
ℂ) |
51 | 50 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((coeff‘𝐹)‘0) ∈
ℂ) |
52 | 51 | mulid1d 9936 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (((coeff‘𝐹)‘0) · 1) =
((coeff‘𝐹)‘0)) |
53 | 39, 52 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (((coeff‘𝐹)‘0) · ((𝐺‘𝑧)↑0)) = ((coeff‘𝐹)‘0)) |
54 | 53, 51 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (((coeff‘𝐹)‘0) · ((𝐺‘𝑧)↑0)) ∈ ℂ) |
55 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → ((coeff‘𝐹)‘𝑘) = ((coeff‘𝐹)‘0)) |
56 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → ((𝐺‘𝑧)↑𝑘) = ((𝐺‘𝑧)↑0)) |
57 | 55, 56 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) = (((coeff‘𝐹)‘0) · ((𝐺‘𝑧)↑0))) |
58 | 57 | fsum1 14320 |
. . . . . . . . 9
⊢ ((0
∈ ℤ ∧ (((coeff‘𝐹)‘0) · ((𝐺‘𝑧)↑0)) ∈ ℂ) →
Σ𝑘 ∈
(0...0)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) = (((coeff‘𝐹)‘0) · ((𝐺‘𝑧)↑0))) |
59 | 37, 54, 58 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈
(0...0)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) = (((coeff‘𝐹)‘0) · ((𝐺‘𝑧)↑0))) |
60 | 59, 53 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈
(0...0)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) = ((coeff‘𝐹)‘0)) |
61 | 60 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈
(0...0)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) = (𝑧 ∈ ℂ ↦ ((coeff‘𝐹)‘0))) |
62 | | fconstmpt 5085 |
. . . . . 6
⊢ (ℂ
× {((coeff‘𝐹)‘0)}) = (𝑧 ∈ ℂ ↦ ((coeff‘𝐹)‘0)) |
63 | 61, 62 | syl6eqr 2662 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈
(0...0)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) = (ℂ × {((coeff‘𝐹)‘0)})) |
64 | | plyconst 23766 |
. . . . . . 7
⊢ (((𝑆 ∪ {0}) ⊆ ℂ
∧ ((coeff‘𝐹)‘0) ∈ (𝑆 ∪ {0})) → (ℂ ×
{((coeff‘𝐹)‘0)}) ∈ (Poly‘(𝑆 ∪ {0}))) |
65 | 44, 49, 64 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (ℂ ×
{((coeff‘𝐹)‘0)}) ∈ (Poly‘(𝑆 ∪ {0}))) |
66 | | plyun0 23757 |
. . . . . 6
⊢
(Poly‘(𝑆 ∪
{0})) = (Poly‘𝑆) |
67 | 65, 66 | syl6eleq 2698 |
. . . . 5
⊢ (𝜑 → (ℂ ×
{((coeff‘𝐹)‘0)}) ∈ (Poly‘𝑆)) |
68 | 63, 67 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈
(0...0)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆)) |
69 | | simprr 792 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ∈ ℕ0 ∧ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆))) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆)) |
70 | 44 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → (𝑆 ∪ {0}) ⊆
ℂ) |
71 | | peano2nn0 11210 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ ℕ0
→ (𝑑 + 1) ∈
ℕ0) |
72 | | ffvelrn 6265 |
. . . . . . . . . . . . . 14
⊢
(((coeff‘𝐹):ℕ0⟶(𝑆 ∪ {0}) ∧ (𝑑 + 1) ∈
ℕ0) → ((coeff‘𝐹)‘(𝑑 + 1)) ∈ (𝑆 ∪ {0})) |
73 | 46, 71, 72 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) →
((coeff‘𝐹)‘(𝑑 + 1)) ∈ (𝑆 ∪ {0})) |
74 | | plyconst 23766 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∪ {0}) ⊆ ℂ
∧ ((coeff‘𝐹)‘(𝑑 + 1)) ∈ (𝑆 ∪ {0})) → (ℂ ×
{((coeff‘𝐹)‘(𝑑 + 1))}) ∈ (Poly‘(𝑆 ∪ {0}))) |
75 | 70, 73, 74 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → (ℂ
× {((coeff‘𝐹)‘(𝑑 + 1))}) ∈ (Poly‘(𝑆 ∪ {0}))) |
76 | 75, 66 | syl6eleq 2698 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → (ℂ
× {((coeff‘𝐹)‘(𝑑 + 1))}) ∈ (Poly‘𝑆)) |
77 | | nn0p1nn 11209 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ ℕ0
→ (𝑑 + 1) ∈
ℕ) |
78 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 1 → ((𝐺‘𝑧)↑𝑥) = ((𝐺‘𝑧)↑1)) |
79 | 78 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 1 → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑥)) = (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑1))) |
80 | 79 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 1 → ((𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑥)) ∈ (Poly‘𝑆) ↔ (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑1)) ∈ (Poly‘𝑆))) |
81 | 80 | imbi2d 329 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1 → ((𝜑 → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑥)) ∈ (Poly‘𝑆)) ↔ (𝜑 → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑1)) ∈ (Poly‘𝑆)))) |
82 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑑 → ((𝐺‘𝑧)↑𝑥) = ((𝐺‘𝑧)↑𝑑)) |
83 | 82 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑑 → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑥)) = (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑))) |
84 | 83 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑑 → ((𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑥)) ∈ (Poly‘𝑆) ↔ (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∈ (Poly‘𝑆))) |
85 | 84 | imbi2d 329 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑑 → ((𝜑 → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑥)) ∈ (Poly‘𝑆)) ↔ (𝜑 → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∈ (Poly‘𝑆)))) |
86 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑑 + 1) → ((𝐺‘𝑧)↑𝑥) = ((𝐺‘𝑧)↑(𝑑 + 1))) |
87 | 86 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑑 + 1) → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑥)) = (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑(𝑑 + 1)))) |
88 | 87 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑑 + 1) → ((𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑥)) ∈ (Poly‘𝑆) ↔ (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑(𝑑 + 1))) ∈ (Poly‘𝑆))) |
89 | 88 | imbi2d 329 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑑 + 1) → ((𝜑 → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑥)) ∈ (Poly‘𝑆)) ↔ (𝜑 → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑(𝑑 + 1))) ∈ (Poly‘𝑆)))) |
90 | 4 | exp1d 12865 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ((𝐺‘𝑧)↑1) = (𝐺‘𝑧)) |
91 | 90 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑1)) = (𝑧 ∈ ℂ ↦ (𝐺‘𝑧))) |
92 | 91, 5 | eqtr4d 2647 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑1)) = 𝐺) |
93 | 92, 1 | eqeltrd 2688 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑1)) ∈ (Poly‘𝑆)) |
94 | | simprr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑑 ∈ ℕ ∧ (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∈ (Poly‘𝑆))) → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∈ (Poly‘𝑆)) |
95 | 1 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑑 ∈ ℕ ∧ (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∈ (Poly‘𝑆))) → 𝐺 ∈ (Poly‘𝑆)) |
96 | | plyco.3 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
97 | 96 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑑 ∈ ℕ ∧ (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∈ (Poly‘𝑆))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
98 | | plyco.4 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) |
99 | 98 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑑 ∈ ℕ ∧ (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∈ (Poly‘𝑆))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) |
100 | 94, 95, 97, 99 | plymul 23778 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑑 ∈ ℕ ∧ (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∈ (Poly‘𝑆))) → ((𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∘𝑓 · 𝐺) ∈ (Poly‘𝑆)) |
101 | 100 | expr 641 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ) → ((𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∈ (Poly‘𝑆) → ((𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∘𝑓 · 𝐺) ∈ (Poly‘𝑆))) |
102 | | cnex 9896 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℂ
∈ V |
103 | 102 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ) → ℂ ∈
V) |
104 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺‘𝑧)↑𝑑) ∈ V |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ) ∧ 𝑧 ∈ ℂ) → ((𝐺‘𝑧)↑𝑑) ∈ V) |
106 | 4 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ) ∧ 𝑧 ∈ ℂ) → (𝐺‘𝑧) ∈ ℂ) |
107 | | eqidd 2611 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ) → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) = (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑))) |
108 | 5 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ) → 𝐺 = (𝑧 ∈ ℂ ↦ (𝐺‘𝑧))) |
109 | 103, 105,
106, 107, 108 | offval2 6812 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ) → ((𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∘𝑓 · 𝐺) = (𝑧 ∈ ℂ ↦ (((𝐺‘𝑧)↑𝑑) · (𝐺‘𝑧)))) |
110 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑑 ∈ ℕ → 𝑑 ∈
ℕ0) |
111 | 110 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ) ∧ 𝑧 ∈ ℂ) → 𝑑 ∈ ℕ0) |
112 | 106, 111 | expp1d 12871 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ) ∧ 𝑧 ∈ ℂ) → ((𝐺‘𝑧)↑(𝑑 + 1)) = (((𝐺‘𝑧)↑𝑑) · (𝐺‘𝑧))) |
113 | 112 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ) → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑(𝑑 + 1))) = (𝑧 ∈ ℂ ↦ (((𝐺‘𝑧)↑𝑑) · (𝐺‘𝑧)))) |
114 | 109, 113 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ) → ((𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∘𝑓 · 𝐺) = (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑(𝑑 + 1)))) |
115 | 114 | eleq1d 2672 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ) → (((𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∘𝑓 · 𝐺) ∈ (Poly‘𝑆) ↔ (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑(𝑑 + 1))) ∈ (Poly‘𝑆))) |
116 | 101, 115 | sylibd 228 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ) → ((𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∈ (Poly‘𝑆) → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑(𝑑 + 1))) ∈ (Poly‘𝑆))) |
117 | 116 | expcom 450 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ ℕ → (𝜑 → ((𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∈ (Poly‘𝑆) → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑(𝑑 + 1))) ∈ (Poly‘𝑆)))) |
118 | 117 | a2d 29 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ ℕ → ((𝜑 → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑𝑑)) ∈ (Poly‘𝑆)) → (𝜑 → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑(𝑑 + 1))) ∈ (Poly‘𝑆)))) |
119 | 81, 85, 89, 89, 93, 118 | nnind 10915 |
. . . . . . . . . . . . 13
⊢ ((𝑑 + 1) ∈ ℕ →
(𝜑 → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑(𝑑 + 1))) ∈ (Poly‘𝑆))) |
120 | 77, 119 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈ ℕ0
→ (𝜑 → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑(𝑑 + 1))) ∈ (Poly‘𝑆))) |
121 | 120 | impcom 445 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑(𝑑 + 1))) ∈ (Poly‘𝑆)) |
122 | 96 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
123 | 98 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 · 𝑦) ∈ 𝑆) |
124 | 76, 121, 122, 123 | plymul 23778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → ((ℂ
× {((coeff‘𝐹)‘(𝑑 + 1))}) ∘𝑓 ·
(𝑧 ∈ ℂ ↦
((𝐺‘𝑧)↑(𝑑 + 1)))) ∈ (Poly‘𝑆)) |
125 | 124 | adantrr 749 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ∈ ℕ0 ∧ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆))) → ((ℂ ×
{((coeff‘𝐹)‘(𝑑 + 1))}) ∘𝑓 ·
(𝑧 ∈ ℂ ↦
((𝐺‘𝑧)↑(𝑑 + 1)))) ∈ (Poly‘𝑆)) |
126 | 96 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑑 ∈ ℕ0 ∧ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆))) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥 + 𝑦) ∈ 𝑆) |
127 | 69, 125, 126 | plyadd 23777 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ∈ ℕ0 ∧ (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆))) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∘𝑓 + ((ℂ
× {((coeff‘𝐹)‘(𝑑 + 1))}) ∘𝑓 ·
(𝑧 ∈ ℂ ↦
((𝐺‘𝑧)↑(𝑑 + 1))))) ∈ (Poly‘𝑆)) |
128 | 127 | expr 641 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → ((𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆) → ((𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∘𝑓 + ((ℂ
× {((coeff‘𝐹)‘(𝑑 + 1))}) ∘𝑓 ·
(𝑧 ∈ ℂ ↦
((𝐺‘𝑧)↑(𝑑 + 1))))) ∈ (Poly‘𝑆))) |
129 | 102 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → ℂ
∈ V) |
130 | | sumex 14266 |
. . . . . . . . . . 11
⊢
Σ𝑘 ∈
(0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) ∈ V |
131 | 130 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) →
Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) ∈ V) |
132 | | ovex 6577 |
. . . . . . . . . . 11
⊢
(((coeff‘𝐹)‘(𝑑 + 1)) · ((𝐺‘𝑧)↑(𝑑 + 1))) ∈ V |
133 | 132 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) →
(((coeff‘𝐹)‘(𝑑 + 1)) · ((𝐺‘𝑧)↑(𝑑 + 1))) ∈ V) |
134 | | eqidd 2611 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)))) |
135 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
((coeff‘𝐹)‘(𝑑 + 1)) ∈ V |
136 | 135 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) →
((coeff‘𝐹)‘(𝑑 + 1)) ∈ V) |
137 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ ((𝐺‘𝑧)↑(𝑑 + 1)) ∈ V |
138 | 137 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → ((𝐺‘𝑧)↑(𝑑 + 1)) ∈ V) |
139 | | fconstmpt 5085 |
. . . . . . . . . . . 12
⊢ (ℂ
× {((coeff‘𝐹)‘(𝑑 + 1))}) = (𝑧 ∈ ℂ ↦ ((coeff‘𝐹)‘(𝑑 + 1))) |
140 | 139 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → (ℂ
× {((coeff‘𝐹)‘(𝑑 + 1))}) = (𝑧 ∈ ℂ ↦ ((coeff‘𝐹)‘(𝑑 + 1)))) |
141 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑(𝑑 + 1))) = (𝑧 ∈ ℂ ↦ ((𝐺‘𝑧)↑(𝑑 + 1)))) |
142 | 129, 136,
138, 140, 141 | offval2 6812 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → ((ℂ
× {((coeff‘𝐹)‘(𝑑 + 1))}) ∘𝑓 ·
(𝑧 ∈ ℂ ↦
((𝐺‘𝑧)↑(𝑑 + 1)))) = (𝑧 ∈ ℂ ↦ (((coeff‘𝐹)‘(𝑑 + 1)) · ((𝐺‘𝑧)↑(𝑑 + 1))))) |
143 | 129, 131,
133, 134, 142 | offval2 6812 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → ((𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∘𝑓 + ((ℂ
× {((coeff‘𝐹)‘(𝑑 + 1))}) ∘𝑓 ·
(𝑧 ∈ ℂ ↦
((𝐺‘𝑧)↑(𝑑 + 1))))) = (𝑧 ∈ ℂ ↦ (Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) + (((coeff‘𝐹)‘(𝑑 + 1)) · ((𝐺‘𝑧)↑(𝑑 + 1)))))) |
144 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑑 ∈
ℕ0) |
145 | | nn0uz 11598 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
146 | 144, 145 | syl6eleq 2698 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → 𝑑 ∈
(ℤ≥‘0)) |
147 | 7 | coef3 23792 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) |
148 | 6, 147 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (coeff‘𝐹):ℕ0⟶ℂ) |
149 | 148 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) →
(coeff‘𝐹):ℕ0⟶ℂ) |
150 | | elfznn0 12302 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (0...(𝑑 + 1)) → 𝑘 ∈ ℕ0) |
151 | | ffvelrn 6265 |
. . . . . . . . . . . . 13
⊢
(((coeff‘𝐹):ℕ0⟶ℂ ∧
𝑘 ∈
ℕ0) → ((coeff‘𝐹)‘𝑘) ∈ ℂ) |
152 | 149, 150,
151 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑑 + 1))) → ((coeff‘𝐹)‘𝑘) ∈ ℂ) |
153 | 4 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) → (𝐺‘𝑧) ∈ ℂ) |
154 | | expcl 12740 |
. . . . . . . . . . . . 13
⊢ (((𝐺‘𝑧) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑧)↑𝑘) ∈ ℂ) |
155 | 153, 150,
154 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑑 + 1))) → ((𝐺‘𝑧)↑𝑘) ∈ ℂ) |
156 | 152, 155 | mulcld 9939 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑑 + 1))) → (((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) ∈ ℂ) |
157 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑑 + 1) → ((coeff‘𝐹)‘𝑘) = ((coeff‘𝐹)‘(𝑑 + 1))) |
158 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑑 + 1) → ((𝐺‘𝑧)↑𝑘) = ((𝐺‘𝑧)↑(𝑑 + 1))) |
159 | 157, 158 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑑 + 1) → (((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) = (((coeff‘𝐹)‘(𝑑 + 1)) · ((𝐺‘𝑧)↑(𝑑 + 1)))) |
160 | 146, 156,
159 | fsump1 14329 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ ℕ0) ∧ 𝑧 ∈ ℂ) →
Σ𝑘 ∈ (0...(𝑑 + 1))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) = (Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) + (((coeff‘𝐹)‘(𝑑 + 1)) · ((𝐺‘𝑧)↑(𝑑 + 1))))) |
161 | 160 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...(𝑑 + 1))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) = (𝑧 ∈ ℂ ↦ (Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)) + (((coeff‘𝐹)‘(𝑑 + 1)) · ((𝐺‘𝑧)↑(𝑑 + 1)))))) |
162 | 143, 161 | eqtr4d 2647 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → ((𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∘𝑓 + ((ℂ
× {((coeff‘𝐹)‘(𝑑 + 1))}) ∘𝑓 ·
(𝑧 ∈ ℂ ↦
((𝐺‘𝑧)↑(𝑑 + 1))))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑑 + 1))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘)))) |
163 | 162 | eleq1d 2672 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → (((𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∘𝑓 + ((ℂ
× {((coeff‘𝐹)‘(𝑑 + 1))}) ∘𝑓 ·
(𝑧 ∈ ℂ ↦
((𝐺‘𝑧)↑(𝑑 + 1))))) ∈ (Poly‘𝑆) ↔ (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑑 + 1))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆))) |
164 | 128, 163 | sylibd 228 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ ℕ0) → ((𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑑 + 1))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆))) |
165 | 164 | expcom 450 |
. . . . 5
⊢ (𝑑 ∈ ℕ0
→ (𝜑 → ((𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆) → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑑 + 1))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆)))) |
166 | 165 | a2d 29 |
. . . 4
⊢ (𝑑 ∈ ℕ0
→ ((𝜑 → (𝑧 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑑)(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆)) → (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(𝑑 + 1))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆)))) |
167 | 21, 26, 31, 36, 68, 166 | nn0ind 11348 |
. . 3
⊢
((deg‘𝐹)
∈ ℕ0 → (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆))) |
168 | 16, 167 | mpcom 37 |
. 2
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · ((𝐺‘𝑧)↑𝑘))) ∈ (Poly‘𝑆)) |
169 | 14, 168 | eqeltrd 2688 |
1
⊢ (𝜑 → (𝐹 ∘ 𝐺) ∈ (Poly‘𝑆)) |