This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑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 opco1i ⊢ ( ( 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 eqtr3id ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ) = ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ‘ ( seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ‘ 𝑁 ) ) )
22 9 13 21 3eqtr4d ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑆 D𝑛 𝐹 ) ‘ ( 𝑁 + 1 ) ) = ( 𝑆 D ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ) )