Step | Hyp | Ref
| Expression |
1 | | plyf 26177 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
2 | 1 | adantl 480 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹:ℂ⟶ℂ) |
3 | 2 | feqmptd 6966 |
. . . 4
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹 = (𝑎 ∈ ℂ ↦ (𝐹‘𝑎))) |
4 | | simplr 767 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → 𝐹 ∈ (Poly‘𝑆)) |
5 | | dgrcl 26212 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
6 | 5 | adantl 480 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈
ℕ0) |
7 | 6 | nn0zd 12617 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈ ℤ) |
8 | 7 | adantr 479 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → (deg‘𝐹) ∈
ℤ) |
9 | | uzid 12870 |
. . . . . . 7
⊢
((deg‘𝐹)
∈ ℤ → (deg‘𝐹) ∈
(ℤ≥‘(deg‘𝐹))) |
10 | | peano2uz 12918 |
. . . . . . 7
⊢
((deg‘𝐹)
∈ (ℤ≥‘(deg‘𝐹)) → ((deg‘𝐹) + 1) ∈
(ℤ≥‘(deg‘𝐹))) |
11 | 8, 9, 10 | 3syl 18 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → ((deg‘𝐹) + 1) ∈
(ℤ≥‘(deg‘𝐹))) |
12 | | simpr 483 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → 𝑎 ∈ ℂ) |
13 | | eqid 2725 |
. . . . . . 7
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
14 | | eqid 2725 |
. . . . . . 7
⊢
(deg‘𝐹) =
(deg‘𝐹) |
15 | 13, 14 | coeid3 26219 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ ((deg‘𝐹) + 1) ∈
(ℤ≥‘(deg‘𝐹)) ∧ 𝑎 ∈ ℂ) → (𝐹‘𝑎) = Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏))) |
16 | 4, 11, 12, 15 | syl3anc 1368 |
. . . . 5
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑎 ∈ ℂ) → (𝐹‘𝑎) = Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏))) |
17 | 16 | mpteq2dva 5249 |
. . . 4
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑎 ∈ ℂ ↦ (𝐹‘𝑎)) = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏)))) |
18 | 3, 17 | eqtrd 2765 |
. . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝐹 = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...((deg‘𝐹) + 1))(((coeff‘𝐹)‘𝑏) · (𝑎↑𝑏)))) |
19 | 6 | nn0cnd 12567 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) ∈ ℂ) |
20 | | ax-1cn 11198 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
21 | | pncan 11498 |
. . . . . . . 8
⊢
(((deg‘𝐹)
∈ ℂ ∧ 1 ∈ ℂ) → (((deg‘𝐹) + 1) − 1) = (deg‘𝐹)) |
22 | 19, 20, 21 | sylancl 584 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (((deg‘𝐹) + 1) − 1) = (deg‘𝐹)) |
23 | 22 | eqcomd 2731 |
. . . . . 6
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (deg‘𝐹) = (((deg‘𝐹) + 1) − 1)) |
24 | 23 | oveq2d 7435 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (0...(deg‘𝐹)) = (0...(((deg‘𝐹) + 1) − 1))) |
25 | 24 | sumeq1d 15683 |
. . . 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 26211 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) |
28 | 27 | adantl 480 |
. . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (coeff‘𝐹):ℕ0⟶ℂ) |
29 | | oveq1 7426 |
. . . . 5
⊢ (𝑐 = 𝑏 → (𝑐 + 1) = (𝑏 + 1)) |
30 | | fvoveq1 7442 |
. . . . 5
⊢ (𝑐 = 𝑏 → ((coeff‘𝐹)‘(𝑐 + 1)) = ((coeff‘𝐹)‘(𝑏 + 1))) |
31 | 29, 30 | oveq12d 7437 |
. . . 4
⊢ (𝑐 = 𝑏 → ((𝑐 + 1) · ((coeff‘𝐹)‘(𝑐 + 1))) = ((𝑏 + 1) · ((coeff‘𝐹)‘(𝑏 + 1)))) |
32 | 31 | cbvmptv 5262 |
. . 3
⊢ (𝑐 ∈ ℕ0
↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1)))) = (𝑏 ∈ ℕ0 ↦ ((𝑏 + 1) ·
((coeff‘𝐹)‘(𝑏 + 1)))) |
33 | | peano2nn0 12545 |
. . . 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 26263 |
. 2
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (ℂ D 𝐹) = (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏)))) |
36 | | cnfldbas 21300 |
. . . . 5
⊢ ℂ =
(Base‘ℂfld) |
37 | 36 | subrgss 20523 |
. . . 4
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ⊆ ℂ) |
38 | 37 | adantr 479 |
. . 3
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → 𝑆 ⊆ ℂ) |
39 | | elfznn0 13629 |
. . . 4
⊢ (𝑏 ∈ (0...(deg‘𝐹)) → 𝑏 ∈ ℕ0) |
40 | | simpll 765 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → 𝑆 ∈
(SubRing‘ℂfld)) |
41 | | zsssubrg 21375 |
. . . . . . . . 9
⊢ (𝑆 ∈
(SubRing‘ℂfld) → ℤ ⊆ 𝑆) |
42 | 41 | ad2antrr 724 |
. . . . . . . 8
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → ℤ
⊆ 𝑆) |
43 | | peano2nn0 12545 |
. . . . . . . . . 10
⊢ (𝑐 ∈ ℕ0
→ (𝑐 + 1) ∈
ℕ0) |
44 | 43 | adantl 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → (𝑐 + 1) ∈
ℕ0) |
45 | 44 | nn0zd 12617 |
. . . . . . . 8
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → (𝑐 + 1) ∈
ℤ) |
46 | 42, 45 | sseldd 3977 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → (𝑐 + 1) ∈ 𝑆) |
47 | | simplr 767 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → 𝐹 ∈ (Poly‘𝑆)) |
48 | | subrgsubg 20528 |
. . . . . . . . . . 11
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 𝑆 ∈
(SubGrp‘ℂfld)) |
49 | | cnfld0 21337 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘ℂfld) |
50 | 49 | subg0cl 19097 |
. . . . . . . . . . 11
⊢ (𝑆 ∈
(SubGrp‘ℂfld) → 0 ∈ 𝑆) |
51 | 48, 50 | syl 17 |
. . . . . . . . . 10
⊢ (𝑆 ∈
(SubRing‘ℂfld) → 0 ∈ 𝑆) |
52 | 51 | ad2antrr 724 |
. . . . . . . . 9
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → 0 ∈
𝑆) |
53 | 13 | coef2 26210 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ 0 ∈ 𝑆) → (coeff‘𝐹):ℕ0⟶𝑆) |
54 | 47, 52, 53 | syl2anc 582 |
. . . . . . . 8
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) →
(coeff‘𝐹):ℕ0⟶𝑆) |
55 | 54, 44 | ffvelcdmd 7094 |
. . . . . . 7
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) →
((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) |
56 | | mpocnfldmul 21303 |
. . . . . . . . 9
⊢ (𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣)) =
(.r‘ℂfld) |
57 | 56 | subrgmcl 20535 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑐 + 1) ∈ 𝑆 ∧ ((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) → ((𝑐 + 1)(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))((coeff‘𝐹)‘(𝑐 + 1))) ∈ 𝑆) |
58 | 37 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆 → 𝑆 ⊆ ℂ)) |
59 | | ssel 3970 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ⊆ ℂ → ((𝑐 + 1) ∈ 𝑆 → (𝑐 + 1) ∈ ℂ)) |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (𝑆 ⊆ ℂ → ((𝑐 + 1) ∈ 𝑆 → (𝑐 + 1) ∈ ℂ))) |
61 | 58, 60 | syld 47 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆 → ((𝑐 + 1) ∈ 𝑆 → (𝑐 + 1) ∈ ℂ))) |
62 | 61 | com23 86 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈
(SubRing‘ℂfld) → ((𝑐 + 1) ∈ 𝑆 → (((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆 → (𝑐 + 1) ∈ ℂ))) |
63 | 62 | 3imp 1108 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑐 + 1) ∈ 𝑆 ∧ ((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) → (𝑐 + 1) ∈ ℂ) |
64 | 37 | a1d 25 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈
(SubRing‘ℂfld) → ((𝑐 + 1) ∈ 𝑆 → 𝑆 ⊆ ℂ)) |
65 | | ssel 3970 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ⊆ ℂ →
(((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆 → ((coeff‘𝐹)‘(𝑐 + 1)) ∈ ℂ)) |
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈
(SubRing‘ℂfld) → (𝑆 ⊆ ℂ → (((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆 → ((coeff‘𝐹)‘(𝑐 + 1)) ∈ ℂ))) |
67 | 64, 66 | syld 47 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈
(SubRing‘ℂfld) → ((𝑐 + 1) ∈ 𝑆 → (((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆 → ((coeff‘𝐹)‘(𝑐 + 1)) ∈ ℂ))) |
68 | 67 | 3imp 1108 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑐 + 1) ∈ 𝑆 ∧ ((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) → ((coeff‘𝐹)‘(𝑐 + 1)) ∈ ℂ) |
69 | 63, 68 | jca 510 |
. . . . . . . . . 10
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑐 + 1) ∈ 𝑆 ∧ ((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) → ((𝑐 + 1) ∈ ℂ ∧
((coeff‘𝐹)‘(𝑐 + 1)) ∈ ℂ)) |
70 | | ovmpot 7582 |
. . . . . . . . . 10
⊢ (((𝑐 + 1) ∈ ℂ ∧
((coeff‘𝐹)‘(𝑐 + 1)) ∈ ℂ) → ((𝑐 + 1)(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))((coeff‘𝐹)‘(𝑐 + 1))) = ((𝑐 + 1) · ((coeff‘𝐹)‘(𝑐 + 1)))) |
71 | 69, 70 | syl 17 |
. . . . . . . . 9
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑐 + 1) ∈ 𝑆 ∧ ((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) → ((𝑐 + 1)(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))((coeff‘𝐹)‘(𝑐 + 1))) = ((𝑐 + 1) · ((coeff‘𝐹)‘(𝑐 + 1)))) |
72 | 71 | eleq1d 2810 |
. . . . . . . 8
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑐 + 1) ∈ 𝑆 ∧ ((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) → (((𝑐 + 1)(𝑢 ∈ ℂ, 𝑣 ∈ ℂ ↦ (𝑢 · 𝑣))((coeff‘𝐹)‘(𝑐 + 1))) ∈ 𝑆 ↔ ((𝑐 + 1) · ((coeff‘𝐹)‘(𝑐 + 1))) ∈ 𝑆)) |
73 | 57, 72 | mpbid 231 |
. . . . . . 7
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ (𝑐 + 1) ∈ 𝑆 ∧ ((coeff‘𝐹)‘(𝑐 + 1)) ∈ 𝑆) → ((𝑐 + 1) · ((coeff‘𝐹)‘(𝑐 + 1))) ∈ 𝑆) |
74 | 40, 46, 55, 73 | syl3anc 1368 |
. . . . . 6
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑐 ∈ ℕ0) → ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))) ∈ 𝑆) |
75 | 74 | fmpttd 7124 |
. . . . 5
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1)))):ℕ0⟶𝑆) |
76 | 75 | ffvelcdmda 7093 |
. . . 4
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑏 ∈ ℕ0) → ((𝑐 ∈ ℕ0
↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) ∈ 𝑆) |
77 | 39, 76 | sylan2 591 |
. . 3
⊢ (((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) ∧ 𝑏 ∈ (0...(deg‘𝐹))) → ((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) ∈ 𝑆) |
78 | 38, 6, 77 | elplyd 26181 |
. 2
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (𝑎 ∈ ℂ ↦ Σ𝑏 ∈ (0...(deg‘𝐹))(((𝑐 ∈ ℕ0 ↦ ((𝑐 + 1) ·
((coeff‘𝐹)‘(𝑐 + 1))))‘𝑏) · (𝑎↑𝑏))) ∈ (Poly‘𝑆)) |
79 | 35, 78 | eqeltrd 2825 |
1
⊢ ((𝑆 ∈
(SubRing‘ℂfld) ∧ 𝐹 ∈ (Poly‘𝑆)) → (ℂ D 𝐹) ∈ (Poly‘𝑆)) |