Theorem dvmptid

Description: Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypothesis	dvmptid.1	|- ( ph -> S e. { RR , CC } )
Assertion	dvmptid	|- ( ph -> ( S _D ( x e. S |-> x ) ) = ( x e. S |-> 1 ) )

Proof

Step	Hyp	Ref	Expression
1		dvmptid.1	|- ( ph -> S e. { RR , CC } )
2		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3	2	cnfldtopon	|- ( TopOpen ` CCfld ) e. ( TopOn ` CC )
4		toponmax	|- ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> CC e. ( TopOpen ` CCfld ) )
5	3 4	mp1i	|- ( ph -> CC e. ( TopOpen ` CCfld ) )
6		recnprss	|- ( S e. { RR , CC } -> S C_ CC )
7	1 6	syl	|- ( ph -> S C_ CC )
8		df-ss	|- ( S C_ CC <-> ( S i^i CC ) = S )
9	7 8	sylib	|- ( ph -> ( S i^i CC ) = S )
10		simpr	|- ( ( ph /\ x e. CC ) -> x e. CC )
11		1cnd	|- ( ( ph /\ x e. CC ) -> 1 e. CC )
12		mptresid	|- ( _I |` CC ) = ( x e. CC |-> x )
13	12	eqcomi	|- ( x e. CC |-> x ) = ( _I |` CC )
14	13	oveq2i	|- ( CC _D ( x e. CC |-> x ) ) = ( CC _D ( _I |` CC ) )
15		dvid	|- ( CC _D ( _I |` CC ) ) = ( CC X. { 1 } )
16		fconstmpt	|- ( CC X. { 1 } ) = ( x e. CC |-> 1 )
17	14 15 16	3eqtri	|- ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 )
18	17	a1i	|- ( ph -> ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 ) )
19	2 1 5 9 10 11 18	dvmptres3	|- ( ph -> ( S _D ( x e. S |-> x ) ) = ( x e. S |-> 1 ) )