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 F 𝑝𝑚 S N 0 S D n F N + 1 = S D S D n F N

Proof

Step Hyp Ref Expression
1 simp3 S F 𝑝𝑚 S N 0 N 0
2 nn0uz 0 = 0
3 1 2 eleqtrdi S F 𝑝𝑚 S N 0 N 0
4 seqp1 N 0 seq 0 x V S D x 1 st 0 × F N + 1 = seq 0 x V S D x 1 st 0 × F N x V S D x 1 st 0 × F N + 1
5 3 4 syl S F 𝑝𝑚 S N 0 seq 0 x V S D x 1 st 0 × F N + 1 = seq 0 x V S D x 1 st 0 × F N x V S D x 1 st 0 × F N + 1
6 fvex seq 0 x V S D x 1 st 0 × F N V
7 fvex 0 × F N + 1 V
8 6 7 algrflem seq 0 x V S D x 1 st 0 × F N x V S D x 1 st 0 × F N + 1 = x V S D x seq 0 x V S D x 1 st 0 × F N
9 5 8 eqtrdi S F 𝑝𝑚 S N 0 seq 0 x V S D x 1 st 0 × F N + 1 = x V S D x seq 0 x V S D x 1 st 0 × F N
10 eqid x V S D x = x V S D x
11 10 dvnfval S F 𝑝𝑚 S S D n F = seq 0 x V S D x 1 st 0 × F
12 11 3adant3 S F 𝑝𝑚 S N 0 S D n F = seq 0 x V S D x 1 st 0 × F
13 12 fveq1d S F 𝑝𝑚 S N 0 S D n F N + 1 = seq 0 x V S D x 1 st 0 × F N + 1
14 fvex S D n F N V
15 oveq2 x = S D n F N S D x = S D S D n F N
16 ovex S D S D n F N V
17 15 10 16 fvmpt S D n F N V x V S D x S D n F N = S D S D n F N
18 14 17 ax-mp x V S D x S D n F N = S D S D n F N
19 12 fveq1d S F 𝑝𝑚 S N 0 S D n F N = seq 0 x V S D x 1 st 0 × F N
20 19 fveq2d S F 𝑝𝑚 S N 0 x V S D x S D n F N = x V S D x seq 0 x V S D x 1 st 0 × F N
21 18 20 syl5eqr S F 𝑝𝑚 S N 0 S D S D n F N = x V S D x seq 0 x V S D x 1 st 0 × F N
22 9 13 21 3eqtr4d S F 𝑝𝑚 S N 0 S D n F N + 1 = S D S D n F N