Definition df-dvap 14062

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.) (Revised by Jim Kingdon, 25-Jun-2023.)

Assertion

Ref	Expression
df-dvap	⊢ D = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ ∪ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ {𝑤 ∈ dom 𝑓 ∣ 𝑤 # 𝑥} ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)))

Distinct variable group:   𝑓,𝑠,𝑥,𝑧,𝑤

Detailed syntax breakdown of Definition df-dvap

Step	Hyp	Ref	Expression
1		cdv 14060	. 2 class D
2		vs	. . 3 setvar 𝑠
3		vf	. . 3 setvar 𝑓
4		cc 7808	. . . 4 class ℂ
5	4	cpw 3575	. . 3 class 𝒫 ℂ
6	2	cv 1352	. . . 4 class 𝑠
7		cpm 6648	. . . 4 class ↑pm
8	4, 6, 7	co 5874	. . 3 class (ℂ ↑pm 𝑠)
9		vx	. . . 4 setvar 𝑥
10	3	cv 1352	. . . . . 6 class 𝑓
11	10	cdm 4626	. . . . 5 class dom 𝑓
12		cabs 11005	. . . . . . . . 9 class abs
13		cmin 8127	. . . . . . . . 9 class −
14	12, 13	ccom 4630	. . . . . . . 8 class (abs ∘ − )
15		cmopn 13381	. . . . . . . 8 class MetOpen
16	14, 15	cfv 5216	. . . . . . 7 class (MetOpen‘(abs ∘ − ))
17		crest 12687	. . . . . . 7 class ↾t
18	16, 6, 17	co 5874	. . . . . 6 class ((MetOpen‘(abs ∘ − )) ↾t 𝑠)
19		cnt 13529	. . . . . 6 class int
20	18, 19	cfv 5216	. . . . 5 class (int‘((MetOpen‘(abs ∘ − )) ↾t 𝑠))
21	11, 20	cfv 5216	. . . 4 class ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑠))‘dom 𝑓)
22	9	cv 1352	. . . . . 6 class 𝑥
23	22	csn 3592	. . . . 5 class {𝑥}
24		vz	. . . . . . 7 setvar 𝑧
25		vw	. . . . . . . . . 10 setvar 𝑤
26	25	cv 1352	. . . . . . . . 9 class 𝑤
27		cap 8537	. . . . . . . . 9 class #
28	26, 22, 27	wbr 4003	. . . . . . . 8 wff 𝑤 # 𝑥
29	28, 25, 11	crab 2459	. . . . . . 7 class {𝑤 ∈ dom 𝑓 ∣ 𝑤 # 𝑥}
30	24	cv 1352	. . . . . . . . . 10 class 𝑧
31	30, 10	cfv 5216	. . . . . . . . 9 class (𝑓‘𝑧)
32	22, 10	cfv 5216	. . . . . . . . 9 class (𝑓‘𝑥)
33	31, 32, 13	co 5874	. . . . . . . 8 class ((𝑓‘𝑧) − (𝑓‘𝑥))
34	30, 22, 13	co 5874	. . . . . . . 8 class (𝑧 − 𝑥)
35		cdiv 8628	. . . . . . . 8 class /
36	33, 34, 35	co 5874	. . . . . . 7 class (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))
37	24, 29, 36	cmpt 4064	. . . . . 6 class (𝑧 ∈ {𝑤 ∈ dom 𝑓 ∣ 𝑤 # 𝑥} ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥)))
38		climc 14059	. . . . . 6 class limℂ
39	37, 22, 38	co 5874	. . . . 5 class ((𝑧 ∈ {𝑤 ∈ dom 𝑓 ∣ 𝑤 # 𝑥} ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)
40	23, 39	cxp 4624	. . . 4 class ({𝑥} × ((𝑧 ∈ {𝑤 ∈ dom 𝑓 ∣ 𝑤 # 𝑥} ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥))
41	9, 21, 40	ciun 3886	. . 3 class ∪ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ {𝑤 ∈ dom 𝑓 ∣ 𝑤 # 𝑥} ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥))
42	2, 3, 5, 8, 41	cmpo 5876	. 2 class (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ ∪ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ {𝑤 ∈ dom 𝑓 ∣ 𝑤 # 𝑥} ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)))
43	1, 42	wceq 1353	1 wff D = (𝑠 ∈ 𝒫 ℂ, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ ∪ 𝑥 ∈ ((int‘((MetOpen‘(abs ∘ − )) ↾t 𝑠))‘dom 𝑓)({𝑥} × ((𝑧 ∈ {𝑤 ∈ dom 𝑓 ∣ 𝑤 # 𝑥} ↦ (((𝑓‘𝑧) − (𝑓‘𝑥)) / (𝑧 − 𝑥))) limℂ 𝑥)))

This definition is referenced by:  reldvg  14084  dvfvalap  14086