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

Definition df-dvn 24580
 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 24576 . 2 class D𝑛
2 vs . . 3 setvar 𝑠
3 vf . . 3 setvar 𝑓
4 cc 10586 . . . 4 class
54cpw 4497 . . 3 class 𝒫 ℂ
62cv 1537 . . . 4 class 𝑠
7 cpm 8423 . . . 4 class pm
84, 6, 7co 7156 . . 3 class (ℂ ↑pm 𝑠)
9 vx . . . . . 6 setvar 𝑥
10 cvv 3409 . . . . . 6 class V
119cv 1537 . . . . . . 7 class 𝑥
12 cdv 24575 . . . . . . 7 class D
136, 11, 12co 7156 . . . . . 6 class (𝑠 D 𝑥)
149, 10, 13cmpt 5116 . . . . 5 class (𝑥 ∈ V ↦ (𝑠 D 𝑥))
15 c1st 7697 . . . . 5 class 1st
1614, 15ccom 5532 . . . 4 class ((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st )
17 cn0 11947 . . . . 5 class 0
183cv 1537 . . . . . 6 class 𝑓
1918csn 4525 . . . . 5 class {𝑓}
2017, 19cxp 5526 . . . 4 class (ℕ0 × {𝑓})
21 cc0 10588 . . . 4 class 0
2216, 20, 21cseq 13431 . . 3 class seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓}))
232, 3, 5, 8, 22cmpo 7158 . 2 class (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
241, 23wceq 1538 1 wff D𝑛 = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ seq0(((𝑥 ∈ V ↦ (𝑠 D 𝑥)) ∘ 1st ), (ℕ0 × {𝑓})))
 Colors of variables: wff setvar class This definition is referenced by:  dvnfval  24634
 Copyright terms: Public domain W3C validator