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 23354
Description: Define the derivative operator on functions on the reals. 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 23350 . 2 class D
2 vs . . 3 setvar 𝑠
3 vf . . 3 setvar 𝑓
4 cc 9790 . . . 4 class
54cpw 4107 . . 3 class 𝒫 ℂ
62cv 1473 . . . 4 class 𝑠
7 cpm 7722 . . . 4 class pm
84, 6, 7co 6527 . . 3 class (ℂ ↑pm 𝑠)
9 vx . . . 4 setvar 𝑥
103cv 1473 . . . . . 6 class 𝑓
1110cdm 5028 . . . . 5 class dom 𝑓
12 ccnfld 19513 . . . . . . . 8 class fld
13 ctopn 15851 . . . . . . . 8 class TopOpen
1412, 13cfv 5790 . . . . . . 7 class (TopOpen‘ℂfld)
15 crest 15850 . . . . . . 7 class t
1614, 6, 15co 6527 . . . . . 6 class ((TopOpen‘ℂfld) ↾t 𝑠)
17 cnt 20573 . . . . . 6 class int
1816, 17cfv 5790 . . . . 5 class (int‘((TopOpen‘ℂfld) ↾t 𝑠))
1911, 18cfv 5790 . . . 4 class ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)
209cv 1473 . . . . . 6 class 𝑥
2120csn 4124 . . . . 5 class {𝑥}
22 vz . . . . . . 7 setvar 𝑧
2311, 21cdif 3536 . . . . . . 7 class (dom 𝑓 ∖ {𝑥})
2422cv 1473 . . . . . . . . . 10 class 𝑧
2524, 10cfv 5790 . . . . . . . . 9 class (𝑓𝑧)
2620, 10cfv 5790 . . . . . . . . 9 class (𝑓𝑥)
27 cmin 10117 . . . . . . . . 9 class
2825, 26, 27co 6527 . . . . . . . 8 class ((𝑓𝑧) − (𝑓𝑥))
2924, 20, 27co 6527 . . . . . . . 8 class (𝑧𝑥)
30 cdiv 10533 . . . . . . . 8 class /
3128, 29, 30co 6527 . . . . . . 7 class (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))
3222, 23, 31cmpt 4637 . . . . . 6 class (𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥)))
33 climc 23349 . . . . . 6 class lim
3432, 20, 33co 6527 . . . . 5 class ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥)
3521, 34cxp 5026 . . . 4 class ({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥))
369, 19, 35ciun 4449 . . 3 class 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥))
372, 3, 5, 8, 36cmpt2 6529 . 2 class (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥)))
381, 37wceq 1474 1 wff D = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓𝑧) − (𝑓𝑥)) / (𝑧𝑥))) lim 𝑥)))
Colors of variables: wff setvar class
This definition is referenced by:  reldv  23357  dvfval  23384  dvbsss  23389  perfdvf  23390
  Copyright terms: Public domain W3C validator