Theorem dvsid

Description: Derivative of the identity function on the real or complex numbers. (Contributed by Steve Rodriguez, 11-Nov-2015)

	Ref	Expression
Assertion	dvsid	|- ( S e. { RR , CC } -> ( S _D ( _I |` S ) ) = ( S X. { 1 } ) )

Proof

Step	Hyp	Ref	Expression
1		fnresi	|- ( _I |` CC ) Fn CC
2		rnresi	|- ran ( _I |` CC ) = CC
3	2	eqimssi	|- ran ( _I |` CC ) C_ CC
4		df-f	|- ( ( _I |` CC ) : CC --> CC <-> ( ( _I |` CC ) Fn CC /\ ran ( _I |` CC ) C_ CC ) )
5	1 3 4	mpbir2an	|- ( _I |` CC ) : CC --> CC
6	5	jctr	|- ( S e. { RR , CC } -> ( S e. { RR , CC } /\ ( _I |` CC ) : CC --> CC ) )
7		recnprss	|- ( S e. { RR , CC } -> S C_ CC )
8		dvid	|- ( CC _D ( _I |` CC ) ) = ( CC X. { 1 } )
9	8	dmeqi	|- dom ( CC _D ( _I |` CC ) ) = dom ( CC X. { 1 } )
10		1ex	|- 1 e. _V
11	10	fconst	|- ( CC X. { 1 } ) : CC --> { 1 }
12	11	fdmi	|- dom ( CC X. { 1 } ) = CC
13	9 12	eqtri	|- dom ( CC _D ( _I |` CC ) ) = CC
14	7 13	sseqtrrdi	|- ( S e. { RR , CC } -> S C_ dom ( CC _D ( _I |` CC ) ) )
15		ssid	|- CC C_ CC
16	14 15	jctil	|- ( S e. { RR , CC } -> ( CC C_ CC /\ S C_ dom ( CC _D ( _I |` CC ) ) ) )
17		dvres3	|- ( ( ( S e. { RR , CC } /\ ( _I |` CC ) : CC --> CC ) /\ ( CC C_ CC /\ S C_ dom ( CC _D ( _I |` CC ) ) ) ) -> ( S _D ( ( _I |` CC ) |` S ) ) = ( ( CC _D ( _I |` CC ) ) |` S ) )
18	6 16 17	syl2anc	|- ( S e. { RR , CC } -> ( S _D ( ( _I |` CC ) |` S ) ) = ( ( CC _D ( _I |` CC ) ) |` S ) )
19	7	resabs1d	|- ( S e. { RR , CC } -> ( ( _I |` CC ) |` S ) = ( _I |` S ) )
20	19	oveq2d	|- ( S e. { RR , CC } -> ( S _D ( ( _I |` CC ) |` S ) ) = ( S _D ( _I |` S ) ) )
21	8	reseq1i	|- ( ( CC _D ( _I |` CC ) ) |` S ) = ( ( CC X. { 1 } ) |` S )
22		xpssres	|- ( S C_ CC -> ( ( CC X. { 1 } ) |` S ) = ( S X. { 1 } ) )
23	21 22	syl5eq	|- ( S C_ CC -> ( ( CC _D ( _I |` CC ) ) |` S ) = ( S X. { 1 } ) )
24	7 23	syl	|- ( S e. { RR , CC } -> ( ( CC _D ( _I |` CC ) ) |` S ) = ( S X. { 1 } ) )
25	18 20 24	3eqtr3d	|- ( S e. { RR , CC } -> ( S _D ( _I |` S ) ) = ( S X. { 1 } ) )