Step | Hyp | Ref
| Expression |
1 | | plyf 25712 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
2 | 1 | adantl 483 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹:ℂ⟶ℂ) |
3 | 2 | feqmptd 6961 |
. . . 4
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹 = (𝑎 ∈ ℂ ↦ (𝐹‘𝑎))) |
4 | | simplr 768 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → 𝐹 ∈ (Poly‘𝑆)) |
5 | | dgrcl 25747 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
6 | 5 | adantl 483 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈
ℕ0) |
7 | 6 | nn0zd 12584 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈ ℤ) |
8 | 7 | adantr 482 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → (deg‘𝐹) ∈
ℤ) |
9 | | uzid 12837 |
. . . . . . 7
⊢
((deg‘𝐹)
∈ ℤ → (deg‘𝐹) ∈
(ℤ≥‘(deg‘𝐹))) |
10 | | peano2uz 12885 |
. . . . . . 7
⊢
((deg‘𝐹)
∈ (ℤ≥‘(deg‘𝐹)) → ((deg‘𝐹) + 1) ∈
(ℤ≥‘(deg‘𝐹))) |
11 | 8, 9, 10 | 3syl 18 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → ((deg‘𝐹) + 1) ∈
(ℤ≥‘(deg‘𝐹))) |
12 | | simpr 486 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → 𝑎 ∈ ℂ) |
13 | | eqid 2733 |
. . . . . . 7
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
14 | | eqid 2733 |
. . . . . . 7
⊢
(deg‘𝐹) =
(deg‘𝐹) |
15 | 13, 14 | coeid3 25754 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ ((deg‘𝐹) + 1) ∈
(ℤ≥‘(deg‘𝐹)) ∧ 𝑎 ∈ ℂ) → (𝐹‘𝑎) = Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏))) |
16 | 4, 11, 12, 15 | syl3anc 1372 |
. . . . 5
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → (𝐹‘𝑎) = Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏))) |
17 | 16 | mpteq2dva 5249 |
. . . 4
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑎 ∈ ℂ ↦ (𝐹‘𝑎)) = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏)))) |
18 | 3, 17 | eqtrd 2773 |
. . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹 = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏)))) |
19 | 6 | nn0cnd 12534 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈ ℂ) |
20 | | ax-1cn 11168 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
21 | | pncan 11466 |
. . . . . . . 8
⊢
(((deg‘𝐹)
∈ ℂ ∧ 1 ∈ ℂ) → (((deg‘𝐹) + 1) − 1) = (deg‘𝐹)) |
22 | 19, 20, 21 | sylancl 587 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (((deg‘𝐹) + 1) − 1) = (deg‘𝐹)) |
23 | 22 | eqcomd 2739 |
. . . . . 6
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) = (((deg‘𝐹) + 1) − 1)) |
24 | 23 | oveq2d 7425 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (0...(deg‘𝐹)) = (0...(((deg‘𝐹) + 1) − 1))) |
25 | 24 | sumeq1d 15647 |
. . . 4
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏)) = Σ𝑏 ∈ (0...(((deg‘𝐹) + 1) − 1))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏))) |
26 | 25 | mpteq2dv 5251 |
. . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏))) = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(((deg‘𝐹) + 1) − 1))(((𝑐 ∈ ℕ0
↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏)))) |
27 | 13 | coef3 25746 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) |
28 | 27 | adantl 483 |
. . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (coeff‘𝐹):ℕ0⟶ℂ) |
29 | | oveq1 7416 |
. . . . 5
⊢ (𝑐 = 𝑏 → (𝑐 + 1) = (𝑏 + 1)) |
30 | | fvoveq1 7432 |
. . . . 5
⊢ (𝑐 = 𝑏 → ((coeff‘𝐹)‘(𝑐 + 1)) = ((coeff‘𝐹)‘(𝑏 + 1))) |
31 | 29, 30 | oveq12d 7427 |
. . . 4
⊢ (𝑐 = 𝑏 → ((𝑐 + 1) · ((coeff‘𝐹)‘(𝑐 + 1))) = ((𝑏 + 1) · ((coeff‘𝐹)‘(𝑏 + 1)))) |
32 | 31 | cbvmptv 5262 |
. . 3
⊢ (𝑐 ∈ ℕ0
↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1)))) = (𝑏 ∈ ℕ0 ↦ ((𝑏 + 1) ·
((coeff‘𝐹)‘(𝑏 + 1)))) |
33 | | peano2nn0 12512 |
. . . 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 25797 |
. 2
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (ℂ D 𝐹) = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏)))) |
36 | | cnfldbas 20948 |
. . . . 5
⊢ ℂ =
(Base‘ℂfld) |
37 | 36 | subrgss 20320 |
. . . 4
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ⊆ ℂ) |
38 | 37 | adantr 482 |
. . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝑆 ⊆ ℂ) |
39 | | elfznn0 13594 |
. . . 4
⊢ (𝑏 ∈ (0...(deg‘𝐹)) → 𝑏 ∈ ℕ0) |
40 | | simpll 766 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → 𝑆 ∈
(SubRing‘ℂfld)) |
41 | | zsssubrg 21003 |
. . . . . . . . 9
⊢ (𝑆 ∈
(SubRing‘ℂfld) → ℤ ⊆ 𝑆) |
42 | 41 | ad2antrr 725 |
. . . . . . . 8
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → ℤ
⊆ 𝑆) |
43 | | peano2nn0 12512 |
. . . . . . . . . 10
⊢ (𝑐 ∈ ℕ0
→ (𝑐 + 1) ∈
ℕ0) |
44 | 43 | adantl 483 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → (𝑐 + 1) ∈
ℕ0) |
45 | 44 | nn0zd 12584 |
. . . . . . . 8
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → (𝑐 + 1) ∈
ℤ) |
46 | 42, 45 | sseldd 3984 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → (𝑐 + 1) ∈ 𝑆) |
47 | | simplr 768 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → 𝐹 ∈ (Poly‘𝑆)) |
48 | | subrgsubg 20325 |
. . . . . . . . . . 11
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ∈
(SubGrp‘ℂfld)) |
49 | | cnfld0 20969 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘ℂfld) |
50 | 49 | subg0cl 19014 |
. . . . . . . . . . 11
⊢ (𝑆 ∈
(SubGrp‘ℂfld) → 0 ∈ 𝑆) |
51 | 48, 50 | syl 17 |
. . . . . . . . . 10
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 0 ∈ 𝑆) |
52 | 51 | ad2antrr 725 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → 0 ∈
𝑆) |
53 | 13 | coef2 25745 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 0 ∈ 𝑆) → (coeff‘𝐹):ℕ0⟶𝑆) |
54 | 47, 52, 53 | syl2anc 585 |
. . . . . . . 8
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) →
(coeff‘𝐹):ℕ0⟶𝑆) |
55 | 54, 44 | ffvelcdmd 7088 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) →
((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) |
56 | | cnfldmul 20950 |
. . . . . . . 8
⊢ ·
= (.r‘ℂfld) |
57 | 56 | subrgmcl 20331 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑐 + 1) ∈ 𝑆 ∧ ((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) → ((𝑐 + 1) · ((coeff‘𝐹)‘(𝑐 + 1))) ∈ 𝑆) |
58 | 40, 46, 55, 57 | syl3anc 1372 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))) ∈ 𝑆) |
59 | 58 | fmpttd 7115 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1)))):ℕ0⟶𝑆) |
60 | 59 | ffvelcdmda 7087 |
. . . 4
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑏 ∈ ℕ0) → ((𝑐 ∈ ℕ0
↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) ∈ 𝑆) |
61 | 39, 60 | sylan2 594 |
. . 3
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑏 ∈ (0...(deg‘𝐹))) → ((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) ∈ 𝑆) |
62 | 38, 6, 61 | elplyd 25716 |
. 2
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏))) ∈ (Poly‘𝑆)) |
63 | 35, 62 | eqeltrd 2834 |
1
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (ℂ D 𝐹) ∈ (Poly‘𝑆)) |