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