| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → ((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) = ((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘)) |
| 2 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑧↑𝑗) = (𝑧↑𝑘)) |
| 3 | 1, 2 | oveq12d 7449 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗)) = (((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) · (𝑧↑𝑘))) |
| 4 | | nffvmpt1 6917 |
. . . . . . 7
⊢
Ⅎ𝑘((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) |
| 5 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑘
· |
| 6 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑘(𝑧↑𝑗) |
| 7 | 4, 5, 6 | nfov 7461 |
. . . . . 6
⊢
Ⅎ𝑘(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗)) |
| 8 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑗(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) |
| 9 | 3, 7, 8 | cbvsum 15731 |
. . . . 5
⊢
Σ𝑗 ∈
(0...𝑁)(((𝑘 ∈ ℕ0
↦ if(𝑘 ∈
(0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗)) = Σ𝑘 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) |
| 10 | | elfznn0 13660 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
| 11 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...𝑁) → if(𝑘 ∈ (0...𝑁), 𝐴, 0) = 𝐴) |
| 12 | 11 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → if(𝑘 ∈ (0...𝑁), 𝐴, 0) = 𝐴) |
| 13 | | elplyd.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ 𝑆) |
| 14 | 12, 13 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → if(𝑘 ∈ (0...𝑁), 𝐴, 0) ∈ 𝑆) |
| 15 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
↦ if(𝑘 ∈
(0...𝑁), 𝐴, 0)) = (𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0)) |
| 16 | 15 | fvmpt2 7027 |
. . . . . . . . 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 7446 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = (𝐴 · (𝑧↑𝑘))) |
| 20 | 19 | sumeq2dv 15738 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) |
| 21 | 9, 20 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗)) = Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) |
| 22 | 21 | mpteq2dv 5244 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑗 ∈ (0...𝑁)(((𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0))‘𝑗) · (𝑧↑𝑗))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘)))) |
| 23 | | elplyd.1 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
| 24 | | 0cnd 11254 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℂ) |
| 25 | 24 | snssd 4809 |
. . . . 5
⊢ (𝜑 → {0} ⊆
ℂ) |
| 26 | 23, 25 | unssd 4192 |
. . . 4
⊢ (𝜑 → (𝑆 ∪ {0}) ⊆
ℂ) |
| 27 | | elplyd.2 |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 28 | | elun1 4182 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑆 → 𝐴 ∈ (𝑆 ∪ {0})) |
| 29 | 13, 28 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ (𝑆 ∪ {0})) |
| 30 | 29 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ (𝑆 ∪ {0})) |
| 31 | | ssun2 4179 |
. . . . . . . 8
⊢ {0}
⊆ (𝑆 ∪
{0}) |
| 32 | | c0ex 11255 |
. . . . . . . . 9
⊢ 0 ∈
V |
| 33 | 32 | snss 4785 |
. . . . . . . 8
⊢ (0 ∈
(𝑆 ∪ {0}) ↔ {0}
⊆ (𝑆 ∪
{0})) |
| 34 | 31, 33 | mpbir 231 |
. . . . . . 7
⊢ 0 ∈
(𝑆 ∪
{0}) |
| 35 | 34 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ ¬
𝑘 ∈ (0...𝑁)) → 0 ∈ (𝑆 ∪ {0})) |
| 36 | 30, 35 | ifclda 4561 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → if(𝑘 ∈ (0...𝑁), 𝐴, 0) ∈ (𝑆 ∪ {0})) |
| 37 | 36 | fmpttd 7135 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ ℕ0 ↦ if(𝑘 ∈ (0...𝑁), 𝐴, 0)):ℕ0⟶(𝑆 ∪ {0})) |
| 38 | | elplyr 26240 |
. . . 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 2842 |
. 2
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) ∈ (Poly‘(𝑆 ∪ {0}))) |
| 41 | | plyun0 26236 |
. 2
⊢
(Poly‘(𝑆 ∪
{0})) = (Poly‘𝑆) |
| 42 | 40, 41 | eleqtrdi 2851 |
1
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(𝐴 · (𝑧↑𝑘))) ∈ (Poly‘𝑆)) |