Metamath Proof Explorer

Theorem dvnply2

Description: Polynomials have polynomials as derivatives of all orders. (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Assertion dvnply2 
|- ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) /\ N e. NN0 ) -> ( ( CC Dn F ) ` N ) e. ( Poly ` S ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = 0 -> ( ( CC Dn F ) ` x ) = ( ( CC Dn F ) ` 0 ) )
2 1 eleq1d 
 |-  ( x = 0 -> ( ( ( CC Dn F ) ` x ) e. ( Poly ` S ) <-> ( ( CC Dn F ) ` 0 ) e. ( Poly ` S ) ) )
3 2 imbi2d 
 |-  ( x = 0 -> ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` x ) e. ( Poly ` S ) ) <-> ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` 0 ) e. ( Poly ` S ) ) ) )
4 fveq2 
 |-  ( x = n -> ( ( CC Dn F ) ` x ) = ( ( CC Dn F ) ` n ) )
5 4 eleq1d 
 |-  ( x = n -> ( ( ( CC Dn F ) ` x ) e. ( Poly ` S ) <-> ( ( CC Dn F ) ` n ) e. ( Poly ` S ) ) )
6 5 imbi2d 
 |-  ( x = n -> ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` x ) e. ( Poly ` S ) ) <-> ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` n ) e. ( Poly ` S ) ) ) )
7 fveq2 
 |-  ( x = ( n + 1 ) -> ( ( CC Dn F ) ` x ) = ( ( CC Dn F ) ` ( n + 1 ) ) )
8 7 eleq1d 
 |-  ( x = ( n + 1 ) -> ( ( ( CC Dn F ) ` x ) e. ( Poly ` S ) <-> ( ( CC Dn F ) ` ( n + 1 ) ) e. ( Poly ` S ) ) )
9 8 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` x ) e. ( Poly ` S ) ) <-> ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` ( n + 1 ) ) e. ( Poly ` S ) ) ) )
10 fveq2 
 |-  ( x = N -> ( ( CC Dn F ) ` x ) = ( ( CC Dn F ) ` N ) )
11 10 eleq1d 
 |-  ( x = N -> ( ( ( CC Dn F ) ` x ) e. ( Poly ` S ) <-> ( ( CC Dn F ) ` N ) e. ( Poly ` S ) ) )
12 11 imbi2d 
 |-  ( x = N -> ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` x ) e. ( Poly ` S ) ) <-> ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` N ) e. ( Poly ` S ) ) ) )
13 ssid 
 |-  CC C_ CC
14 cnex 
 |-  CC e. _V
15 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
16 15 adantl 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> F : CC --> CC )
17 fpmg 
 |-  ( ( CC e. _V /\ CC e. _V /\ F : CC --> CC ) -> F e. ( CC ^pm CC ) )
18 14 14 16 17 mp3an12i 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> F e. ( CC ^pm CC ) )
19 dvn0 
 |-  ( ( CC C_ CC /\ F e. ( CC ^pm CC ) ) -> ( ( CC Dn F ) ` 0 ) = F )
20 13 18 19 sylancr 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` 0 ) = F )
21 simpr 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> F e. ( Poly ` S ) )
22 20 21 eqeltrd 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` 0 ) e. ( Poly ` S ) )
23 dvply2g 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ ( ( CC Dn F ) ` n ) e. ( Poly ` S ) ) -> ( CC _D ( ( CC Dn F ) ` n ) ) e. ( Poly ` S ) )
24 23 ex 
 |-  ( S e. ( SubRing ` CCfld ) -> ( ( ( CC Dn F ) ` n ) e. ( Poly ` S ) -> ( CC _D ( ( CC Dn F ) ` n ) ) e. ( Poly ` S ) ) )
25 24 ad2antrr 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( ( CC Dn F ) ` n ) e. ( Poly ` S ) -> ( CC _D ( ( CC Dn F ) ` n ) ) e. ( Poly ` S ) ) )
26 dvnp1 
 |-  ( ( CC C_ CC /\ F e. ( CC ^pm CC ) /\ n e. NN0 ) -> ( ( CC Dn F ) ` ( n + 1 ) ) = ( CC _D ( ( CC Dn F ) ` n ) ) )
27 13 26 mp3an1 
 |-  ( ( F e. ( CC ^pm CC ) /\ n e. NN0 ) -> ( ( CC Dn F ) ` ( n + 1 ) ) = ( CC _D ( ( CC Dn F ) ` n ) ) )
28 18 27 sylan 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( CC Dn F ) ` ( n + 1 ) ) = ( CC _D ( ( CC Dn F ) ` n ) ) )
29 28 eleq1d 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( ( CC Dn F ) ` ( n + 1 ) ) e. ( Poly ` S ) <-> ( CC _D ( ( CC Dn F ) ` n ) ) e. ( Poly ` S ) ) )
30 25 29 sylibrd 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ n e. NN0 ) -> ( ( ( CC Dn F ) ` n ) e. ( Poly ` S ) -> ( ( CC Dn F ) ` ( n + 1 ) ) e. ( Poly ` S ) ) )
31 30 expcom 
 |-  ( n e. NN0 -> ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( ( CC Dn F ) ` n ) e. ( Poly ` S ) -> ( ( CC Dn F ) ` ( n + 1 ) ) e. ( Poly ` S ) ) ) )
32 31 a2d 
 |-  ( n e. NN0 -> ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` n ) e. ( Poly ` S ) ) -> ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` ( n + 1 ) ) e. ( Poly ` S ) ) ) )
33 3 6 9 12 22 32 nn0ind 
 |-  ( N e. NN0 -> ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) -> ( ( CC Dn F ) ` N ) e. ( Poly ` S ) ) )
34 33 impcom 
 |-  ( ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) ) /\ N e. NN0 ) -> ( ( CC Dn F ) ` N ) e. ( Poly ` S ) )
35 34 3impa 
 |-  ( ( S e. ( SubRing ` CCfld ) /\ F e. ( Poly ` S ) /\ N e. NN0 ) -> ( ( CC Dn F ) ` N ) e. ( Poly ` S ) )