MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dvn Structured version   Visualization version   GIF version

Definition df-dvn 23538
Description: Define the 𝑛-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.)
Assertion
Ref Expression
df-dvn D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
Distinct variable group:   𝑓,𝑠,𝑥

Detailed syntax breakdown of Definition df-dvn
StepHypRef Expression
1 cdvn 23534 . 2 class D𝑛
2 vs . . 3 setvar 𝑠
3 vf . . 3 setvar 𝑓
4 cc 9878 . . . 4 class
54cpw 4130 . . 3 class 𝒫 ℂ
62cv 1479 . . . 4 class 𝑠
7 cpm 7803 . . . 4 class pm
84, 6, 7co 6604 . . 3 class (ℂ ↑pm 𝑠)
9 vx . . . . . 6 setvar 𝑥
10 cvv 3186 . . . . . 6 class V
119cv 1479 . . . . . . 7 class 𝑥
12 cdv 23533 . . . . . . 7 class D
136, 11, 12co 6604 . . . . . 6 class (𝑠 D 𝑥)
149, 10, 13cmpt 4673 . . . . 5 class (𝑥 ∈ V ↦ (𝑠 D 𝑥))
15 c1st 7111 . . . . 5 class 1st
1614, 15ccom 5078 . . . 4 class ((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st )
17 cn0 11236 . . . . 5 class 0
183cv 1479 . . . . . 6 class 𝑓
1918csn 4148 . . . . 5 class {𝑓}
2017, 19cxp 5072 . . . 4 class (ℕ0 × {𝑓})
21 cc0 9880 . . . 4 class 0
2216, 20, 21cseq 12741 . . 3 class seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓}))
232, 3, 5, 8, 22cmpt2 6606 . 2 class (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
241, 23wceq 1480 1 wff D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
Colors of variables: wff setvar class
This definition is referenced by:  dvnfval  23591
  Copyright terms: Public domain W3C validator