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 
|- ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( CC _D F ) e. ( Poly ` S ) )

Proof

Step Hyp Ref Expression
1 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
2 1 adantl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> F : CC --> CC )
3 2 feqmptd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> F = ( a e. CC |-> ( F ` a ) ) )
4 simplr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ a e. CC ) -> F e. ( Poly ` S ) )
5 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
6 5 adantl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( deg ` F ) e. NN0 )
7 6 nn0zd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( deg ` F ) e. ZZ )
8 7 adantr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ a e. CC ) -> ( deg ` F ) e. ZZ )
9 uzid 
 |-  ( ( deg ` F ) e. ZZ -> ( deg ` F ) e. ( ZZ>= ` ( deg ` F ) ) )
10 peano2uz 
 |-  ( ( deg ` F ) e. ( ZZ>= ` ( deg ` F ) ) -> ( ( deg ` F ) + 1 ) e. ( ZZ>= ` ( deg ` F ) ) )
11 8 9 10 3syl 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ a e. CC ) -> ( ( deg ` F ) + 1 ) e. ( ZZ>= ` ( deg ` F ) ) )
12 simpr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ a e. CC ) -> a e. CC )
13 eqid 
 |-  ( coeff ` F ) = ( coeff ` F )
14 eqid 
 |-  ( deg ` F ) = ( deg ` F )
15 13 14 coeid3 
 |-  ( ( F e. ( Poly ` S ) /\ ( ( deg ` F ) + 1 ) e. ( ZZ>= ` ( deg ` F ) ) /\ a e. CC ) -> ( F ` a ) = sum_ b e. ( 0 ... ( ( deg ` F ) + 1 ) ) ( ( ( coeff ` F ) ` b ) x. ( a ^ b ) ) )
16 4 11 12 15 syl3anc 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ a e. CC ) -> ( F ` a ) = sum_ b e. ( 0 ... ( ( deg ` F ) + 1 ) ) ( ( ( coeff ` F ) ` b ) x. ( a ^ b ) ) )
17 16 mpteq2dva 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( a e. CC |-> ( F ` a ) ) = ( a e. CC |-> sum_ b e. ( 0 ... ( ( deg ` F ) + 1 ) ) ( ( ( coeff ` F ) ` b ) x. ( a ^ b ) ) ) )
18 3 17 eqtrd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> F = ( a e. CC |-> sum_ b e. ( 0 ... ( ( deg ` F ) + 1 ) ) ( ( ( coeff ` F ) ` b ) x. ( a ^ b ) ) ) )
19 6 nn0cnd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( deg ` F ) e. CC )
20 ax-1cn 
 |-  1 e. CC
21 pncan 
 |-  ( ( ( deg ` F ) e. CC /\ 1 e. CC ) -> ( ( ( deg ` F ) + 1 ) - 1 ) = ( deg ` F ) )
22 19 20 21 sylancl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( ( deg ` F ) + 1 ) - 1 ) = ( deg ` F ) )
23 22 eqcomd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( deg ` F ) = ( ( ( deg ` F ) + 1 ) - 1 ) )
24 23 oveq2d 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( 0 ... ( deg ` F ) ) = ( 0 ... ( ( ( deg ` F ) + 1 ) - 1 ) ) )
25 24 sumeq1d 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> sum_ b e. ( 0 ... ( deg ` F ) ) ( ( ( c e. NN0 |-> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) ) ` b ) x. ( a ^ b ) ) = sum_ b e. ( 0 ... ( ( ( deg ` F ) + 1 ) - 1 ) ) ( ( ( c e. NN0 |-> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) ) ` b ) x. ( a ^ b ) ) )
26 25 mpteq2dv 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( a e. CC |-> sum_ b e. ( 0 ... ( deg ` F ) ) ( ( ( c e. NN0 |-> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) ) ` b ) x. ( a ^ b ) ) ) = ( a e. CC |-> sum_ b e. ( 0 ... ( ( ( deg ` F ) + 1 ) - 1 ) ) ( ( ( c e. NN0 |-> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) ) ` b ) x. ( a ^ b ) ) ) )
27 13 coef3 
 |-  ( F e. ( Poly ` S ) -> ( coeff ` F ) : NN0 --> CC )
28 27 adantl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( coeff ` F ) : NN0 --> CC )
29 oveq1 
 |-  ( c = b -> ( c + 1 ) = ( b + 1 ) )
30 fvoveq1 
 |-  ( c = b -> ( ( coeff ` F ) ` ( c + 1 ) ) = ( ( coeff ` F ) ` ( b + 1 ) ) )
31 29 30 oveq12d 
 |-  ( c = b -> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) = ( ( b + 1 ) x. ( ( coeff ` F ) ` ( b + 1 ) ) ) )
32 31 cbvmptv 
 |-  ( c e. NN0 |-> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) ) = ( b e. NN0 |-> ( ( b + 1 ) x. ( ( coeff ` F ) ` ( b + 1 ) ) ) )
33 peano2nn0 
 |-  ( ( deg ` F ) e. NN0 -> ( ( deg ` F ) + 1 ) e. NN0 )
34 6 33 syl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( deg ` F ) + 1 ) e. NN0 )
35 18 26 28 32 34 dvply1 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( CC _D F ) = ( a e. CC |-> sum_ b e. ( 0 ... ( deg ` F ) ) ( ( ( c e. NN0 |-> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) ) ` b ) x. ( a ^ b ) ) ) )
36 cnfldbas 
 |-  CC = ( Base ` CCfld )
37 36 subrgss 
 |-  ( S e. ( SubRing ` CCfld ) -> S C_ CC )
