Theorem dvmptcj

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

	Ref	Expression
Hypotheses	dvmptcj.a	|- ( ( ph /\ x e. X ) -> A e. CC )
	dvmptcj.b	|- ( ( ph /\ x e. X ) -> B e. V )
	dvmptcj.da	|- ( ph -> ( RR _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
Assertion	dvmptcj	|- ( ph -> ( RR _D ( x e. X |-> ( * ` A ) ) ) = ( x e. X |-> ( * ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvmptcj.a	|- ( ( ph /\ x e. X ) -> A e. CC )
2		dvmptcj.b	|- ( ( ph /\ x e. X ) -> B e. V )
3		dvmptcj.da	|- ( ph -> ( RR _D ( x e. X |-> A ) ) = ( x e. X |-> B ) )
4	1	fmpttd	|- ( ph -> ( x e. X |-> A ) : X --> CC )
5	3	dmeqd	|- ( ph -> dom ( RR _D ( x e. X |-> A ) ) = dom ( x e. X |-> B ) )
6	2	ralrimiva	|- ( ph -> A. x e. X B e. V )
7		dmmptg	|- ( A. x e. X B e. V -> dom ( x e. X |-> B ) = X )
8	6 7	syl	|- ( ph -> dom ( x e. X |-> B ) = X )
9	5 8	eqtrd	|- ( ph -> dom ( RR _D ( x e. X |-> A ) ) = X )
10		dvbsss	|- dom ( RR _D ( x e. X |-> A ) ) C_ RR
11	9 10	eqsstrrdi	|- ( ph -> X C_ RR )
12		dvcj	|- ( ( ( x e. X |-> A ) : X --> CC /\ X C_ RR ) -> ( RR _D ( * o. ( x e. X |-> A ) ) ) = ( * o. ( RR _D ( x e. X |-> A ) ) ) )
13	4 11 12	syl2anc	|- ( ph -> ( RR _D ( * o. ( x e. X |-> A ) ) ) = ( * o. ( RR _D ( x e. X |-> A ) ) ) )
14		cjf	|- * : CC --> CC
15	14	a1i	|- ( ph -> * : CC --> CC )
16	15 1	cofmpt	|- ( ph -> ( * o. ( x e. X |-> A ) ) = ( x e. X |-> ( * ` A ) ) )
17	16	oveq2d	|- ( ph -> ( RR _D ( * o. ( x e. X |-> A ) ) ) = ( RR _D ( x e. X |-> ( * ` A ) ) ) )
18		reelprrecn	|- RR e. { RR , CC }
19	18	a1i	|- ( ph -> RR e. { RR , CC } )
20	19 1 2 3	dvmptcl	|- ( ( ph /\ x e. X ) -> B e. CC )
21	15	feqmptd	|- ( ph -> * = ( y e. CC |-> ( * ` y ) ) )
22		fveq2	|- ( y = B -> ( * ` y ) = ( * ` B ) )
23	20 3 21 22	fmptco	|- ( ph -> ( * o. ( RR _D ( x e. X |-> A ) ) ) = ( x e. X |-> ( * ` B ) ) )
24	13 17 23	3eqtr3d	|- ( ph -> ( RR _D ( x e. X |-> ( * ` A ) ) ) = ( x e. X |-> ( * ` B ) ) )