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 × { 𝐹 } ) ) )