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

Definition df-dv 24394
Description: Define the derivative operator. This acts on functions to produce a function that is defined where the original function is differentiable, with value the derivative of the function at these points. The set 𝑠 here is the ambient topological space under which we are evaluating the continuity of the difference quotient. Although the definition is valid for any subset of and is well-behaved when 𝑠 contains no isolated points, we will restrict our attention to the cases 𝑠 = ℝ or 𝑠 = ℂ for the majority of the development, these corresponding respectively to real and complex differentiation. (Contributed by Mario Carneiro, 7-Aug-2014.)
Assertion
Ref Expression
df-dv D = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥)))
Distinct variable group:   𝑓,𝑠,𝑥,𝑧

Detailed syntax breakdown of Definition df-dv
StepHypRef Expression
1 cdv 24390 . 2 class D
2 vs . . 3 setvar 𝑠
3 vf . . 3 setvar 𝑓
4 cc 10524 . . . 4 class
54cpw 4537 . . 3 class 𝒫 ℂ
62cv 1527 . . . 4 class 𝑠
7 cpm 8397 . . . 4 class pm
84, 6, 7co 7145 . . 3 class (ℂ ↑pm 𝑠)
9 vx . . . 4 setvar 𝑥
103cv 1527 . . . . . 6 class 𝑓
1110cdm 5549 . . . . 5 class dom 𝑓
12 ccnfld 20475 . . . . . . . 8 class fld
13 ctopn 16685 . . . . . . . 8 class TopOpen
1412, 13cfv 6349 . . . . . . 7 class (TopOpen‘ℂfld)
15 crest 16684 . . . . . . 7 class t
1614, 6, 15co 7145 . . . . . 6 class ((TopOpen‘ℂfld) ↾t 𝑠)
17 cnt 21555 . . . . . 6 class int
1816, 17cfv 6349 . . . . 5 class (int‘((TopOpen‘ℂfld) ↾t 𝑠))
1911, 18cfv 6349 . . . 4 class ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)
209cv 1527 . . . . . 6 class 𝑥
2120csn 4559 . . . . 5 class {𝑥}
22 vz . . . . . . 7 setvar 𝑧
2311, 21cdif 3932 . . . . . . 7 class (dom 𝑓 ∖ {𝑥})
2422cv 1527 . . . . . . . . . 10 class 𝑧
2524, 10cfv 6349 . . . . . . . . 9 class (𝑓𝑧)
2620, 10cfv 6349 . . . . . . . . 9 class (𝑓𝑥)
27 cmin 10859 . . . . . . . . 9 class
2825, 26, 27co 7145 . . . . . . . 8 class ((𝑓𝑧) − (𝑓𝑥))
2924, 20, 27co 7145 . . . . . . . 8 class (𝑧𝑥)
30 cdiv 11286 . . . . . . . 8 class /
3128, 29, 30co 7145 . . . . . . 7 class (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))
3222, 23, 31cmpt 5138 . . . . . 6 class (𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥)))
33 climc 24389 . . . . . 6 class lim
3432, 20, 33co 7145 . . . . 5 class ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥)
3521, 34cxp 5547 . . . 4 class ({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥))
369, 19, 35ciun 4912 . . 3 class 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥))
372, 3, 5, 8, 36cmpo 7147 . 2 class (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥)))
381, 37wceq 1528 1 wff D = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥)))
Colors of variables: wff setvar class
This definition is referenced by:  reldv  24397  dvfval  24424  dvbsss  24429  perfdvf  24430
  Copyright terms: Public domain W3C validator