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