Metamath Proof Explorer

Theorem dvmptre

Description: Function-builder for derivative, real 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 dvmptre 
|- ( ph -> ( RR _D ( x e. X |-> ( Re ` A ) ) ) = ( x e. X |-> ( Re ` 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 addcld 
 |-  ( ( 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 addcld 
 |-  ( ( 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 dvmptadd 
 |-  ( ph -> ( RR _D ( x e. X |-> ( A + ( * ` A ) ) ) ) = ( x e. X |-> ( B + ( * ` B ) ) ) )
13 halfcn 
 |-  ( 1 / 2 ) e. CC
14 13 a1i 
 |-  ( ph -> ( 1 / 2 ) e. CC )
15 5 7 10 12 14 dvmptcmul 
 |-  ( ph -> ( RR _D ( x e. X |-> ( ( 1 / 2 ) x. ( A + ( * ` A ) ) ) ) ) = ( x e. X |-> ( ( 1 / 2 ) x. ( B + ( * ` B ) ) ) ) )
16 reval 
 |-  ( A e. CC -> ( Re ` A ) = ( ( A + ( * ` A ) ) / 2 ) )
17 1 16 syl 
 |-  ( ( ph /\ x e. X ) -> ( Re ` A ) = ( ( A + ( * ` A ) ) / 2 ) )
18 2cn 
 |-  2 e. CC
19 2ne0 
 |-  2 =/= 0
20 divrec2 
 |-  ( ( ( A + ( * ` A ) ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( A + ( * ` A ) ) / 2 ) = ( ( 1 / 2 ) x. ( A + ( * ` A ) ) ) )
21 18 19 20 mp3an23 
 |-  ( ( A + ( * ` A ) ) e. CC -> ( ( A + ( * ` A ) ) / 2 ) = ( ( 1 / 2 ) x. ( A + ( * ` A ) ) ) )
22 7 21 syl 
 |-  ( ( ph /\ x e. X ) -> ( ( A + ( * ` A ) ) / 2 ) = ( ( 1 / 2 ) x. ( A + ( * ` A ) ) ) )
23 17 22 eqtrd 
 |-  ( ( ph /\ x e. X ) -> ( Re ` A ) = ( ( 1 / 2 ) x. ( A + ( * ` A ) ) ) )
24 23 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( Re ` A ) ) = ( x e. X |-> ( ( 1 / 2 ) x. ( A + ( * ` A ) ) ) ) )
25 24 oveq2d 
 |-  ( ph -> ( RR _D ( x e. X |-> ( Re ` A ) ) ) = ( RR _D ( x e. X |-> ( ( 1 / 2 ) x. ( A + ( * ` A ) ) ) ) ) )
26 reval 
 |-  ( B e. CC -> ( Re ` B ) = ( ( B + ( * ` B ) ) / 2 ) )
27 8 26 syl 
 |-  ( ( ph /\ x e. X ) -> ( Re ` B ) = ( ( B + ( * ` B ) ) / 2 ) )
28 divrec2 
 |-  ( ( ( B + ( * ` B ) ) e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( B + ( * ` B ) ) / 2 ) = ( ( 1 / 2 ) x. ( B + ( * ` B ) ) ) )
29 18 19 28 mp3an23 
 |-  ( ( B + ( * ` B ) ) e. CC -> ( ( B + ( * ` B ) ) / 2 ) = ( ( 1 / 2 ) x. ( B + ( * ` B ) ) ) )
30 10 29 syl 
 |-  ( ( ph /\ x e. X ) -> ( ( B + ( * ` B ) ) / 2 ) = ( ( 1 / 2 ) x. ( B + ( * ` B ) ) ) )
31 27 30 eqtrd 
 |-  ( ( ph /\ x e. X ) -> ( Re ` B ) = ( ( 1 / 2 ) x. ( B + ( * ` B ) ) ) )
32 31 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( Re ` B ) ) = ( x e. X |-> ( ( 1 / 2 ) x. ( B + ( * ` B ) ) ) ) )
33 15 25 32 3eqtr4d 
 |-  ( ph -> ( RR _D ( x e. X |-> ( Re ` A ) ) ) = ( x e. X |-> ( Re ` B ) ) )