Step | Hyp | Ref
| Expression |
1 | | plyf 23999 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
2 | 1 | adantl 481 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹:ℂ⟶ℂ) |
3 | 2 | feqmptd 6288 |
. . . 4
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹 = (𝑎 ∈ ℂ ↦ (𝐹‘𝑎))) |
4 | | simplr 807 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → 𝐹 ∈ (Poly‘𝑆)) |
5 | | dgrcl 24034 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
6 | 5 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈
ℕ0) |
7 | 6 | nn0zd 11518 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈ ℤ) |
8 | 7 | adantr 480 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → (deg‘𝐹) ∈
ℤ) |
9 | | uzid 11740 |
. . . . . . 7
⊢
((deg‘𝐹)
∈ ℤ → (deg‘𝐹) ∈
(ℤ≥‘(deg‘𝐹))) |
10 | | peano2uz 11779 |
. . . . . . 7
⊢
((deg‘𝐹)
∈ (ℤ≥‘(deg‘𝐹)) → ((deg‘𝐹) + 1) ∈
(ℤ≥‘(deg‘𝐹))) |
11 | 8, 9, 10 | 3syl 18 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → ((deg‘𝐹) + 1) ∈
(ℤ≥‘(deg‘𝐹))) |
12 | | simpr 476 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → 𝑎 ∈ ℂ) |
13 | | eqid 2651 |
. . . . . . 7
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
14 | | eqid 2651 |
. . . . . . 7
⊢
(deg‘𝐹) =
(deg‘𝐹) |
15 | 13, 14 | coeid3 24041 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ ((deg‘𝐹) + 1) ∈
(ℤ≥‘(deg‘𝐹)) ∧ 𝑎 ∈ ℂ) → (𝐹‘𝑎) = Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏))) |
16 | 4, 11, 12, 15 | syl3anc 1366 |
. . . . 5
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → (𝐹‘𝑎) = Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏))) |
17 | 16 | mpteq2dva 4777 |
. . . 4
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑎 ∈ ℂ ↦ (𝐹‘𝑎)) = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏)))) |
18 | 3, 17 | eqtrd 2685 |
. . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹 = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏)))) |
19 | 6 | nn0cnd 11391 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈ ℂ) |
20 | | ax-1cn 10032 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
21 | | pncan 10325 |
. . . . . . . 8
⊢
(((deg‘𝐹)
∈ ℂ ∧ 1 ∈ ℂ) → (((deg‘𝐹) + 1) − 1) = (deg‘𝐹)) |
22 | 19, 20, 21 | sylancl 695 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (((deg‘𝐹) + 1) − 1) = (deg‘𝐹)) |
23 | 22 | eqcomd 2657 |
. . . . . 6
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) = (((deg‘𝐹) + 1) − 1)) |
24 | 23 | oveq2d 6706 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (0...(deg‘𝐹)) = (0...(((deg‘𝐹) + 1) − 1))) |
25 | 24 | sumeq1d 14475 |
. . . 4
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏)) = Σ𝑏 ∈ (0...(((deg‘𝐹) + 1) − 1))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏))) |
26 | 25 | mpteq2dv 4778 |
. . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏))) = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(((deg‘𝐹) + 1) − 1))(((𝑐 ∈ ℕ0
↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏)))) |
27 | 13 | coef3 24033 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) |
28 | 27 | adantl 481 |
. . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (coeff‘𝐹):ℕ0⟶ℂ) |
29 | | oveq1 6697 |
. . . . 5
⊢ (𝑐 = 𝑏 → (𝑐 + 1) = (𝑏 + 1)) |
30 | 29 | fveq2d 6233 |
. . . . 5
⊢ (𝑐 = 𝑏 → ((coeff‘𝐹)‘(𝑐 + 1)) = ((coeff‘𝐹)‘(𝑏 + 1))) |
31 | 29, 30 | oveq12d 6708 |
. . . 4
⊢ (𝑐 = 𝑏 → ((𝑐 + 1) · ((coeff‘𝐹)‘(𝑐 + 1))) = ((𝑏 + 1) · ((coeff‘𝐹)‘(𝑏 + 1)))) |
32 | 31 | cbvmptv 4783 |
. . 3
⊢ (𝑐 ∈ ℕ0
↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1)))) = (𝑏 ∈ ℕ0 ↦ ((𝑏 + 1) ·
((coeff‘𝐹)‘(𝑏 + 1)))) |
33 | | peano2nn0 11371 |
. . . 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 24084 |
. 2
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (ℂ D 𝐹) = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏)))) |
36 | | cnfldbas 19798 |
. . . . 5
⊢ ℂ =
(Base‘ℂfld) |
37 | 36 | subrgss 18829 |
. . . 4
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ⊆ ℂ) |
38 | 37 | adantr 480 |
. . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝑆 ⊆ ℂ) |
39 | | elfznn0 12471 |
. . . 4
⊢ (𝑏 ∈ (0...(deg‘𝐹)) → 𝑏 ∈ ℕ0) |
40 | | simpll 805 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → 𝑆 ∈
(SubRing‘ℂfld)) |
41 | | zsssubrg 19852 |
. . . . . . . . 9
⊢ (𝑆 ∈
(SubRing‘ℂfld) → ℤ ⊆ 𝑆) |
42 | 41 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → ℤ
⊆ 𝑆) |
43 | | peano2nn0 11371 |
. . . . . . . . . 10
⊢ (𝑐 ∈ ℕ0
→ (𝑐 + 1) ∈
ℕ0) |
44 | 43 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → (𝑐 + 1) ∈
ℕ0) |
45 | 44 | nn0zd 11518 |
. . . . . . . 8
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → (𝑐 + 1) ∈
ℤ) |
46 | 42, 45 | sseldd 3637 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → (𝑐 + 1) ∈ 𝑆) |
47 | | simplr 807 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → 𝐹 ∈ (Poly‘𝑆)) |
48 | | subrgsubg 18834 |
. . . . . . . . . . 11
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ∈
(SubGrp‘ℂfld)) |
49 | | cnfld0 19818 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘ℂfld) |
50 | 49 | subg0cl 17649 |
. . . . . . . . . . 11
⊢ (𝑆 ∈
(SubGrp‘ℂfld) → 0 ∈ 𝑆) |
51 | 48, 50 | syl 17 |
. . . . . . . . . 10
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 0 ∈ 𝑆) |
52 | 51 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → 0 ∈
𝑆) |
53 | 13 | coef2 24032 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 0 ∈ 𝑆) → (coeff‘𝐹):ℕ0⟶𝑆) |
54 | 47, 52, 53 | syl2anc 694 |
. . . . . . . 8
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) →
(coeff‘𝐹):ℕ0⟶𝑆) |
55 | 54, 44 | ffvelrnd 6400 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) →
((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) |
56 | | cnfldmul 19800 |
. . . . . . . 8
⊢ ·
= (.r‘ℂfld) |
57 | 56 | subrgmcl 18840 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑐 + 1) ∈ 𝑆 ∧ ((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) → ((𝑐 + 1) · ((coeff‘𝐹)‘(𝑐 + 1))) ∈ 𝑆) |
58 | 40, 46, 55, 57 | syl3anc 1366 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))) ∈ 𝑆) |
59 | | eqid 2651 |
. . . . . 6
⊢ (𝑐 ∈ ℕ0
↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1)))) = (𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1)))) |
60 | 58, 59 | fmptd 6425 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1)))):ℕ0⟶𝑆) |
61 | 60 | ffvelrnda 6399 |
. . . 4
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑏 ∈ ℕ0) → ((𝑐 ∈ ℕ0
↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) ∈ 𝑆) |
62 | 39, 61 | sylan2 490 |
. . 3
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑏 ∈ (0...(deg‘𝐹))) → ((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) ∈ 𝑆) |
63 | 38, 6, 62 | elplyd 24003 |
. 2
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏))) ∈ (Poly‘𝑆)) |
64 | 35, 63 | eqeltrd 2730 |
1
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (ℂ D 𝐹) ∈ (Poly‘𝑆)) |