Metamath Proof Explorer

Theorem dvnff

Description: The iterated derivative is a function. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion dvnff 
|- ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> ( S Dn F ) : NN0 --> ( CC ^pm dom F ) )

Proof

Step Hyp Ref Expression
1 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
2 0zd 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> 0 e. ZZ )
3 fvconst2g 
 |-  ( ( F e. ( CC ^pm S ) /\ k e. NN0 ) -> ( ( NN0 X. { F } ) ` k ) = F )
4 3 adantll 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ k e. NN0 ) -> ( ( NN0 X. { F } ) ` k ) = F )
5 dmexg 
 |-  ( F e. ( CC ^pm S ) -> dom F e. _V )
6 5 ad2antlr 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ k e. NN0 ) -> dom F e. _V )
7 cnex 
 |-  CC e. _V
8 7 a1i 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ k e. NN0 ) -> CC e. _V )
9 elpm2g 
 |-  ( ( CC e. _V /\ S e. { RR , CC } ) -> ( F e. ( CC ^pm S ) <-> ( F : dom F --> CC /\ dom F C_ S ) ) )
10 7 9 mpan 
 |-  ( S e. { RR , CC } -> ( F e. ( CC ^pm S ) <-> ( F : dom F --> CC /\ dom F C_ S ) ) )
11 10 biimpa 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> ( F : dom F --> CC /\ dom F C_ S ) )
12 11 simpld 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> F : dom F --> CC )
13 12 adantr 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ k e. NN0 ) -> F : dom F --> CC )
14 fpmg 
 |-  ( ( dom F e. _V /\ CC e. _V /\ F : dom F --> CC ) -> F e. ( CC ^pm dom F ) )
15 6 8 13 14 syl3anc 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ k e. NN0 ) -> F e. ( CC ^pm dom F ) )
16 4 15 eqeltrd 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ k e. NN0 ) -> ( ( NN0 X. { F } ) ` k ) e. ( CC ^pm dom F ) )
17 vex 
 |-  k e. _V
18 vex 
 |-  n e. _V
19 17 18 algrflem 
 |-  ( k ( ( x e. _V |-> ( S _D x ) ) o. 1st ) n ) = ( ( x e. _V |-> ( S _D x ) ) ` k )
20 oveq2 
 |-  ( x = k -> ( S _D x ) = ( S _D k ) )
21 eqid 
 |-  ( x e. _V |-> ( S _D x ) ) = ( x e. _V |-> ( S _D x ) )
22 ovex 
 |-  ( S _D k ) e. _V
23 20 21 22 fvmpt 
 |-  ( k e. _V -> ( ( x e. _V |-> ( S _D x ) ) ` k ) = ( S _D k ) )
24 23 elv 
 |-  ( ( x e. _V |-> ( S _D x ) ) ` k ) = ( S _D k )
25 19 24 eqtri 
 |-  ( k ( ( x e. _V |-> ( S _D x ) ) o. 1st ) n ) = ( S _D k )
26 7 a1i 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( k e. ( CC ^pm dom F ) /\ n e. ( CC ^pm dom F ) ) ) -> CC e. _V )
27 5 ad2antlr 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( k e. ( CC ^pm dom F ) /\ n e. ( CC ^pm dom F ) ) ) -> dom F e. _V )
28 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D k ) : dom ( S _D k ) --> CC )
29 28 ad2antrr 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( k e. ( CC ^pm dom F ) /\ n e. ( CC ^pm dom F ) ) ) -> ( S _D k ) : dom ( S _D k ) --> CC )
30 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
31 30 ad2antrr 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( k e. ( CC ^pm dom F ) /\ n e. ( CC ^pm dom F ) ) ) -> S C_ CC )
32 simprl 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( k e. ( CC ^pm dom F ) /\ n e. ( CC ^pm dom F ) ) ) -> k e. ( CC ^pm dom F ) )
33 elpm2g 
 |-  ( ( CC e. _V /\ dom F e. _V ) -> ( k e. ( CC ^pm dom F ) <-> ( k : dom k --> CC /\ dom k C_ dom F ) ) )
34 7 27 33 sylancr 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( k e. ( CC ^pm dom F ) /\ n e. ( CC ^pm dom F ) ) ) -> ( k e. ( CC ^pm dom F ) <-> ( k : dom k --> CC /\ dom k C_ dom F ) ) )
35 32 34 mpbid 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( k e. ( CC ^pm dom F ) /\ n e. ( CC ^pm dom F ) ) ) -> ( k : dom k --> CC /\ dom k C_ dom F ) )
36 35 simpld 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( k e. ( CC ^pm dom F ) /\ n e. ( CC ^pm dom F ) ) ) -> k : dom k --> CC )
37 35 simprd 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( k e. ( CC ^pm dom F ) /\ n e. ( CC ^pm dom F ) ) ) -> dom k C_ dom F )
38 11 simprd 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> dom F C_ S )
39 38 adantr 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( k e. ( CC ^pm dom F ) /\ n e. ( CC ^pm dom F ) ) ) -> dom F C_ S )
40 37 39 sstrd 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( k e. ( CC ^pm dom F ) /\ n e. ( CC ^pm dom F ) ) ) -> dom k C_ S )
41 31 36 40 dvbss 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( k e. ( CC ^pm dom F ) /\ n e. ( CC ^pm dom F ) ) ) -> dom ( S _D k ) C_ dom k )
42 41 37 sstrd 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( k e. ( CC ^pm dom F ) /\ n e. ( CC ^pm dom F ) ) ) -> dom ( S _D k ) C_ dom F )
43 elpm2r 
 |-  ( ( ( CC e. _V /\ dom F e. _V ) /\ ( ( S _D k ) : dom ( S _D k ) --> CC /\ dom ( S _D k ) C_ dom F ) ) -> ( S _D k ) e. ( CC ^pm dom F ) )
44 26 27 29 42 43 syl22anc 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( k e. ( CC ^pm dom F ) /\ n e. ( CC ^pm dom F ) ) ) -> ( S _D k ) e. ( CC ^pm dom F ) )
45 25 44 eqeltrid 
 |-  ( ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) /\ ( k e. ( CC ^pm dom F ) /\ n e. ( CC ^pm dom F ) ) ) -> ( k ( ( x e. _V |-> ( S _D x ) ) o. 1st ) n ) e. ( CC ^pm dom F ) )
46 1 2 16 45 seqf 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) : NN0 --> ( CC ^pm dom F ) )
47 21 dvnfval 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( S Dn F ) = seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) )
48 30 47 sylan 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> ( S Dn F ) = seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) )
49 48 feq1d 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) : NN0 --> ( CC ^pm dom F ) <-> seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) : NN0 --> ( CC ^pm dom F ) ) )
50 46 49 mpbird 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) ) -> ( S Dn F ) : NN0 --> ( CC ^pm dom F ) )