Definition df-dv 23631

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

Step	Hyp	Ref	Expression
1		cdv 23627	. 2 class D
2		vs	. . 3 setvar 𝑠
3		vf	. . 3 setvar 𝑓
4		cc 9934	. . . 4 class ℂ
5	4	cpw 4158	. . 3 class 𝒫 ℂ
6	2	cv 1482	. . . 4 class 𝑠
7		cpm 7858	. . . 4 class ↑pm
8	4, 6, 7	co 6650	. . 3 class (ℂ ↑pm 𝑠)
9		vx	. . . 4 setvar 𝑥
10	3	cv 1482	. . . . . 6 class 𝑓
11	10	cdm 5114	. . . . 5 class dom 𝑓
12		ccnfld 19746	. . . . . . . 8 class ℂfld
13		ctopn 16082	. . . . . . . 8 class TopOpen
14	12, 13	cfv 5888	. . . . . . 7 class (TopOpen‘ℂfld)
15		crest 16081	. . . . . . 7 class ↾t
16	14, 6, 15	co 6650	. . . . . 6 class ((TopOpen‘ℂfld) ↾t 𝑠)
17		cnt 20821	. . . . . 6 class int
18	16, 17	cfv 5888	. . . . 5 class (int‘((TopOpen‘ℂfld) ↾t 𝑠))
19	11, 18	cfv 5888	. . . 4 class ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)
20	9	cv 1482	. . . . . 6 class 𝑥
21	20	csn 4177	. . . . 5 class {𝑥}
22		vz	. . . . . . 7 setvar 𝑧
23	11, 21	cdif 3571	. . . . . . 7 class (dom 𝑓 ∖ {𝑥})
24	22	cv 1482	. . . . . . . . . 10 class 𝑧
25	24, 10	cfv 5888	. . . . . . . . 9 class (𝑓‘𝑧)
26	20, 10	cfv 5888	. . . . . . . . 9 class (𝑓‘𝑥)
27		cmin 10266	. . . . . . . . 9 class −
28	25, 26, 27	co 6650	. . . . . . . 8 class ((𝑓‘𝑧) − (𝑓‘𝑥))
29	24, 20, 27	co 6650	. . . . . . . 8 class (𝑧 − 𝑥)
30		cdiv 10684	. . . . . . . 8 class /
31	28, 29, 30	co 6650	. . . . . . 7 class (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))
32	22, 23, 31	cmpt 4729	. . . . . 6 class (𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥)))
33		climc 23626	. . . . . 6 class limℂ
34	32, 20, 33	co 6650	. . . . 5 class ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)
35	21, 34	cxp 5112	. . . 4 class ({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥))
36	9, 19, 35	ciun 4520	. . 3 class ∪ 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥))
37	2, 3, 5, 8, 36	cmpt2 6652	. 2 class (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ ∪ 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)))
38	1, 37	wceq 1483	1 wff D = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ ∪ 𝑥 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ (dom 𝑓 ∖ {𝑥}) ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)))

This definition is referenced by:  reldv  23634  dvfval  23661  dvbsss  23666  perfdvf  23667