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 = ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdv ⊢ D
1 vs ⊢ 𝑠
2 cc ⊢ ℂ
3 2 cpw ⊢ 𝒫 ℂ
4 vf ⊢ 𝑓
5 cpm ⊢ ↑pm
6 1 cv ⊢ 𝑠
7 2 6 5 co ⊢ ( ℂ ↑pm 𝑠 )
8 vx ⊢ 𝑥
9 cnt ⊢ int
10 ctopn ⊢ TopOpen
11 ccnfld ⊢ ℂfld
12 11 10 cfv ⊢ ( TopOpen ‘ ℂfld )
13 crest ⊢ ↾t
14 12 6 13 co ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 )
15 14 9 cfv ⊢ ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) )
16 4 cv ⊢ 𝑓
17 16 cdm ⊢ dom 𝑓
18 17 15 cfv ⊢ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 )
19 8 cv ⊢ 𝑥
20 19 csn ⊢ { 𝑥 }
21 vz ⊢ 𝑧
22 17 20 cdif ⊢ ( dom 𝑓 ∖ { 𝑥 } )
23 21 cv ⊢ 𝑧
24 23 16 cfv ⊢ ( 𝑓 ‘ 𝑧 )
25 cmin ⊢ −
26 19 16 cfv ⊢ ( 𝑓 ‘ 𝑥 )
27 24 26 25 co ⊢ ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) )
28 cdiv ⊢ /
29 23 19 25 co ⊢ ( 𝑧 − 𝑥 )
30 27 29 28 co ⊢ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) )
31 21 22 30 cmpt ⊢ ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) )
32 climc ⊢ limℂ
33 31 19 32 co ⊢ ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 )
34 20 33 cxp ⊢ ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) )
35 8 18 34 ciun ⊢ ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) )
36 1 4 3 7 35 cmpo ⊢ ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) )
37 0 36 wceq ⊢ D = ( 𝑠 ∈ 𝒫 ℂ , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ ∪ 𝑥 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑠 ) ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( dom 𝑓 ∖ { 𝑥 } ) ↦ ( ( ( 𝑓 ‘ 𝑧 ) − ( 𝑓 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) )