Definition df-dvap 12800

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 s 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 CC and is well-behaved when s contains no isolated points, we will restrict our attention to the cases s = RR or s = CC 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 = ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( MetOpen ` ( abs o. - ) ) ↾t s ) ) ` dom f ) ( { x } X. ( ( z e. { w e. dom f | w # x } |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x ) ) )

Distinct variable group:   f, s, x, z, w

Detailed syntax breakdown of Definition df-dvap

Step	Hyp	Ref	Expression
1		cdv 12798	. 2 class _D
2		vs	. . 3 setvar s
3		vf	. . 3 setvar f
4		cc 7623	. . . 4 class CC
5	4	cpw 3510	. . 3 class ~P CC
6	2	cv 1330	. . . 4 class s
7		cpm 6543	. . . 4 class ^pm
8	4, 6, 7	co 5774	. . 3 class ( CC ^pm s )
9		vx	. . . 4 setvar x
10	3	cv 1330	. . . . . 6 class f
11	10	cdm 4539	. . . . 5 class dom f
12		cabs 10774	. . . . . . . . 9 class abs
13		cmin 7938	. . . . . . . . 9 class -
14	12, 13	ccom 4543	. . . . . . . 8 class ( abs o. - )
15		cmopn 12159	. . . . . . . 8 class MetOpen
16	14, 15	cfv 5123	. . . . . . 7 class ( MetOpen ` ( abs o. - ) )
17		crest 12125	. . . . . . 7 class ↾t
18	16, 6, 17	co 5774	. . . . . 6 class ( ( MetOpen ` ( abs o. - ) ) ↾t s )
19		cnt 12267	. . . . . 6 class int
20	18, 19	cfv 5123	. . . . 5 class ( int ` ( ( MetOpen ` ( abs o. - ) ) ↾t s ) )
21	11, 20	cfv 5123	. . . 4 class ( ( int ` ( ( MetOpen ` ( abs o. - ) ) ↾t s ) ) ` dom f )
22	9	cv 1330	. . . . . 6 class x
23	22	csn 3527	. . . . 5 class { x }
24		vz	. . . . . . 7 setvar z
25		vw	. . . . . . . . . 10 setvar w
26	25	cv 1330	. . . . . . . . 9 class w
27		cap 8348	. . . . . . . . 9 class #
28	26, 22, 27	wbr 3929	. . . . . . . 8 wff w # x
29	28, 25, 11	crab 2420	. . . . . . 7 class { w e. dom f | w # x }
30	24	cv 1330	. . . . . . . . . 10 class z
31	30, 10	cfv 5123	. . . . . . . . 9 class ( f ` z )
32	22, 10	cfv 5123	. . . . . . . . 9 class ( f ` x )
33	31, 32, 13	co 5774	. . . . . . . 8 class ( ( f ` z ) - ( f ` x ) )
34	30, 22, 13	co 5774	. . . . . . . 8 class ( z - x )
35		cdiv 8437	. . . . . . . 8 class /
36	33, 34, 35	co 5774	. . . . . . 7 class ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) )
37	24, 29, 36	cmpt 3989	. . . . . 6 class ( z e. { w e. dom f | w # x } |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) )
38		climc 12797	. . . . . 6 class lim CC
39	37, 22, 38	co 5774	. . . . 5 class ( ( z e. { w e. dom f | w # x } |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x )
40	23, 39	cxp 4537	. . . 4 class ( { x } X. ( ( z e. { w e. dom f | w # x } |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x ) )
41	9, 21, 40	ciun 3813	. . 3 class U_ x e. ( ( int ` ( ( MetOpen ` ( abs o. - ) ) ↾t s ) ) ` dom f ) ( { x } X. ( ( z e. { w e. dom f | w # x } |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x ) )
42	2, 3, 5, 8, 41	cmpo 5776	. 2 class ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( MetOpen ` ( abs o. - ) ) ↾t s ) ) ` dom f ) ( { x } X. ( ( z e. { w e. dom f | w # x } |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x ) ) )
43	1, 42	wceq 1331	1 wff _D = ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( MetOpen ` ( abs o. - ) ) ↾t s ) ) ` dom f ) ( { x } X. ( ( z e. { w e. dom f | w # x } |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x ) ) )

This definition is referenced by:  reldvg  12822  dvfvalap  12824