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

Definition df-dv 19211
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 19207 . 2  class  _D
2 vs . . 3  set  s
3 vf . . 3  set  f
4 cc 8730 . . . 4  class  CC
54cpw 3626 . . 3  class  ~P CC
62cv 1623 . . . 4  class  s
7 cpm 6768 . . . 4  class  ^pm
84, 6, 7co 5819 . . 3  class  ( CC 
^pm  s )
9 vx . . . 4  set  x
103cv 1623 . . . . . 6  class  f
1110cdm 4688 . . . . 5  class  dom  f
12 ccnfld 16371 . . . . . . . 8  classfld
13 ctopn 13320 . . . . . . . 8  class  TopOpen
1412, 13cfv 5221 . . . . . . 7  class  ( TopOpen ` fld )
15 crest 13319 . . . . . . 7  classt
1614, 6, 15co 5819 . . . . . 6  class  ( (
TopOpen ` fld )t  s )
17 cnt 16748 . . . . . 6  class  int
1816, 17cfv 5221 . . . . 5  class  ( int `  ( ( TopOpen ` fld )t  s ) )
1911, 18cfv 5221 . . . 4  class  ( ( int `  ( (
TopOpen ` fld )t  s ) ) `  dom  f )
209cv 1623 . . . . . 6  class  x
2120csn 3641 . . . . 5  class  { x }
22 vz . . . . . . 7  set  z
2311, 21cdif 3150 . . . . . . 7  class  ( dom  f  \  { x } )
2422cv 1623 . . . . . . . . . 10  class  z
2524, 10cfv 5221 . . . . . . . . 9  class  ( f `
 z )
2620, 10cfv 5221 . . . . . . . . 9  class  ( f `
 x )
27 cmin 9032 . . . . . . . . 9  class  -
2825, 26, 27co 5819 . . . . . . . 8  class  ( ( f `  z )  -  ( f `  x ) )
2924, 20, 27co 5819 . . . . . . . 8  class  ( z  -  x )
30 cdiv 9418 . . . . . . . 8  class  /
3128, 29, 30co 5819 . . . . . . 7  class  ( ( ( f `  z
)  -  ( f `
 x ) )  /  ( z  -  x ) )
3222, 23, 31cmpt 4078 . . . . . 6  class  ( z  e.  ( dom  f  \  { x } ) 
|->  ( ( ( f `
 z )  -  ( f `  x
) )  /  (
z  -  x ) ) )
33 climc 19206 . . . . . 6  class lim CC
3432, 20, 33co 5819 . . . . 5  class  ( ( z  e.  ( dom  f  \  { x } )  |->  ( ( ( f `  z
)  -  ( f `
 x ) )  /  ( z  -  x ) ) ) lim
CC  x )
3521, 34cxp 4686 . . . 4  class  ( { x }  X.  (
( z  e.  ( dom  f  \  {
x } )  |->  ( ( ( f `  z )  -  (
f `  x )
)  /  ( z  -  x ) ) ) lim CC  x ) )
369, 19, 35ciun 3906 . . 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 5821 . 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 1624 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  19214  dvfval  19241  dvbsss  19246  perfdvf  19247
  Copyright terms: Public domain W3C validator