Metamath Proof Explorer


Theorem dvply2g

Description: The derivative of a polynomial with coefficients in a subring is a polynomial with coefficients in the same ring. (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Assertion dvply2g ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ℂ D 𝐹 ) ∈ ( Poly ‘ 𝑆 ) )

Proof

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 ‘ 𝑆 ) )