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

Definition df-dv 24566
 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 24562 . 2 class D
2 vs . . 3 setvar 𝑠
3 vf . . 3 setvar 𝑓
4 cc 10573 . . . 4 class
54cpw 4494 . . 3 class 𝒫 ℂ
62cv 1537 . . . 4 class 𝑠
7 cpm 8417 . . . 4 class pm
84, 6, 7co 7150 . . 3 class (ℂ ↑pm 𝑠)
9 vx . . . 4 setvar 𝑥
103cv 1537 . . . . . 6 class 𝑓
1110cdm 5524 . . . . 5 class dom 𝑓
12 ccnfld 20166 . . . . . . . 8 class fld
13 ctopn 16753 . . . . . . . 8 class TopOpen
1412, 13cfv 6335 . . . . . . 7 class (TopOpen‘ℂfld)
15 crest 16752 . . . . . . 7 class t
1614, 6, 15co 7150 . . . . . 6 class ((TopOpen‘ℂfld) ↾t 𝑠)
17 cnt 21717 . . . . . 6 class int
1816, 17cfv 6335 . . . . 5 class (int‘((TopOpen‘ℂfld) ↾t 𝑠))
1911, 18cfv 6335 . . . 4 class ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)
209cv 1537 . . . . . 6 class 𝑥
2120csn 4522 . . . . 5 class {𝑥}
22 vz . . . . . . 7 setvar 𝑧
2311, 21cdif 3855 . . . . . . 7 class (dom 𝑓 ∖ {𝑥})
2422cv 1537 . . . . . . . . . 10 class 𝑧
2524, 10cfv 6335 . . . . . . . . 9 class (𝑓𝑧)
2620, 10cfv 6335 . . . . . . . . 9 class (𝑓𝑥)
27 cmin 10908 . . . . . . . . 9 class
2825, 26, 27co 7150 . . . . . . . 8 class ((𝑓𝑧) − (𝑓𝑥))
2924, 20, 27co 7150 . . . . . . . 8 class (𝑧𝑥)
30 cdiv 11335 . . . . . . . 8 class /
3128, 29, 30co 7150 . . . . . . 7 class (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))
3222, 23, 31cmpt 5112 . . . . . 6 class (𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥)))
33 climc 24561 . . . . . 6 class lim
3432, 20, 33co 7150 . . . . 5 class ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥)
3521, 34cxp 5522 . . . 4 class ({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥))
369, 19, 35ciun 4883 . . 3 class 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥))
372, 3, 5, 8, 36cmpo 7152 . 2 class (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥)))
381, 37wceq 1538 1 wff D = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥)))
 Colors of variables: wff setvar class This definition is referenced by:  reldv  24569  dvfval  24596  dvbsss  24601  perfdvf  24602
 Copyright terms: Public domain W3C validator