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	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp3	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
2		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
3	1 2	eleqtrdi	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
4		seqp1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 0 ) → ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ 𝑁 ) ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) ( ( ℕ0 × { 𝐹 } ) ‘ ( 𝑁 + 1 ) ) ) )
5	3 4	syl	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ 𝑁 ) ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) ( ( ℕ0 × { 𝐹 } ) ‘ ( 𝑁 + 1 ) ) ) )
6		fvex	⊢ ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ 𝑁 ) ∈ V
7		fvex	⊢ ( ( ℕ0 × { 𝐹 } ) ‘ ( 𝑁 + 1 ) ) ∈ V
8	6 7	algrflem	⊢ ( ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ 𝑁 ) ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) ( ( ℕ0 × { 𝐹 } ) ‘ ( 𝑁 + 1 ) ) ) = ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ‘ ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ 𝑁 ) )
9	5 8	eqtrdi	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ ( 𝑁 + 1 ) ) = ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ‘ ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ 𝑁 ) ) )
10		eqid	⊢ ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) = ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) )
11	10	dvnfval	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( 𝑆 D𝑛 𝐹 ) = seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) )
12	11	3adant3	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑆 D𝑛 𝐹 ) = seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) )
13	12	fveq1d	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ ( 𝑁 + 1 ) ) )
14		fvex	⊢ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ∈ V
15		oveq2	⊢ ( 𝑥 = ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) → ( 𝑆 D 𝑥 ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ) )
16		ovex	⊢ ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ) ∈ V
17	15 10 16	fvmpt	⊢ ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ∈ V → ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ‘ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ) )
18	14 17	ax-mp	⊢ ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ‘ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
19	12	fveq1d	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) = ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ 𝑁 ) )
20	19	fveq2d	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ‘ ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ) = ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ‘ ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ 𝑁 ) ) )
21	18 20	syl5eqr	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ) = ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ‘ ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ 𝑁 ) ) )
22	9 13 21	3eqtr4d	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ) )