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

Definition df-dv 19217
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 19213 . 2  class  _D
2 vs . . 3  set  s
3 vf . . 3  set  f
4 cc 8735 . . . 4  class  CC
54cpw 3625 . . 3  class  ~P CC
62cv 1622 . . . 4  class  s
7 cpm 6773 . . . 4  class  ^pm
84, 6, 7co 5858 . . 3  class  ( CC 
^pm  s )
9 vx . . . 4  set  x
103cv 1622 . . . . . 6  class  f
1110cdm 4689 . . . . 5  class  dom  f
12 ccnfld 16377 . . . . . . . 8  classfld
13 ctopn 13326 . . . . . . . 8  class  TopOpen
1412, 13cfv 5255 . . . . . . 7  class  ( TopOpen ` fld )
15 crest 13325 . . . . . . 7  classt
1614, 6, 15co 5858 . . . . . 6  class  ( (
TopOpen ` fld )t  s )
17 cnt 16754 . . . . . 6  class  int
1816, 17cfv 5255 . . . . 5  class  ( int `  ( ( TopOpen ` fld )t  s ) )
1911, 18cfv 5255 . . . 4  class  ( ( int `  ( (
TopOpen ` fld )t  s ) ) `  dom  f )
209cv 1622 . . . . . 6  class  x
2120csn 3640 . . . . 5  class  { x }
22 vz . . . . . . 7  set  z
2311, 21cdif 3149 . . . . . . 7  class  ( dom  f  \  { x } )
2422cv 1622 . . . . . . . . . 10  class  z
2524, 10cfv 5255 . . . . . . . . 9  class  ( f `
 z )
2620, 10cfv 5255 . . . . . . . . 9  class  ( f `
 x )
27 cmin 9037 . . . . . . . . 9  class  -
2825, 26, 27co 5858 . . . . . . . 8  class  ( ( f `  z )  -  ( f `  x ) )
2924, 20, 27co 5858 . . . . . . . 8  class  ( z  -  x )
30 cdiv 9423 . . . . . . . 8  class  /
3128, 29, 30co 5858 . . . . . . 7  class  ( ( ( f `  z
)  -  ( f `
 x ) )  /  ( z  -  x ) )
3222, 23, 31cmpt 4077 . . . . . 6  class  ( z  e.  ( dom  f  \  { x } ) 
|->  ( ( ( f `
 z )  -  ( f `  x
) )  /  (
z  -  x ) ) )
33 climc 19212 . . . . . 6  class lim CC
3432, 20, 33co 5858 . . . . 5  class  ( ( z  e.  ( dom  f  \  { x } )  |->  ( ( ( f `  z
)  -  ( f `
 x ) )  /  ( z  -  x ) ) ) lim
CC  x )
3521, 34cxp 4687 . . . 4  class  ( { x }  X.  (
( z  e.  ( dom  f  \  {
x } )  |->  ( ( ( f `  z )  -  (
f `  x )
)  /  ( z  -  x ) ) ) lim CC  x ) )
369, 19, 35ciun 3905 . . 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 5860 . 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 1623 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  19220  dvfval  19247  dvbsss  19252  perfdvf  19253
  Copyright terms: Public domain W3C validator