Definition df-dvn

Description: Define the n -th derivative operator on functions on the complex numbers. This just iterates the derivative operation according to the last argument. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Assertion	df-dvn	⊢ D𝑛 = ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝑓 } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdvn	⊢ D𝑛
1		vs	⊢ 𝑠
2		cc	⊢ ℂ
3	2	cpw	⊢ 𝒫 ℂ
4		vf	⊢ 𝑓
5		cpm	⊢ ↑pm
6	1	cv	⊢ 𝑠
7	2 6 5	co	⊢ ( ℂ ↑pm 𝑠 )
8		cc0	⊢ 0
9		vx	⊢ 𝑥
10		cvv	⊢ V
11		cdv	⊢ D
12	9	cv	⊢ 𝑥
13	6 12 11	co	⊢ ( 𝑠 D 𝑥 )
14	9 10 13	cmpt	⊢ ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) )
15		c1st	⊢ 1st
16	14 15	ccom	⊢ ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1st )
17		cn0	⊢ ℕ0
18	4	cv	⊢ 𝑓
19	18	csn	⊢ { 𝑓 }
20	17 19	cxp	⊢ ( ℕ0 × { 𝑓 } )
21	16 20 8	cseq	⊢ seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝑓 } ) )
22	1 4 3 7 21	cmpo	⊢ ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝑓 } ) ) )
23	0 22	wceq	⊢ D𝑛 = ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ seq 0 ( ( ( 𝑥 ∈ V ↦ ( 𝑠 D 𝑥 ) ) ∘ 1st ) , ( ℕ0 × { 𝑓 } ) ) )