MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-dv Unicode version

Definition df-dv 19707
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
StepHypRef Expression
1 cdv 19703 . 2  class  _D
2 vs . . 3  set  s
3 vf . . 3  set  f
4 cc 8944 . . . 4  class  CC
54cpw 3759 . . 3  class  ~P CC
62cv 1648 . . . 4  class  s
7 cpm 6978 . . . 4  class  ^pm
84, 6, 7co 6040 . . 3  class  ( CC 
^pm  s )
9 vx . . . 4  set  x
103cv 1648 . . . . . 6  class  f
1110cdm 4837 . . . . 5  class  dom  f
12 ccnfld 16658 . . . . . . . 8  classfld
13 ctopn 13604 . . . . . . . 8  class  TopOpen
1412, 13cfv 5413 . . . . . . 7  class  ( TopOpen ` fld )
15 crest 13603 . . . . . . 7  classt
1614, 6, 15co 6040 . . . . . 6  class  ( (
TopOpen ` fld )t  s )
17 cnt 17036 . . . . . 6  class  int
1816, 17cfv 5413 . . . . 5  class  ( int `  ( ( TopOpen ` fld )t  s ) )
1911, 18cfv 5413 . . . 4  class  ( ( int `  ( (
TopOpen ` fld )t  s ) ) `  dom  f )
209cv 1648 . . . . . 6  class  x
2120csn 3774 . . . . 5  class  { x }
22 vz . . . . . . 7  set  z
2311, 21cdif 3277 . . . . . . 7  class  ( dom  f  \  { x } )
2422cv 1648 . . . . . . . . . 10  class  z
2524, 10cfv 5413 . . . . . . . . 9  class  ( f `
 z )
2620, 10cfv 5413 . . . . . . . . 9  class  ( f `
 x )
27 cmin 9247 . . . . . . . . 9  class  -
2825, 26, 27co 6040 . . . . . . . 8  class  ( ( f `  z )  -  ( f `  x ) )
2924, 20, 27co 6040 . . . . . . . 8  class  ( z  -  x )
30 cdiv 9633 . . . . . . . 8  class  /
3128, 29, 30co 6040 . . . . . . 7  class  ( ( ( f `  z
)  -  ( f `
 x ) )  /  ( z  -  x ) )
3222, 23, 31cmpt 4226 . . . . . 6  class  ( z  e.  ( dom  f  \  { x } ) 
|->  ( ( ( f `
 z )  -  ( f `  x
) )  /  (
z  -  x ) ) )
33 climc 19702 . . . . . 6  class lim CC
3432, 20, 33co 6040 . . . . 5  class  ( ( z  e.  ( dom  f  \  { x } )  |->  ( ( ( f `  z
)  -  ( f `
 x ) )  /  ( z  -  x ) ) ) lim
CC  x )
3521, 34cxp 4835 . . . 4  class  ( { x }  X.  (
( z  e.  ( dom  f  \  {
x } )  |->  ( ( ( f `  z )  -  (
f `  x )
)  /  ( z  -  x ) ) ) lim CC  x ) )
369, 19, 35ciun 4053 . . 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
) )
372, 3, 5, 8, 36cmpt2 6042 . 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 ) ) )
381, 37wceq 1649 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
) ) )
Colors of variables: wff set class
This definition is referenced by:  reldv  19710  dvfval  19737  dvbsss  19742  perfdvf  19743
  Copyright terms: Public domain W3C validator