| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | plyf 26237 | . . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) | 
| 2 | 1 | adantl 481 | . . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹:ℂ⟶ℂ) | 
| 3 | 2 | feqmptd 6977 | . . . 4
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹 = (𝑎 ∈ ℂ ↦ (𝐹‘𝑎))) | 
| 4 |  | simplr 769 | . . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → 𝐹 ∈ (Poly‘𝑆)) | 
| 5 |  | dgrcl 26272 | . . . . . . . . . 10
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) | 
| 6 | 5 | adantl 481 | . . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈
ℕ0) | 
| 7 | 6 | nn0zd 12639 | . . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈ ℤ) | 
| 8 | 7 | adantr 480 | . . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → (deg‘𝐹) ∈
ℤ) | 
| 9 |  | uzid 12893 | . . . . . . 7
⊢
((deg‘𝐹)
∈ ℤ → (deg‘𝐹) ∈
(ℤ≥‘(deg‘𝐹))) | 
| 10 |  | peano2uz 12943 | . . . . . . 7
⊢
((deg‘𝐹)
∈ (ℤ≥‘(deg‘𝐹)) → ((deg‘𝐹) + 1) ∈
(ℤ≥‘(deg‘𝐹))) | 
| 11 | 8, 9, 10 | 3syl 18 | . . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → ((deg‘𝐹) + 1) ∈
(ℤ≥‘(deg‘𝐹))) | 
| 12 |  | simpr 484 | . . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → 𝑎 ∈ ℂ) | 
| 13 |  | eqid 2737 | . . . . . . 7
⊢
(coeff‘𝐹) =
(coeff‘𝐹) | 
| 14 |  | eqid 2737 | . . . . . . 7
⊢
(deg‘𝐹) =
(deg‘𝐹) | 
| 15 | 13, 14 | coeid3 26279 | . . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ ((deg‘𝐹) + 1) ∈
(ℤ≥‘(deg‘𝐹)) ∧ 𝑎 ∈ ℂ) → (𝐹‘𝑎) = Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏))) | 
| 16 | 4, 11, 12, 15 | syl3anc 1373 | . . . . 5
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → (𝐹‘𝑎) = Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏))) | 
| 17 | 16 | mpteq2dva 5242 | . . . 4
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑎 ∈ ℂ ↦ (𝐹‘𝑎)) = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏)))) | 
| 18 | 3, 17 | eqtrd 2777 | . . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹 = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏)))) | 
| 19 | 6 | nn0cnd 12589 | . . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈ ℂ) | 
| 20 |  | ax-1cn 11213 | . . . . . . . 8
⊢ 1 ∈
ℂ | 
| 21 |  | pncan 11514 | . . . . . . . 8
⊢
(((deg‘𝐹)
∈ ℂ ∧ 1 ∈ ℂ) → (((deg‘𝐹) + 1) − 1) = (deg‘𝐹)) | 
| 22 | 19, 20, 21 | sylancl 586 | . . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (((deg‘𝐹) + 1) − 1) = (deg‘𝐹)) | 
| 23 | 22 | eqcomd 2743 | . . . . . 6
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) = (((deg‘𝐹) + 1) − 1)) | 
| 24 | 23 | oveq2d 7447 | . . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (0...(deg‘𝐹)) = (0...(((deg‘𝐹) + 1) − 1))) | 
| 25 | 24 | sumeq1d 15736 | . . . 4
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏)) = Σ𝑏 ∈ (0...(((deg‘𝐹) + 1) − 1))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏))) | 
| 26 | 25 | mpteq2dv 5244 | . . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏))) = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(((deg‘𝐹) + 1) − 1))(((𝑐 ∈ ℕ0
↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏)))) | 
| 27 | 13 | coef3 26271 | . . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) | 
| 28 | 27 | adantl 481 | . . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (coeff‘𝐹):ℕ0⟶ℂ) | 
| 29 |  | oveq1 7438 | . . . . 5
⊢ (𝑐 = 𝑏 → (𝑐 + 1) = (𝑏 + 1)) | 
| 30 |  | fvoveq1 7454 | . . . . 5
⊢ (𝑐 = 𝑏 → ((coeff‘𝐹)‘(𝑐 + 1)) = ((coeff‘𝐹)‘(𝑏 + 1))) | 
| 31 | 29, 30 | oveq12d 7449 | . . . 4
⊢ (𝑐 = 𝑏 → ((𝑐 + 1) · ((coeff‘𝐹)‘(𝑐 + 1))) = ((𝑏 + 1) · ((coeff‘𝐹)‘(𝑏 + 1)))) | 
| 32 | 31 | cbvmptv 5255 | . . 3
⊢ (𝑐 ∈ ℕ0
↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1)))) = (𝑏 ∈ ℕ0 ↦ ((𝑏 + 1) ·
((coeff‘𝐹)‘(𝑏 + 1)))) | 
| 33 |  | peano2nn0 12566 | . . . 4
⊢
((deg‘𝐹)
∈ ℕ0 → ((deg‘𝐹) + 1) ∈
ℕ0) | 
| 34 | 6, 33 | syl 17 | . . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → ((deg‘𝐹) + 1) ∈
ℕ0) | 
| 35 | 18, 26, 28, 32, 34 | dvply1 26325 | . 2
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (ℂ D 𝐹) = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏)))) | 
| 36 |  | cnfldbas 21368 | . . . . 5
⊢ ℂ =
(Base‘ℂfld) | 
| 37 | 36 | subrgss 20572 | . . . 4
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ⊆ ℂ) | 
| 38 | 37 | adantr 480 | . . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝑆 ⊆ ℂ) | 
| 39 |  | elfznn0 13660 | . . . 4
⊢ (𝑏 ∈ (0...(deg‘𝐹)) → 𝑏 ∈ ℕ0) | 
| 40 |  | simpll 767 | . . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → 𝑆 ∈
(SubRing‘ℂfld)) | 
| 41 |  | zsssubrg 21443 | . . . . . . . . 9
⊢ (𝑆 ∈
(SubRing‘ℂfld) → ℤ ⊆ 𝑆) | 
| 42 | 41 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → ℤ
⊆ 𝑆) | 
| 43 |  | peano2nn0 12566 | . . . . . . . . . 10
⊢ (𝑐 ∈ ℕ0
→ (𝑐 + 1) ∈
ℕ0) | 
| 44 | 43 | adantl 481 | . . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → (𝑐 + 1) ∈
ℕ0) | 
| 45 | 44 | nn0zd 12639 | . . . . . . . 8
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → (𝑐 + 1) ∈
ℤ) | 
| 46 | 42, 45 | sseldd 3984 | . . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → (𝑐 + 1) ∈ 𝑆) | 
| 47 |  | simplr 769 | . . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → 𝐹 ∈ (Poly‘𝑆)) | 
| 48 |  | subrgsubg 20577 | . . . . . . . . . . 11
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ∈
(SubGrp‘ℂfld)) | 
| 49 |  | cnfld0 21405 | . . . . . . . . . . . 12
⊢ 0 =
(0g‘ℂfld) | 
| 50 | 49 | subg0cl 19152 | . . . . . . . . . . 11
⊢ (𝑆 ∈
(SubGrp‘ℂfld) → 0 ∈ 𝑆) | 
| 51 | 48, 50 | syl 17 | . . . . . . . . . 10
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 0 ∈ 𝑆) | 
| 52 | 51 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → 0 ∈
𝑆) | 
| 53 | 13 | coef2 26270 | . . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 0 ∈ 𝑆) → (coeff‘𝐹):ℕ0⟶𝑆) | 
| 54 | 47, 52, 53 | syl2anc 584 | . . . . . . . 8
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) →
(coeff‘𝐹):ℕ0⟶𝑆) | 
| 55 | 54, 44 | ffvelcdmd 7105 | . . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) →
((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) | 
| 56 |  | cnfldmul 21372 | . . . . . . . 8
⊢  ·
= (.r‘ℂfld) | 
| 57 | 56 | subrgmcl 20584 | . . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑐 + 1) ∈ 𝑆 ∧ ((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) → ((𝑐 + 1) · ((coeff‘𝐹)‘(𝑐 + 1))) ∈ 𝑆) | 
| 58 | 40, 46, 55, 57 | syl3anc 1373 | . . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))) ∈ 𝑆) | 
| 59 | 58 | fmpttd 7135 | . . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1)))):ℕ0⟶𝑆) | 
| 60 | 59 | ffvelcdmda 7104 | . . . 4
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑏 ∈ ℕ0) → ((𝑐 ∈ ℕ0
↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) ∈ 𝑆) | 
| 61 | 39, 60 | sylan2 593 | . . 3
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑏 ∈ (0...(deg‘𝐹))) → ((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) ∈ 𝑆) | 
| 62 | 38, 6, 61 | elplyd 26241 | . 2
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏))) ∈ (Poly‘𝑆)) | 
| 63 | 35, 62 | eqeltrd 2841 | 1
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (ℂ D 𝐹) ∈ (Poly‘𝑆)) |