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 23438
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 23434 . 2 class D𝑛
2 vs . . 3 setvar 𝑠
3 vf . . 3 setvar 𝑓
4 cc 9813 . . . 4 class
54cpw 4108 . . 3 class 𝒫 ℂ
62cv 1474 . . . 4 class 𝑠
7 cpm 7745 . . . 4 class pm
84, 6, 7co 6549 . . 3 class (ℂ ↑pm 𝑠)
9 vx . . . . . 6 setvar 𝑥
10 cvv 3173 . . . . . 6 class V
119cv 1474 . . . . . . 7 class 𝑥
12 cdv 23433 . . . . . . 7 class D
136, 11, 12co 6549 . . . . . 6 class (𝑠 D 𝑥)
149, 10, 13cmpt 4643 . . . . 5 class (𝑥 ∈ V ↦ (𝑠 D 𝑥))
15 c1st 7057 . . . . 5 class 1st
1614, 15ccom 5042 . . . 4 class ((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st )
17 cn0 11169 . . . . 5 class 0
183cv 1474 . . . . . 6 class 𝑓
1918csn 4125 . . . . 5 class {𝑓}
2017, 19cxp 5036 . . . 4 class (ℕ0 × {𝑓})
21 cc0 9815 . . . 4 class 0
2216, 20, 21cseq 12663 . . 3 class seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓}))
232, 3, 5, 8, 22cmpt2 6551 . 2 class (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
241, 23wceq 1475 1 wff D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
Colors of variables: wff setvar class
This definition is referenced by:  dvnfval  23491
  Copyright terms: Public domain W3C validator