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 23802
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 23798 . 2 class D𝑛
2 vs . . 3 setvar 𝑠
3 vf . . 3 setvar 𝑓
4 cc 10097 . . . 4 class
54cpw 4290 . . 3 class 𝒫 ℂ
62cv 1619 . . . 4 class 𝑠
7 cpm 8012 . . . 4 class pm
84, 6, 7co 6801 . . 3 class (ℂ ↑pm 𝑠)
9 vx . . . . . 6 setvar 𝑥
10 cvv 3328 . . . . . 6 class V
119cv 1619 . . . . . . 7 class 𝑥
12 cdv 23797 . . . . . . 7 class D
136, 11, 12co 6801 . . . . . 6 class (𝑠 D 𝑥)
149, 10, 13cmpt 4869 . . . . 5 class (𝑥 ∈ V ↦ (𝑠 D 𝑥))
15 c1st 7319 . . . . 5 class 1st
1614, 15ccom 5258 . . . 4 class ((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st )
17 cn0 11455 . . . . 5 class 0
183cv 1619 . . . . . 6 class 𝑓
1918csn 4309 . . . . 5 class {𝑓}
2017, 19cxp 5252 . . . 4 class (ℕ0 × {𝑓})
21 cc0 10099 . . . 4 class 0
2216, 20, 21cseq 12966 . . 3 class seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓}))
232, 3, 5, 8, 22cmpt2 6803 . 2 class (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
241, 23wceq 1620 1 wff D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
Colors of variables: wff setvar class
This definition is referenced by:  dvnfval  23855
  Copyright terms: Public domain W3C validator