Step | Hyp | Ref
| Expression |
1 | | nffvmpt1 6111 |
. . . . . . 7
⊢
Ⅎ𝑘((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) |
2 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑘
· |
3 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑘(𝑧↑𝑗) |
4 | 1, 2, 3 | nfov 6575 |
. . . . . 6
⊢
Ⅎ𝑘(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗)) |
5 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑗(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) |
6 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) = ((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘)) |
7 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑧↑𝑗) = (𝑧↑𝑘)) |
8 | 6, 7 | oveq12d 6567 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗)) = (((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) · (𝑧↑𝑘))) |
9 | 4, 5, 8 | cbvsumi 14275 |
. . . . 5
⊢
Σ𝑗 ∈
(0...𝑁)(((𝑘 ∈ ℕ0
↦ if(𝑘 ∈
(0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗)) = Σ𝑘 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) |
10 | | elfznn0 12302 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
11 | 10 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
12 | | iftrue 4042 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...𝑁) → if(𝑘 ∈ (0...𝑁), 𝐴, 0) = 𝐴) |
13 | 12 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → if(𝑘 ∈ (0...𝑁), 𝐴, 0) = 𝐴) |
14 | | elplyd.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ 𝑆) |
15 | 13, 14 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → if(𝑘 ∈ (0...𝑁), 𝐴, 0) ∈ 𝑆) |
16 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
↦ if(𝑘 ∈
(0...𝑁), 𝐴, 0)) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0)) |
17 | 16 | fvmpt2 6200 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ if(𝑘 ∈
(0...𝑁), 𝐴, 0) ∈ 𝑆) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) = if(𝑘 ∈ (0...𝑁), 𝐴, 0)) |
18 | 11, 15, 17 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) = if(𝑘 ∈ (0...𝑁), 𝐴, 0)) |
19 | 18, 13 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) = 𝐴) |
20 | 19 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = (𝐴 · (𝑧↑𝑘))) |
21 | 20 | sumeq2dv 14281 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) |
22 | 9, 21 | syl5eq 2656 |
. . . 4
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗)) = Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) |
23 | 22 | mpteq2dv 4673 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘)))) |
24 | | elplyd.1 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
25 | | 0cnd 9912 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℂ) |
26 | 25 | snssd 4281 |
. . . . 5
⊢ (𝜑 → {0} ⊆
ℂ) |
27 | 24, 26 | unssd 3751 |
. . . 4
⊢ (𝜑 → (𝑆 ∪ {0}) ⊆
ℂ) |
28 | | elplyd.2 |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
29 | | elun1 3742 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑆 → 𝐴 ∈ (𝑆 ∪ {0})) |
30 | 14, 29 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ (𝑆 ∪ {0})) |
31 | 30 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ (𝑆 ∪ {0})) |
32 | | ssun2 3739 |
. . . . . . . 8
⊢ {0}
⊆ (𝑆 ∪
{0}) |
33 | | c0ex 9913 |
. . . . . . . . 9
⊢ 0 ∈
V |
34 | 33 | snss 4259 |
. . . . . . . 8
⊢ (0 ∈
(𝑆 ∪ {0}) ↔ {0}
⊆ (𝑆 ∪
{0})) |
35 | 32, 34 | mpbir 220 |
. . . . . . 7
⊢ 0 ∈
(𝑆 ∪
{0}) |
36 | 35 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (0...𝑁)) → 0 ∈ (𝑆 ∪ {0})) |
37 | 31, 36 | ifclda 4070 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ∈ (0...𝑁), 𝐴, 0) ∈ (𝑆 ∪ {0})) |
38 | 37, 16 | fmptd 6292 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0)):ℕ0⟶(𝑆 ∪ {0})) |
39 | | elplyr 23761 |
. . . 4
⊢ (((𝑆 ∪ {0}) ⊆ ℂ
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0)):ℕ0⟶(𝑆 ∪ {0})) → (𝑧 ∈ ℂ ↦
Σ𝑗 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗))) ∈ (Poly‘(𝑆 ∪ {0}))) |
40 | 27, 28, 38, 39 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗))) ∈ (Poly‘(𝑆 ∪ {0}))) |
41 | 23, 40 | eqeltrrd 2689 |
. 2
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) ∈ (Poly‘(𝑆 ∪ {0}))) |
42 | | plyun0 23757 |
. 2
⊢
(Poly‘(𝑆 ∪
{0})) = (Poly‘𝑆) |
43 | 41, 42 | syl6eleq 2698 |
1
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) |