38 37 adantr 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> S C_ CC )
39 elfznn0 
 |-  ( b e. ( 0 ... ( deg ` F ) ) -> b e. NN0 )
40 simpll 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ c e. NN0 ) -> S e. ( SubRing ` CCfld ) )
41 zsssubrg 
 |-  ( S e. ( SubRing ` CCfld ) -> ZZ C_ S )
42 41 ad2antrr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ c e. NN0 ) -> ZZ C_ S )
43 peano2nn0 
 |-  ( c e. NN0 -> ( c + 1 ) e. NN0 )
44 43 adantl 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ c e. NN0 ) -> ( c + 1 ) e. NN0 )
45 44 nn0zd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ c e. NN0 ) -> ( c + 1 ) e. ZZ )
46 42 45 sseldd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ c e. NN0 ) -> ( c + 1 ) e. S )
47 simplr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ c e. NN0 ) -> F e. ( Poly ` S ) )
48 subrgsubg 
 |-  ( S e. ( SubRing ` CCfld ) -> S e. ( SubGrp ` CCfld ) )
49 cnfld0 
 |-  0 = ( 0g ` CCfld )
50 49 subg0cl 
 |-  ( S e. ( SubGrp ` CCfld ) -> 0 e. S )
51 48 50 syl 
 |-  ( S e. ( SubRing ` CCfld ) -> 0 e. S )
52 51 ad2antrr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ c e. NN0 ) -> 0 e. S )
53 13 coef2 
 |-  ( ( F e. ( Poly ` S ) /\ 0 e. S ) -> ( coeff ` F ) : NN0 --> S )
54 47 52 53 syl2anc 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ c e. NN0 ) -> ( coeff ` F ) : NN0 --> S )
55 54 44 ffvelrnd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ c e. NN0 ) -> ( ( coeff ` F ) ` ( c + 1 ) ) e. S )
56 cnfldmul 
 |-  x. = ( .r ` CCfld )
57 56 subrgmcl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( c + 1 ) e. S /\ ( ( coeff ` F ) ` ( c + 1 ) ) e. S ) -> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) e. S )
58 40 46 55 57 syl3anc 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ c e. NN0 ) -> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) e. S )
59 58 fmpttd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( c e. NN0 |-> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) ) : NN0 --> S )
60 59 ffvelrnda 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ b e. NN0 ) -> ( ( c e. NN0 |-> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) ) ` b ) e. S )
61 39 60 sylan2 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ b e. ( 0 ... ( deg ` F ) ) ) -> ( ( c e. NN0 |-> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) ) ` b ) e. S )
62 38 6 61 elplyd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( a e. CC |-> sum_ b e. ( 0 ... ( deg ` F ) ) ( ( ( c e. NN0 |-> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) ) ` b ) x. ( a ^ b ) ) ) e. ( Poly ` S ) )
63 35 62 eqeltrd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( CC _D F ) e. ( Poly ` S ) )