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

Metamath Proof Explorer

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