This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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