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 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.)

Assertion

Ref	Expression
df-dv	|- _D = ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x ) ) )

Distinct variable group:   f, s, x, z

Detailed syntax breakdown of Definition df-dv

Step	Hyp	Ref	Expression
1		cdv 23627	. 2 class _D
2		vs	. . 3 setvar s
3		vf	. . 3 setvar f
4		cc 9934	. . . 4 class CC
5	4	cpw 4158	. . 3 class ~P CC
6	2	cv 1482	. . . 4 class s
7		cpm 7858	. . . 4 class ^pm
8	4, 6, 7	co 6650	. . 3 class ( CC ^pm s )
9		vx	. . . 4 setvar x
10	3	cv 1482	. . . . . 6 class f
11	10	cdm 5114	. . . . 5 class dom f
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 s )
17		cnt 20821	. . . . . 6 class int
18	16, 17	cfv 5888	. . . . 5 class ( int ` ( ( TopOpen ` ℂfld ) ↾t s ) )
19	11, 18	cfv 5888	. . . 4 class ( ( int ` ( ( TopOpen ` ℂfld ) ↾t s ) ) ` dom f )
20	9	cv 1482	. . . . . 6 class x
21	20	csn 4177	. . . . 5 class { x }
22		vz	. . . . . . 7 setvar z
23	11, 21	cdif 3571	. . . . . . 7 class ( dom f \ { x } )
24	22	cv 1482	. . . . . . . . . 10 class z
25	24, 10	cfv 5888	. . . . . . . . 9 class ( f ` z )
26	20, 10	cfv 5888	. . . . . . . . 9 class ( f ` x )
27		cmin 10266	. . . . . . . . 9 class -
28	25, 26, 27	co 6650	. . . . . . . 8 class ( ( f ` z ) - ( f ` x ) )
29	24, 20, 27	co 6650	. . . . . . . 8 class ( z - x )
30		cdiv 10684	. . . . . . . 8 class /
31	28, 29, 30	co 6650	. . . . . . 7 class ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) )
32	22, 23, 31	cmpt 4729	. . . . . 6 class ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) )
33		climc 23626	. . . . . 6 class lim CC
34	32, 20, 33	co 6650	. . . . 5 class ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x )
35	21, 34	cxp 5112	. . . 4 class ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x ) )
36	9, 19, 35	ciun 4520	. . 3 class U_ x e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x ) )
37	2, 3, 5, 8, 36	cmpt2 6652	. 2 class ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x ) ) )
38	1, 37	wceq 1483	1 wff _D = ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) lim CC x ) ) )

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