This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) Avoid ax-mulf . (Revised by GG, 30-Apr-2025)

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 ffvelcdmd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ c e. NN0 ) -> ( ( coeff ` F ) ` ( c + 1 ) ) e. S )
56 mpocnfldmul 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) = ( .r ` CCfld )
57 56 subrgmcl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( c + 1 ) e. S /\ ( ( coeff ` F ) ` ( c + 1 ) ) e. S ) -> ( ( c + 1 ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( ( coeff ` F ) ` ( c + 1 ) ) ) e. S )
58 37 a1d 
 |-  ( S e. ( SubRing ` CCfld ) -> ( ( ( coeff ` F ) ` ( c + 1 ) ) e. S -> S C_ CC ) )
59 ssel 
 |-  ( S C_ CC -> ( ( c + 1 ) e. S -> ( c + 1 ) e. CC ) )
60 59 a1i 
 |-  ( S e. ( SubRing ` CCfld ) -> ( S C_ CC -> ( ( c + 1 ) e. S -> ( c + 1 ) e. CC ) ) )
61 58 60 syld 
 |-  ( S e. ( SubRing ` CCfld ) -> ( ( ( coeff ` F ) ` ( c + 1 ) ) e. S -> ( ( c + 1 ) e. S -> ( c + 1 ) e. CC ) ) )
62 61 com23 
 |-  ( S e. ( SubRing ` CCfld ) -> ( ( c + 1 ) e. S -> ( ( ( coeff ` F ) ` ( c + 1 ) ) e. S -> ( c + 1 ) e. CC ) ) )
63 62 3imp 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( c + 1 ) e. S /\ ( ( coeff ` F ) ` ( c + 1 ) ) e. S ) -> ( c + 1 ) e. CC )
64 37 a1d 
 |-  ( S e. ( SubRing ` CCfld ) -> ( ( c + 1 ) e. S -> S C_ CC ) )
65 ssel 
 |-  ( S C_ CC -> ( ( ( coeff ` F ) ` ( c + 1 ) ) e. S -> ( ( coeff ` F ) ` ( c + 1 ) ) e. CC ) )
66 65 a1i 
 |-  ( S e. ( SubRing ` CCfld ) -> ( S C_ CC -> ( ( ( coeff ` F ) ` ( c + 1 ) ) e. S -> ( ( coeff ` F ) ` ( c + 1 ) ) e. CC ) ) )
67 64 66 syld 
 |-  ( S e. ( SubRing ` CCfld ) -> ( ( c + 1 ) e. S -> ( ( ( coeff ` F ) ` ( c + 1 ) ) e. S -> ( ( coeff ` F ) ` ( c + 1 ) ) e. CC ) ) )
68 67 3imp 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( c + 1 ) e. S /\ ( ( coeff ` F ) ` ( c + 1 ) ) e. S ) -> ( ( coeff ` F ) ` ( c + 1 ) ) e. CC )
69 63 68 jca 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( c + 1 ) e. S /\ ( ( coeff ` F ) ` ( c + 1 ) ) e. S ) -> ( ( c + 1 ) e. CC /\ ( ( coeff ` F ) ` ( c + 1 ) ) e. CC ) )
70 ovmpot 
 |-  ( ( ( c + 1 ) e. CC /\ ( ( coeff ` F ) ` ( c + 1 ) ) e. CC ) -> ( ( c + 1 ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( ( coeff ` F ) ` ( c + 1 ) ) ) = ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) )
71 69 70 syl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( c + 1 ) e. S /\ ( ( coeff ` F ) ` ( c + 1 ) ) e. S ) -> ( ( c + 1 ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( ( coeff ` F ) ` ( c + 1 ) ) ) = ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) )
72 71 eleq1d 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( c + 1 ) e. S /\ ( ( coeff ` F ) ` ( c + 1 ) ) e. S ) -> ( ( ( c + 1 ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( ( coeff ` F ) ` ( c + 1 ) ) ) e. S <-> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) e. S ) )
73 57 72 mpbid 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( c + 1 ) e. S /\ ( ( coeff ` F ) ` ( c + 1 ) ) e. S ) -> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) e. S )
74 40 46 55 73 syl3anc 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ c e. NN0 ) -> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) e. S )
75 74 fmpttd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( c e. NN0 |-> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) ) : NN0 --> S )
76 75 ffvelcdmda 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ b e. NN0 ) -> ( ( c e. NN0 |-> ( ( c + 1 ) x. ( ( coeff ` F ) ` ( c + 1 ) ) ) ) ` b ) e. S )
77 39 76 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 )
78 38 6 77 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 ) )
79 35 78 eqeltrd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( CC _D F ) e. ( Poly ` S ) )