Step | Hyp | Ref
| Expression |
1 | | plyf 25347 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
2 | 1 | adantl 482 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹:ℂ⟶ℂ) |
3 | 2 | feqmptd 6830 |
. . . 4
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹 = (𝑎 ∈ ℂ ↦ (𝐹‘𝑎))) |
4 | | simplr 766 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → 𝐹 ∈ (Poly‘𝑆)) |
5 | | dgrcl 25382 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
6 | 5 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈
ℕ0) |
7 | 6 | nn0zd 12412 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈ ℤ) |
8 | 7 | adantr 481 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → (deg‘𝐹) ∈
ℤ) |
9 | | uzid 12585 |
. . . . . . 7
⊢
((deg‘𝐹)
∈ ℤ → (deg‘𝐹) ∈
(ℤ≥‘(deg‘𝐹))) |
10 | | peano2uz 12629 |
. . . . . . 7
⊢
((deg‘𝐹)
∈ (ℤ≥‘(deg‘𝐹)) → ((deg‘𝐹) + 1) ∈
(ℤ≥‘(deg‘𝐹))) |
11 | 8, 9, 10 | 3syl 18 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → ((deg‘𝐹) + 1) ∈
(ℤ≥‘(deg‘𝐹))) |
12 | | simpr 485 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → 𝑎 ∈ ℂ) |
13 | | eqid 2738 |
. . . . . . 7
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
14 | | eqid 2738 |
. . . . . . 7
⊢
(deg‘𝐹) =
(deg‘𝐹) |
15 | 13, 14 | coeid3 25389 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ ((deg‘𝐹) + 1) ∈
(ℤ≥‘(deg‘𝐹)) ∧ 𝑎 ∈ ℂ) → (𝐹‘𝑎) = Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏))) |
16 | 4, 11, 12, 15 | syl3anc 1370 |
. . . . 5
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → (𝐹‘𝑎) = Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏))) |
17 | 16 | mpteq2dva 5174 |
. . . 4
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑎 ∈ ℂ ↦ (𝐹‘𝑎)) = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏)))) |
18 | 3, 17 | eqtrd 2778 |
. . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹 = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏)))) |
19 | 6 | nn0cnd 12283 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈ ℂ) |
20 | | ax-1cn 10917 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
21 | | pncan 11215 |
. . . . . . . 8
⊢
(((deg‘𝐹)
∈ ℂ ∧ 1 ∈ ℂ) → (((deg‘𝐹) + 1) − 1) = (deg‘𝐹)) |
22 | 19, 20, 21 | sylancl 586 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (((deg‘𝐹) + 1) − 1) = (deg‘𝐹)) |
23 | 22 | eqcomd 2744 |
. . . . . 6
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) = (((deg‘𝐹) + 1) − 1)) |
24 | 23 | oveq2d 7284 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (0...(deg‘𝐹)) = (0...(((deg‘𝐹) + 1) − 1))) |
25 | 24 | sumeq1d 15401 |
. . . 4
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏)) = Σ𝑏 ∈ (0...(((deg‘𝐹) + 1) − 1))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏))) |
26 | 25 | mpteq2dv 5176 |
. . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏))) = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(((deg‘𝐹) + 1) − 1))(((𝑐 ∈ ℕ0
↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏)))) |
27 | 13 | coef3 25381 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) |
28 | 27 | adantl 482 |
. . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (coeff‘𝐹):ℕ0⟶ℂ) |
29 | | oveq1 7275 |
. . . . 5
⊢ (𝑐 = 𝑏 → (𝑐 + 1) = (𝑏 + 1)) |
30 | | fvoveq1 7291 |
. . . . 5
⊢ (𝑐 = 𝑏 → ((coeff‘𝐹)‘(𝑐 + 1)) = ((coeff‘𝐹)‘(𝑏 + 1))) |
31 | 29, 30 | oveq12d 7286 |
. . . 4
⊢ (𝑐 = 𝑏 → ((𝑐 + 1) · ((coeff‘𝐹)‘(𝑐 + 1))) = ((𝑏 + 1) · ((coeff‘𝐹)‘(𝑏 + 1)))) |
32 | 31 | cbvmptv 5187 |
. . 3
⊢ (𝑐 ∈ ℕ0
↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1)))) = (𝑏 ∈ ℕ0 ↦ ((𝑏 + 1) ·
((coeff‘𝐹)‘(𝑏 + 1)))) |
33 | | peano2nn0 12261 |
. . . 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 25432 |
. 2
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (ℂ D 𝐹) = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏)))) |
36 | | cnfldbas 20589 |
. . . . 5
⊢ ℂ =
(Base‘ℂfld) |
37 | 36 | subrgss 20013 |
. . . 4
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ⊆ ℂ) |
38 | 37 | adantr 481 |
. . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝑆 ⊆ ℂ) |
39 | | elfznn0 13337 |
. . . 4
⊢ (𝑏 ∈ (0...(deg‘𝐹)) → 𝑏 ∈ ℕ0) |
40 | | simpll 764 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → 𝑆 ∈
(SubRing‘ℂfld)) |
41 | | zsssubrg 20644 |
. . . . . . . . 9
⊢ (𝑆 ∈
(SubRing‘ℂfld) → ℤ ⊆ 𝑆) |
42 | 41 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → ℤ
⊆ 𝑆) |
43 | | peano2nn0 12261 |
. . . . . . . . . 10
⊢ (𝑐 ∈ ℕ0
→ (𝑐 + 1) ∈
ℕ0) |
44 | 43 | adantl 482 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → (𝑐 + 1) ∈
ℕ0) |
45 | 44 | nn0zd 12412 |
. . . . . . . 8
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → (𝑐 + 1) ∈
ℤ) |
46 | 42, 45 | sseldd 3922 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → (𝑐 + 1) ∈ 𝑆) |
47 | | simplr 766 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → 𝐹 ∈ (Poly‘𝑆)) |
48 | | subrgsubg 20018 |
. . . . . . . . . . 11
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ∈
(SubGrp‘ℂfld)) |
49 | | cnfld0 20610 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘ℂfld) |
50 | 49 | subg0cl 18751 |
. . . . . . . . . . 11
⊢ (𝑆 ∈
(SubGrp‘ℂfld) → 0 ∈ 𝑆) |
51 | 48, 50 | syl 17 |
. . . . . . . . . 10
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 0 ∈ 𝑆) |
52 | 51 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → 0 ∈
𝑆) |
53 | 13 | coef2 25380 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 0 ∈ 𝑆) → (coeff‘𝐹):ℕ0⟶𝑆) |
54 | 47, 52, 53 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) →
(coeff‘𝐹):ℕ0⟶𝑆) |
55 | 54, 44 | ffvelrnd 6955 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) →
((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) |
56 | | cnfldmul 20591 |
. . . . . . . 8
⊢ ·
= (.r‘ℂfld) |
57 | 56 | subrgmcl 20024 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑐 + 1) ∈ 𝑆 ∧ ((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) → ((𝑐 + 1) · ((coeff‘𝐹)‘(𝑐 + 1))) ∈ 𝑆) |
58 | 40, 46, 55, 57 | syl3anc 1370 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))) ∈ 𝑆) |
59 | 58 | fmpttd 6982 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1)))):ℕ0⟶𝑆) |
60 | 59 | ffvelrnda 6954 |
. . . 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 25351 |
. 2
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏))) ∈ (Poly‘𝑆)) |
63 | 35, 62 | eqeltrd 2839 |
1
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (ℂ D 𝐹) ∈ (Poly‘𝑆)) |