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