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 ( ( 𝐺 ∘ 1^st ) , ( ℕ₀ × { 𝐹 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvnfval.1	⊢ 𝐺 = ( 𝑥 ∈ V ↦ ( 𝑆 D 𝑥 ) )
2		df-dvn	⊢ D^𝑛 = ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑_pm 𝑠 ) ↦ seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1^st ) , ( ℕ₀ × { 𝑓 } ) ) )
3	2	a1i	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) → D^𝑛 = ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑_pm 𝑠 ) ↦ seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1^st ) , ( ℕ₀ × { 𝑓 } ) ) ) )
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 𝑥 ) ) ∘ 1^st ) = ( 𝐺 ∘ 1^st ) )
9	8	seqeq2d	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1^st ) , ( ℕ₀ × { 𝑓 } ) ) = seq 0 ( ( 𝐺 ∘ 1^st ) , ( ℕ₀ × { 𝑓 } ) ) )
10		simprr	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → 𝑓 = 𝐹 )
11	10	sneqd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → { 𝑓 } = { 𝐹 } )
12	11	xpeq2d	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( ℕ₀ × { 𝑓 } ) = ( ℕ₀ × { 𝐹 } ) )
13	12	seqeq3d	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → seq 0 ( ( 𝐺 ∘ 1^st ) , ( ℕ₀ × { 𝑓 } ) ) = seq 0 ( ( 𝐺 ∘ 1^st ) , ( ℕ₀ × { 𝐹 } ) ) )
14	9 13	eqtrd	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1^st ) , ( ℕ₀ × { 𝑓 } ) ) = seq 0 ( ( 𝐺 ∘ 1^st ) , ( ℕ₀ × { 𝐹 } ) ) )
15		simpr	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑠 = 𝑆 ) → 𝑠 = 𝑆 )
16	15	oveq2d	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) ∧ 𝑠 = 𝑆 ) → ( ℂ ↑_pm 𝑠 ) = ( ℂ ↑_pm 𝑆 ) )
17		cnex	⊢ ℂ ∈ V
18	17	elpw2	⊢ ( 𝑆 ∈ 𝒫 ℂ ↔ 𝑆 ⊆ ℂ )
19	18	biranri	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) → 𝑆 ∈ 𝒫 ℂ )
20		simpr	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) → 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) )
21		seqex	⊢ seq 0 ( ( 𝐺 ∘ 1^st ) , ( ℕ₀ × { 𝐹 } ) ) ∈ V
22	21	a1i	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) → seq 0 ( ( 𝐺 ∘ 1^st ) , ( ℕ₀ × { 𝐹 } ) ) ∈ V )
23	3 14 16 19 20 22	ovmpodx	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) ) → ( 𝑆 D^𝑛 𝐹 ) = seq 0 ( ( 𝐺 ∘ 1^st ) , ( ℕ₀ × { 𝐹 } ) ) )

Metamath Proof Explorer

Theorem dvnfval

Proof