Metamath Proof Explorer

Theorem dvnp1

Description: Successor iterated derivative. (Contributed by Stefan O'Rear, 15-Nov-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion dvnp1 
|- ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( ( S Dn F ) ` ( N + 1 ) ) = ( S _D ( ( S Dn F ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> N e. NN0 )
2 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
3 1 2 eleqtrdi 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> N e. ( ZZ>= ` 0 ) )
4 seqp1 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) ` ( N + 1 ) ) = ( ( seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) ` N ) ( ( x e. _V |-> ( S _D x ) ) o. 1st ) ( ( NN0 X. { F } ) ` ( N + 1 ) ) ) )
5 3 4 syl 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) ` ( N + 1 ) ) = ( ( seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) ` N ) ( ( x e. _V |-> ( S _D x ) ) o. 1st ) ( ( NN0 X. { F } ) ` ( N + 1 ) ) ) )
6 fvex 
 |-  ( seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) ` N ) e. _V
7 fvex 
 |-  ( ( NN0 X. { F } ) ` ( N + 1 ) ) e. _V
8 6 7 opco1i 
 |-  ( ( seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) ` N ) ( ( x e. _V |-> ( S _D x ) ) o. 1st ) ( ( NN0 X. { F } ) ` ( N + 1 ) ) ) = ( ( x e. _V |-> ( S _D x ) ) ` ( seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) ` N ) )
9 5 8 eqtrdi 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) ` ( N + 1 ) ) = ( ( x e. _V |-> ( S _D x ) ) ` ( seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) ` N ) ) )
10 eqid 
 |-  ( x e. _V |-> ( S _D x ) ) = ( x e. _V |-> ( S _D x ) )
11 10 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 } ) ) )
12 11 3adant3 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( S Dn F ) = seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) )
13 12 fveq1d 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( ( S Dn F ) ` ( N + 1 ) ) = ( seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) ` ( N + 1 ) ) )
14 fvex 
 |-  ( ( S Dn F ) ` N ) e. _V
15 oveq2 
 |-  ( x = ( ( S Dn F ) ` N ) -> ( S _D x ) = ( S _D ( ( S Dn F ) ` N ) ) )
16 ovex 
 |-  ( S _D ( ( S Dn F ) ` N ) ) e. _V
17 15 10 16 fvmpt 
 |-  ( ( ( S Dn F ) ` N ) e. _V -> ( ( x e. _V |-> ( S _D x ) ) ` ( ( S Dn F ) ` N ) ) = ( S _D ( ( S Dn F ) ` N ) ) )
18 14 17 ax-mp 
 |-  ( ( x e. _V |-> ( S _D x ) ) ` ( ( S Dn F ) ` N ) ) = ( S _D ( ( S Dn F ) ` N ) )
19 12 fveq1d 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( ( S Dn F ) ` N ) = ( seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) ` N ) )
20 19 fveq2d 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( ( x e. _V |-> ( S _D x ) ) ` ( ( S Dn F ) ` N ) ) = ( ( x e. _V |-> ( S _D x ) ) ` ( seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) ` N ) ) )
21 18 20 eqtr3id 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( S _D ( ( S Dn F ) ` N ) ) = ( ( x e. _V |-> ( S _D x ) ) ` ( seq 0 ( ( ( x e. _V |-> ( S _D x ) ) o. 1st ) , ( NN0 X. { F } ) ) ` N ) ) )
22 9 13 21 3eqtr4d 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( ( S Dn F ) ` ( N + 1 ) ) = ( S _D ( ( S Dn F ) ` N ) ) )