This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 dfss2 
 |-  ( 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 ) )