| Step | Hyp | Ref
| Expression |
| 1 | | plycjlem.2 |
. . 3
⊢ 𝐺 = ((∗ ∘ 𝐹) ∘
∗) |
| 2 | | cjcl 15144 |
. . . . 5
⊢ (𝑧 ∈ ℂ →
(∗‘𝑧) ∈
ℂ) |
| 3 | 2 | adantl 481 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) → (∗‘𝑧) ∈
ℂ) |
| 4 | | cjf 15143 |
. . . . . 6
⊢
∗:ℂ⟶ℂ |
| 5 | 4 | a1i 11 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) →
∗:ℂ⟶ℂ) |
| 6 | 5 | feqmptd 6977 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → ∗ = (𝑧 ∈ ℂ ↦
(∗‘𝑧))) |
| 7 | | fzfid 14014 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑥 ∈ ℂ) → (0...𝑁) ∈ Fin) |
| 8 | | plycjlem.3 |
. . . . . . . . . 10
⊢ 𝐴 = (coeff‘𝐹) |
| 9 | 8 | coef3 26271 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐴:ℕ0⟶ℂ) |
| 10 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑥 ∈ ℂ) → 𝐴:ℕ0⟶ℂ) |
| 11 | | elfznn0 13660 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
| 12 | | ffvelcdm 7101 |
. . . . . . . 8
⊢ ((𝐴:ℕ0⟶ℂ ∧
𝑘 ∈
ℕ0) → (𝐴‘𝑘) ∈ ℂ) |
| 13 | 10, 11, 12 | syl2an 596 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ) |
| 14 | | expcl 14120 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑥↑𝑘) ∈
ℂ) |
| 15 | 11, 14 | sylan2 593 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑘 ∈ (0...𝑁)) → (𝑥↑𝑘) ∈ ℂ) |
| 16 | 15 | adantll 714 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑥↑𝑘) ∈ ℂ) |
| 17 | 13, 16 | mulcld 11281 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ) |
| 18 | 7, 17 | fsumcl 15769 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑥 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘)) ∈ ℂ) |
| 19 | | plycjlem.1 |
. . . . . 6
⊢ 𝑁 = (deg‘𝐹) |
| 20 | 8, 19 | coeid 26277 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘)))) |
| 21 | | fveq2 6906 |
. . . . 5
⊢ (𝑧 = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘)) → (∗‘𝑧) = (∗‘Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘)))) |
| 22 | 18, 20, 6, 21 | fmptco 7149 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → (∗ ∘ 𝐹) = (𝑥 ∈ ℂ ↦
(∗‘Σ𝑘
∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘))))) |
| 23 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = (∗‘𝑧) → (𝑥↑𝑘) = ((∗‘𝑧)↑𝑘)) |
| 24 | 23 | oveq2d 7447 |
. . . . . 6
⊢ (𝑥 = (∗‘𝑧) → ((𝐴‘𝑘) · (𝑥↑𝑘)) = ((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))) |
| 25 | 24 | sumeq2sdv 15739 |
. . . . 5
⊢ (𝑥 = (∗‘𝑧) → Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘)) = Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))) |
| 26 | 25 | fveq2d 6910 |
. . . 4
⊢ (𝑥 = (∗‘𝑧) →
(∗‘Σ𝑘
∈ (0...𝑁)((𝐴‘𝑘) · (𝑥↑𝑘))) = (∗‘Σ𝑘 ∈ (0...𝑁)((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘)))) |
| 27 | 3, 6, 22, 26 | fmptco 7149 |
. . 3
⊢ (𝐹 ∈ (Poly‘𝑆) → ((∗ ∘
𝐹) ∘ ∗) =
(𝑧 ∈ ℂ ↦
(∗‘Σ𝑘
∈ (0...𝑁)((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))))) |
| 28 | 1, 27 | eqtrid 2789 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐺 = (𝑧 ∈ ℂ ↦
(∗‘Σ𝑘
∈ (0...𝑁)((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))))) |
| 29 | | fzfid 14014 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) → (0...𝑁) ∈ Fin) |
| 30 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) → 𝐴:ℕ0⟶ℂ) |
| 31 | 30, 11, 12 | syl2an 596 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐴‘𝑘) ∈ ℂ) |
| 32 | | expcl 14120 |
. . . . . . 7
⊢
(((∗‘𝑧)
∈ ℂ ∧ 𝑘
∈ ℕ0) → ((∗‘𝑧)↑𝑘) ∈ ℂ) |
| 33 | 3, 11, 32 | syl2an 596 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((∗‘𝑧)↑𝑘) ∈ ℂ) |
| 34 | 31, 33 | mulcld 11281 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘)) ∈ ℂ) |
| 35 | 29, 34 | fsumcj 15846 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) →
(∗‘Σ𝑘
∈ (0...𝑁)((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))) = Σ𝑘 ∈ (0...𝑁)(∗‘((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘)))) |
| 36 | 31, 33 | cjmuld 15260 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (∗‘((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))) = ((∗‘(𝐴‘𝑘)) ·
(∗‘((∗‘𝑧)↑𝑘)))) |
| 37 | | fvco3 7008 |
. . . . . . . 8
⊢ ((𝐴:ℕ0⟶ℂ ∧
𝑘 ∈
ℕ0) → ((∗ ∘ 𝐴)‘𝑘) = (∗‘(𝐴‘𝑘))) |
| 38 | 30, 11, 37 | syl2an 596 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((∗ ∘ 𝐴)‘𝑘) = (∗‘(𝐴‘𝑘))) |
| 39 | | cjexp 15189 |
. . . . . . . . 9
⊢
(((∗‘𝑧)
∈ ℂ ∧ 𝑘
∈ ℕ0) → (∗‘((∗‘𝑧)↑𝑘)) = ((∗‘(∗‘𝑧))↑𝑘)) |
| 40 | 3, 11, 39 | syl2an 596 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) →
(∗‘((∗‘𝑧)↑𝑘)) = ((∗‘(∗‘𝑧))↑𝑘)) |
| 41 | | cjcj 15179 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℂ →
(∗‘(∗‘𝑧)) = 𝑧) |
| 42 | 41 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) →
(∗‘(∗‘𝑧)) = 𝑧) |
| 43 | 42 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) →
((∗‘(∗‘𝑧))↑𝑘) = (𝑧↑𝑘)) |
| 44 | 40, 43 | eqtr2d 2778 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑧↑𝑘) = (∗‘((∗‘𝑧)↑𝑘))) |
| 45 | 38, 44 | oveq12d 7449 |
. . . . . 6
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘)) = ((∗‘(𝐴‘𝑘)) ·
(∗‘((∗‘𝑧)↑𝑘)))) |
| 46 | 36, 45 | eqtr4d 2780 |
. . . . 5
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (∗‘((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))) = (((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘))) |
| 47 | 46 | sumeq2dv 15738 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)(∗‘((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))) = Σ𝑘 ∈ (0...𝑁)(((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘))) |
| 48 | 35, 47 | eqtrd 2777 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ) →
(∗‘Σ𝑘
∈ (0...𝑁)((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘))) = Σ𝑘 ∈ (0...𝑁)(((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘))) |
| 49 | 48 | mpteq2dva 5242 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝑧 ∈ ℂ ↦
(∗‘Σ𝑘
∈ (0...𝑁)((𝐴‘𝑘) · ((∗‘𝑧)↑𝑘)))) = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘)))) |
| 50 | 28, 49 | eqtrd 2777 |
1
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((∗ ∘ 𝐴)‘𝑘) · (𝑧↑𝑘)))) |