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

Metamath Proof Explorer

Theorem dvmptc

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

Ref Expression
Hypotheses dvmptid.1 
|- ( ph -> S e. { RR , CC } )
dvmptc.2 
|- ( ph -> A e. CC )
Assertion dvmptc 
|- ( ph -> ( S _D ( x e. S |-> A ) ) = ( x e. S |-> 0 ) )

Proof

Step Hyp Ref Expression
1 dvmptid.1 
 |-  ( ph -> S e. { RR , CC } )
2 dvmptc.2 
 |-  ( ph -> A e. CC )
3 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
4 3 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
5 toponmax 
 |-  ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> CC e. ( TopOpen ` CCfld ) )
6 4 5 mp1i 
 |-  ( ph -> CC e. ( TopOpen ` CCfld ) )
7 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
8 1 7 syl 
 |-  ( ph -> S C_ CC )
9 dfss2 
 |-  ( S C_ CC <-> ( S i^i CC ) = S )
10 8 9 sylib 
 |-  ( ph -> ( S i^i CC ) = S )
11 2 adantr 
 |-  ( ( ph /\ x e. CC ) -> A e. CC )
12 0cnd 
 |-  ( ( ph /\ x e. CC ) -> 0 e. CC )
13 dvconst 
 |-  ( A e. CC -> ( CC _D ( CC X. { A } ) ) = ( CC X. { 0 } ) )
14 2 13 syl 
 |-  ( ph -> ( CC _D ( CC X. { A } ) ) = ( CC X. { 0 } ) )
15 fconstmpt 
 |-  ( CC X. { A } ) = ( x e. CC |-> A )
16 15 oveq2i 
 |-  ( CC _D ( CC X. { A } ) ) = ( CC _D ( x e. CC |-> A ) )
17 fconstmpt 
 |-  ( CC X. { 0 } ) = ( x e. CC |-> 0 )
18 14 16 17 3eqtr3g 
 |-  ( ph -> ( CC _D ( x e. CC |-> A ) ) = ( x e. CC |-> 0 ) )
19 3 1 6 10 11 12 18 dvmptres3 
 |-  ( ph -> ( S _D ( x e. S |-> A ) ) = ( x e. S |-> 0 ) )