Metamath Proof Explorer

Theorem dvmptim

Description: Function-builder for derivative, imaginary part. (Contributed by Mario Carneiro, 1-Sep-2014)

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 dvmptim 
|- ( ph -> ( RR _D ( x e. X |-> ( Im ` A ) ) ) = ( x e. X |-> ( Im ` 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 reelprrecn 
 |-  RR e. { RR , CC }
5 4 a1i 
 |-  ( ph -> RR e. { RR , CC } )
6 1 cjcld 
 |-  ( ( ph /\ x e. X ) -> ( * ` A ) e. CC )
7 1 6 subcld 
 |-  ( ( ph /\ x e. X ) -> ( A - ( * ` A ) ) e. CC )
8 5 1 2 3 dvmptcl 
 |-  ( ( ph /\ x e. X ) -> B e. CC )
9 8 cjcld 
 |-  ( ( ph /\ x e. X ) -> ( * ` B ) e. CC )
10 8 9 subcld 
 |-  ( ( ph /\ x e. X ) -> ( B - ( * ` B ) ) e. CC )
11 1 2 3 dvmptcj 
 |-  ( ph -> ( RR _D ( x e. X |-> ( * ` A ) ) ) = ( x e. X |-> ( * ` B ) ) )
12 5 1 2 3 6 9 11 dvmptsub 
 |-  ( ph -> ( RR _D ( x e. X |-> ( A - ( * ` A ) ) ) ) = ( x e. X |-> ( B - ( * ` B ) ) ) )
13 2mulicn 
 |-  ( 2 x. _i ) e. CC
14 2muline0 
 |-  ( 2 x. _i ) =/= 0
15 13 14 reccli 
 |-  ( 1 / ( 2 x. _i ) ) e. CC
16 15 a1i 
 |-  ( ph -> ( 1 / ( 2 x. _i ) ) e. CC )
17 5 7 10 12 16 dvmptcmul 
 |-  ( ph -> ( RR _D ( x e. X |-> ( ( 1 / ( 2 x. _i ) ) x. ( A - ( * ` A ) ) ) ) ) = ( x e. X |-> ( ( 1 / ( 2 x. _i ) ) x. ( B - ( * ` B ) ) ) ) )
18 imval2 
 |-  ( A e. CC -> ( Im ` A ) = ( ( A - ( * ` A ) ) / ( 2 x. _i ) ) )
19 1 18 syl 
 |-  ( ( ph /\ x e. X ) -> ( Im ` A ) = ( ( A - ( * ` A ) ) / ( 2 x. _i ) ) )
20 divrec2 
 |-  ( ( ( A - ( * ` A ) ) e. CC /\ ( 2 x. _i ) e. CC /\ ( 2 x. _i ) =/= 0 ) -> ( ( A - ( * ` A ) ) / ( 2 x. _i ) ) = ( ( 1 / ( 2 x. _i ) ) x. ( A - ( * ` A ) ) ) )
21 13 14 20 mp3an23 
 |-  ( ( A - ( * ` A ) ) e. CC -> ( ( A - ( * ` A ) ) / ( 2 x. _i ) ) = ( ( 1 / ( 2 x. _i ) ) x. ( A - ( * ` A ) ) ) )
22 7 21 syl 
 |-  ( ( ph /\ x e. X ) -> ( ( A - ( * ` A ) ) / ( 2 x. _i ) ) = ( ( 1 / ( 2 x. _i ) ) x. ( A - ( * ` A ) ) ) )
23 19 22 eqtrd 
 |-  ( ( ph /\ x e. X ) -> ( Im ` A ) = ( ( 1 / ( 2 x. _i ) ) x. ( A - ( * ` A ) ) ) )
24 23 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( Im ` A ) ) = ( x e. X |-> ( ( 1 / ( 2 x. _i ) ) x. ( A - ( * ` A ) ) ) ) )
25 24 oveq2d 
 |-  ( ph -> ( RR _D ( x e. X |-> ( Im ` A ) ) ) = ( RR _D ( x e. X |-> ( ( 1 / ( 2 x. _i ) ) x. ( A - ( * ` A ) ) ) ) ) )
26 imval2 
 |-  ( B e. CC -> ( Im ` B ) = ( ( B - ( * ` B ) ) / ( 2 x. _i ) ) )
27 8 26 syl 
 |-  ( ( ph /\ x e. X ) -> ( Im ` B ) = ( ( B - ( * ` B ) ) / ( 2 x. _i ) ) )
28 divrec2 
 |-  ( ( ( B - ( * ` B ) ) e. CC /\ ( 2 x. _i ) e. CC /\ ( 2 x. _i ) =/= 0 ) -> ( ( B - ( * ` B ) ) / ( 2 x. _i ) ) = ( ( 1 / ( 2 x. _i ) ) x. ( B - ( * ` B ) ) ) )
29 13 14 28 mp3an23 
 |-  ( ( B - ( * ` B ) ) e. CC -> ( ( B - ( * ` B ) ) / ( 2 x. _i ) ) = ( ( 1 / ( 2 x. _i ) ) x. ( B - ( * ` B ) ) ) )
30 10 29 syl 
 |-  ( ( ph /\ x e. X ) -> ( ( B - ( * ` B ) ) / ( 2 x. _i ) ) = ( ( 1 / ( 2 x. _i ) ) x. ( B - ( * ` B ) ) ) )
31 27 30 eqtrd 
 |-  ( ( ph /\ x e. X ) -> ( Im ` B ) = ( ( 1 / ( 2 x. _i ) ) x. ( B - ( * ` B ) ) ) )
32 31 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( Im ` B ) ) = ( x e. X |-> ( ( 1 / ( 2 x. _i ) ) x. ( B - ( * ` B ) ) ) ) )
33 17 25 32 3eqtr4d 
 |-  ( ph -> ( RR _D ( x e. X |-> ( Im ` A ) ) ) = ( x e. X |-> ( Im ` B ) ) )