Step | Hyp | Ref
| Expression |
1 | | nffvmpt1 6728 |
. . . . . . 7
⊢
Ⅎ𝑘((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) |
2 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑘
· |
3 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑘(𝑧↑𝑗) |
4 | 1, 2, 3 | nfov 7243 |
. . . . . 6
⊢
Ⅎ𝑘(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗)) |
5 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑗(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) |
6 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) = ((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘)) |
7 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑧↑𝑗) = (𝑧↑𝑘)) |
8 | 6, 7 | oveq12d 7231 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗)) = (((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) · (𝑧↑𝑘))) |
9 | 4, 5, 8 | cbvsumi 15261 |
. . . . 5
⊢
Σ𝑗 ∈
(0...𝑁)(((𝑘 ∈ ℕ0
↦ if(𝑘 ∈
(0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗)) = Σ𝑘 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) |
10 | | elfznn0 13205 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
11 | | iftrue 4445 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...𝑁) → if(𝑘 ∈ (0...𝑁), 𝐴, 0) = 𝐴) |
12 | 11 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → if(𝑘 ∈ (0...𝑁), 𝐴, 0) = 𝐴) |
13 | | elplyd.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ 𝑆) |
14 | 12, 13 | eqeltrd 2838 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → if(𝑘 ∈ (0...𝑁), 𝐴, 0) ∈ 𝑆) |
15 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
↦ if(𝑘 ∈
(0...𝑁), 𝐴, 0)) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0)) |
16 | 15 | fvmpt2 6829 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ if(𝑘 ∈
(0...𝑁), 𝐴, 0) ∈ 𝑆) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) = if(𝑘 ∈ (0...𝑁), 𝐴, 0)) |
17 | 10, 14, 16 | syl2an2 686 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) = if(𝑘 ∈ (0...𝑁), 𝐴, 0)) |
18 | 17, 12 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) = 𝐴) |
19 | 18 | oveq1d 7228 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = (𝐴 · (𝑧↑𝑘))) |
20 | 19 | sumeq2dv 15267 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) |
21 | 9, 20 | syl5eq 2790 |
. . . 4
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗)) = Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) |
22 | 21 | mpteq2dv 5151 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘)))) |
23 | | elplyd.1 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
24 | | 0cnd 10826 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℂ) |
25 | 24 | snssd 4722 |
. . . . 5
⊢ (𝜑 → {0} ⊆
ℂ) |
26 | 23, 25 | unssd 4100 |
. . . 4
⊢ (𝜑 → (𝑆 ∪ {0}) ⊆
ℂ) |
27 | | elplyd.2 |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
28 | | elun1 4090 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑆 → 𝐴 ∈ (𝑆 ∪ {0})) |
29 | 13, 28 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ (𝑆 ∪ {0})) |
30 | 29 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ (𝑆 ∪ {0})) |
31 | | ssun2 4087 |
. . . . . . . 8
⊢ {0}
⊆ (𝑆 ∪
{0}) |
32 | | c0ex 10827 |
. . . . . . . . 9
⊢ 0 ∈
V |
33 | 32 | snss 4699 |
. . . . . . . 8
⊢ (0 ∈
(𝑆 ∪ {0}) ↔ {0}
⊆ (𝑆 ∪
{0})) |
34 | 31, 33 | mpbir 234 |
. . . . . . 7
⊢ 0 ∈
(𝑆 ∪
{0}) |
35 | 34 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (0...𝑁)) → 0 ∈ (𝑆 ∪ {0})) |
36 | 30, 35 | ifclda 4474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ∈ (0...𝑁), 𝐴, 0) ∈ (𝑆 ∪ {0})) |
37 | 36 | fmpttd 6932 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0)):ℕ0⟶(𝑆 ∪ {0})) |
38 | | elplyr 25095 |
. . . 4
⊢ (((𝑆 ∪ {0}) ⊆ ℂ
∧ 𝑁 ∈
ℕ0 ∧ (𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0)):ℕ0⟶(𝑆 ∪ {0})) → (𝑧 ∈ ℂ ↦
Σ𝑗 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗))) ∈ (Poly‘(𝑆 ∪ {0}))) |
39 | 26, 27, 37, 38 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗))) ∈ (Poly‘(𝑆 ∪ {0}))) |
40 | 22, 39 | eqeltrrd 2839 |
. 2
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) ∈ (Poly‘(𝑆 ∪ {0}))) |
41 | | plyun0 25091 |
. 2
⊢
(Poly‘(𝑆 ∪
{0})) = (Poly‘𝑆) |
42 | 40, 41 | eleqtrdi 2848 |
1
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) |