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

Metamath Proof Explorer

Theorem dvnfval

Description: Value of the iterated derivative. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypothesis dvnfval.1 ⊢ 𝐺 = ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) )
Assertion dvnfval ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( 𝑆 D𝑛 𝐹 ) = seq 0 ( ( 𝐺 ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) )

Proof

Step Hyp Ref Expression
1 dvnfval.1 ⊢ 𝐺 = ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) )
2 df-dvn ⊢ D𝑛 = ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝑓 } ) ) )
3 2 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → D𝑛 = ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝑓 } ) ) ) )
4 simprl ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → 𝑠 = 𝑆 )
5 4 oveq1d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( 𝑠 D 𝑥 ) = ( 𝑆 D 𝑥 ) )
6 5 mpteq2dv ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) = ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) ) )
7 6 1 eqtr4di ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) = 𝐺 )
8 7 coeq1d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1st ) = ( 𝐺 ∘ 1st ) )
9 8 seqeq2d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝑓 } ) ) = seq 0 ( ( 𝐺 ∘ 1st ) , ( ℕ0 × { 𝑓 } ) ) )
10 simprr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → 𝑓 = 𝐹 )
11 10 sneqd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → { 𝑓 } = { 𝐹 } )
12 11 xpeq2d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( ℕ0 × { 𝑓 } ) = ( ℕ0 × { 𝐹 } ) )
13 12 seqeq3d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → seq 0 ( ( 𝐺 ∘ 1st ) , ( ℕ0 × { 𝑓 } ) ) = seq 0 ( ( 𝐺 ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) )
14 9 13 eqtrd ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝑓 } ) ) = seq 0 ( ( 𝐺 ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) )
15 simpr ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑠 = 𝑆 ) → 𝑠 = 𝑆 )
16 15 oveq2d ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) ∧ 𝑠 = 𝑆 ) → ( ℂ ↑pm 𝑠 ) = ( ℂ ↑pm 𝑆 ) )
17 simpl ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → 𝑆 ⊆ ℂ )
18 cnex ⊢ ℂ ∈ V
19 18 elpw2 ⊢ ( 𝑆 ∈ 𝒫 ℂ ↔ 𝑆 ⊆ ℂ )
20 17 19 sylibr ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → 𝑆 ∈ 𝒫 ℂ )
21 simpr ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → 𝐹 ∈ ( ℂ ↑pm 𝑆 ) )
22 seqex ⊢ seq 0 ( ( 𝐺 ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ∈ V
23 22 a1i ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → seq 0 ( ( 𝐺 ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) ∈ V )
24 3 14 16 20 21 23 ovmpodx ⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑pm 𝑆 ) ) → ( 𝑆 D𝑛 𝐹 ) = seq 0 ( ( 𝐺 ∘ 1st ) , ( ℕ0 × { 𝐹 } ) ) )