Step |
Hyp |
Ref |
Expression |
1 |
|
plyf |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ ) |
2 |
1
|
adantl |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 : ℂ ⟶ ℂ ) |
3 |
2
|
feqmptd |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 = ( 𝑎 ∈ ℂ ↦ ( 𝐹 ‘ 𝑎 ) ) ) |
4 |
|
simplr |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑎 ∈ ℂ ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) ) |
5 |
|
dgrcl |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 ) |
6 |
5
|
adantl |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ 𝐹 ) ∈ ℕ0 ) |
7 |
6
|
nn0zd |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ 𝐹 ) ∈ ℤ ) |
8 |
7
|
adantr |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑎 ∈ ℂ ) → ( deg ‘ 𝐹 ) ∈ ℤ ) |
9 |
|
uzid |
⊢ ( ( deg ‘ 𝐹 ) ∈ ℤ → ( deg ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( deg ‘ 𝐹 ) ) ) |
10 |
|
peano2uz |
⊢ ( ( deg ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( deg ‘ 𝐹 ) ) → ( ( deg ‘ 𝐹 ) + 1 ) ∈ ( ℤ≥ ‘ ( deg ‘ 𝐹 ) ) ) |
11 |
8 9 10
|
3syl |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑎 ∈ ℂ ) → ( ( deg ‘ 𝐹 ) + 1 ) ∈ ( ℤ≥ ‘ ( deg ‘ 𝐹 ) ) ) |
12 |
|
simpr |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑎 ∈ ℂ ) → 𝑎 ∈ ℂ ) |
13 |
|
eqid |
⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 ) |
14 |
|
eqid |
⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 ) |
15 |
13 14
|
coeid3 |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ ( ( deg ‘ 𝐹 ) + 1 ) ∈ ( ℤ≥ ‘ ( deg ‘ 𝐹 ) ) ∧ 𝑎 ∈ ℂ ) → ( 𝐹 ‘ 𝑎 ) = Σ 𝑏 ∈ ( 0 ... ( ( deg ‘ 𝐹 ) + 1 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑏 ) · ( 𝑎 ↑ 𝑏 ) ) ) |
16 |
4 11 12 15
|
syl3anc |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑎 ∈ ℂ ) → ( 𝐹 ‘ 𝑎 ) = Σ 𝑏 ∈ ( 0 ... ( ( deg ‘ 𝐹 ) + 1 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑏 ) · ( 𝑎 ↑ 𝑏 ) ) ) |
17 |
16
|
mpteq2dva |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝑎 ∈ ℂ ↦ ( 𝐹 ‘ 𝑎 ) ) = ( 𝑎 ∈ ℂ ↦ Σ 𝑏 ∈ ( 0 ... ( ( deg ‘ 𝐹 ) + 1 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑏 ) · ( 𝑎 ↑ 𝑏 ) ) ) ) |
18 |
3 17
|
eqtrd |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → 𝐹 = ( 𝑎 ∈ ℂ ↦ Σ 𝑏 ∈ ( 0 ... ( ( deg ‘ 𝐹 ) + 1 ) ) ( ( ( coeff ‘ 𝐹 ) ‘ 𝑏 ) · ( 𝑎 ↑ 𝑏 ) ) ) ) |
19 |
6
|
nn0cnd |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ 𝐹 ) ∈ ℂ ) |
20 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
21 |
|
pncan |
⊢ ( ( ( deg ‘ 𝐹 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( deg ‘ 𝐹 ) + 1 ) − 1 ) = ( deg ‘ 𝐹 ) ) |
22 |
19 20 21
|
sylancl |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ( deg ‘ 𝐹 ) + 1 ) − 1 ) = ( deg ‘ 𝐹 ) ) |
23 |
22
|
eqcomd |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ 𝐹 ) = ( ( ( deg ‘ 𝐹 ) + 1 ) − 1 ) ) |
24 |
23
|
oveq2d |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( 0 ... ( deg ‘ 𝐹 ) ) = ( 0 ... ( ( ( deg ‘ 𝐹 ) + 1 ) − 1 ) ) ) |
25 |
24
|
sumeq1d |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → Σ 𝑏 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( 𝑐 ∈ ℕ0 ↦ ( ( 𝑐 + 1 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) ) ) ‘ 𝑏 ) · ( 𝑎 ↑ 𝑏 ) ) = Σ 𝑏 ∈ ( 0 ... ( ( ( deg ‘ 𝐹 ) + 1 ) − 1 ) ) ( ( ( 𝑐 ∈ ℕ0 ↦ ( ( 𝑐 + 1 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) ) ) ‘ 𝑏 ) · ( 𝑎 ↑ 𝑏 ) ) ) |
26 |
25
|
mpteq2dv |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝑎 ∈ ℂ ↦ Σ 𝑏 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( 𝑐 ∈ ℕ0 ↦ ( ( 𝑐 + 1 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) ) ) ‘ 𝑏 ) · ( 𝑎 ↑ 𝑏 ) ) ) = ( 𝑎 ∈ ℂ ↦ Σ 𝑏 ∈ ( 0 ... ( ( ( deg ‘ 𝐹 ) + 1 ) − 1 ) ) ( ( ( 𝑐 ∈ ℕ0 ↦ ( ( 𝑐 + 1 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) ) ) ‘ 𝑏 ) · ( 𝑎 ↑ 𝑏 ) ) ) ) |
27 |
13
|
coef3 |
⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ ) |
28 |
27
|
adantl |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℂ ) |
29 |
|
oveq1 |
⊢ ( 𝑐 = 𝑏 → ( 𝑐 + 1 ) = ( 𝑏 + 1 ) ) |
30 |
|
fvoveq1 |
⊢ ( 𝑐 = 𝑏 → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) = ( ( coeff ‘ 𝐹 ) ‘ ( 𝑏 + 1 ) ) ) |
31 |
29 30
|
oveq12d |
⊢ ( 𝑐 = 𝑏 → ( ( 𝑐 + 1 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) ) = ( ( 𝑏 + 1 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑏 + 1 ) ) ) ) |
32 |
31
|
cbvmptv |
⊢ ( 𝑐 ∈ ℕ0 ↦ ( ( 𝑐 + 1 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) ) ) = ( 𝑏 ∈ ℕ0 ↦ ( ( 𝑏 + 1 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑏 + 1 ) ) ) ) |
33 |
|
peano2nn0 |
⊢ ( ( deg ‘ 𝐹 ) ∈ ℕ0 → ( ( deg ‘ 𝐹 ) + 1 ) ∈ ℕ0 ) |
34 |
6 33
|
syl |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( deg ‘ 𝐹 ) + 1 ) ∈ ℕ0 ) |
35 |
18 26 28 32 34
|
dvply1 |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ℂ D 𝐹 ) = ( 𝑎 ∈ ℂ ↦ Σ 𝑏 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( 𝑐 ∈ ℕ0 ↦ ( ( 𝑐 + 1 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) ) ) ‘ 𝑏 ) · ( 𝑎 ↑ 𝑏 ) ) ) ) |
36 |
|
cnfldbas |
⊢ ℂ = ( Base ‘ ℂfld ) |
37 |
36
|
subrgss |
⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 𝑆 ⊆ ℂ ) |
38 |
37
|
adantr |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → 𝑆 ⊆ ℂ ) |
39 |
|
elfznn0 |
⊢ ( 𝑏 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) → 𝑏 ∈ ℕ0 ) |
40 |
|
simpll |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℕ0 ) → 𝑆 ∈ ( SubRing ‘ ℂfld ) ) |
41 |
|
zsssubrg |
⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → ℤ ⊆ 𝑆 ) |
42 |
41
|
ad2antrr |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℕ0 ) → ℤ ⊆ 𝑆 ) |
43 |
|
peano2nn0 |
⊢ ( 𝑐 ∈ ℕ0 → ( 𝑐 + 1 ) ∈ ℕ0 ) |
44 |
43
|
adantl |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℕ0 ) → ( 𝑐 + 1 ) ∈ ℕ0 ) |
45 |
44
|
nn0zd |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℕ0 ) → ( 𝑐 + 1 ) ∈ ℤ ) |
46 |
42 45
|
sseldd |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℕ0 ) → ( 𝑐 + 1 ) ∈ 𝑆 ) |
47 |
|
simplr |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℕ0 ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) ) |
48 |
|
subrgsubg |
⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 𝑆 ∈ ( SubGrp ‘ ℂfld ) ) |
49 |
|
cnfld0 |
⊢ 0 = ( 0g ‘ ℂfld ) |
50 |
49
|
subg0cl |
⊢ ( 𝑆 ∈ ( SubGrp ‘ ℂfld ) → 0 ∈ 𝑆 ) |
51 |
48 50
|
syl |
⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 0 ∈ 𝑆 ) |
52 |
51
|
ad2antrr |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℕ0 ) → 0 ∈ 𝑆 ) |
53 |
13
|
coef2 |
⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 0 ∈ 𝑆 ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ 𝑆 ) |
54 |
47 52 53
|
syl2anc |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℕ0 ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ 𝑆 ) |
55 |
54 44
|
ffvelrnd |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) ∈ 𝑆 ) |
56 |
|
cnfldmul |
⊢ · = ( .r ‘ ℂfld ) |
57 |
56
|
subrgmcl |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑐 + 1 ) ∈ 𝑆 ∧ ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) ∈ 𝑆 ) → ( ( 𝑐 + 1 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) ) ∈ 𝑆 ) |
58 |
40 46 55 57
|
syl3anc |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑐 ∈ ℕ0 ) → ( ( 𝑐 + 1 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) ) ∈ 𝑆 ) |
59 |
58
|
fmpttd |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝑐 ∈ ℕ0 ↦ ( ( 𝑐 + 1 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) ) ) : ℕ0 ⟶ 𝑆 ) |
60 |
59
|
ffvelrnda |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑏 ∈ ℕ0 ) → ( ( 𝑐 ∈ ℕ0 ↦ ( ( 𝑐 + 1 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) ) ) ‘ 𝑏 ) ∈ 𝑆 ) |
61 |
39 60
|
sylan2 |
⊢ ( ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝑏 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ) → ( ( 𝑐 ∈ ℕ0 ↦ ( ( 𝑐 + 1 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) ) ) ‘ 𝑏 ) ∈ 𝑆 ) |
62 |
38 6 61
|
elplyd |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝑎 ∈ ℂ ↦ Σ 𝑏 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( ( 𝑐 ∈ ℕ0 ↦ ( ( 𝑐 + 1 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑐 + 1 ) ) ) ) ‘ 𝑏 ) · ( 𝑎 ↑ 𝑏 ) ) ) ∈ ( Poly ‘ 𝑆 ) ) |
63 |
35 62
|
eqeltrd |
⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ℂ D 𝐹 ) ∈ ( Poly ‘ 𝑆 ) ) |