Definition df-dv

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdv	|- _D
1		vs	|- s
2		cc	|- CC
3	2	cpw	|- ~P CC
4		vf	|- f
5		cpm	|- ^pm
6	1	cv	|- s
7	2 6 5	co	|- ( CC ^pm s )
8		vx	|- x
9		cnt	|- int
10		ctopn	|- TopOpen
11		ccnfld	|- CCfld
12	11 10	cfv	|- ( TopOpen ` CCfld )
13		crest	|- |`t
14	12 6 13	co	|- ( ( TopOpen ` CCfld ) |`t s )
15	14 9	cfv	|- ( int ` ( ( TopOpen ` CCfld ) |`t s ) )
16	4	cv	|- f
17	16	cdm	|- dom f
18	17 15	cfv	|- ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f )
19	8	cv	|- x
20	19	csn	|- { x }
21		vz	|- z
22	17 20	cdif	|- ( dom f \ { x } )
23	21	cv	|- z
24	23 16	cfv	|- ( f ` z )
25		cmin	|- -
26	19 16	cfv	|- ( f ` x )
27	24 26 25	co	|- ( ( f ` z ) - ( f ` x ) )
28		cdiv	|- /
29	23 19 25	co	|- ( z - x )
30	27 29 28	co	|- ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) )
31	21 22 30	cmpt	|- ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) )
32		climc	|- limCC
33	31 19 32	co	|- ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x )
34	20 33	cxp	|- ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) )
35	8 18 34	ciun	|- U_ x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) )
36	1 4 3 7 35	cmpo	|- ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) ) )
37	0 36	wceq	|- _D = ( s e. ~P CC , f e. ( CC ^pm s ) |-> U_ x e. ( ( int ` ( ( TopOpen ` CCfld ) |`t s ) ) ` dom f ) ( { x } X. ( ( z e. ( dom f \ { x } ) |-> ( ( ( f ` z ) - ( f ` x ) ) / ( z - x ) ) ) limCC x ) ) )