Metamath Proof Explorer

Theorem dvcj

Description: The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr . (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Assertion dvcj 
|- ( ( F : X --> CC /\ X C_ RR ) -> ( RR _D ( * o. F ) ) = ( * o. ( RR _D F ) ) )

Proof

Step Hyp Ref Expression
1 dvf 
 |-  ( RR _D ( * o. F ) ) : dom ( RR _D ( * o. F ) ) --> CC
2 ffun 
 |-  ( ( RR _D ( * o. F ) ) : dom ( RR _D ( * o. F ) ) --> CC -> Fun ( RR _D ( * o. F ) ) )
3 1 2 ax-mp 
 |-  Fun ( RR _D ( * o. F ) )
4 simpll 
 |-  ( ( ( F : X --> CC /\ X C_ RR ) /\ x e. dom ( RR _D F ) ) -> F : X --> CC )
5 simplr 
 |-  ( ( ( F : X --> CC /\ X C_ RR ) /\ x e. dom ( RR _D F ) ) -> X C_ RR )
6 simpr 
 |-  ( ( ( F : X --> CC /\ X C_ RR ) /\ x e. dom ( RR _D F ) ) -> x e. dom ( RR _D F ) )
7 4 5 6 dvcjbr 
 |-  ( ( ( F : X --> CC /\ X C_ RR ) /\ x e. dom ( RR _D F ) ) -> x ( RR _D ( * o. F ) ) ( * ` ( ( RR _D F ) ` x ) ) )
8 funbrfv 
 |-  ( Fun ( RR _D ( * o. F ) ) -> ( x ( RR _D ( * o. F ) ) ( * ` ( ( RR _D F ) ` x ) ) -> ( ( RR _D ( * o. F ) ) ` x ) = ( * ` ( ( RR _D F ) ` x ) ) ) )
9 3 7 8 mpsyl 
 |-  ( ( ( F : X --> CC /\ X C_ RR ) /\ x e. dom ( RR _D F ) ) -> ( ( RR _D ( * o. F ) ) ` x ) = ( * ` ( ( RR _D F ) ` x ) ) )
10 9 mpteq2dva 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> ( x e. dom ( RR _D F ) |-> ( ( RR _D ( * o. F ) ) ` x ) ) = ( x e. dom ( RR _D F ) |-> ( * ` ( ( RR _D F ) ` x ) ) ) )
11 cjf 
 |-  * : CC --> CC
12 fco 
 |-  ( ( * : CC --> CC /\ F : X --> CC ) -> ( * o. F ) : X --> CC )
13 11 12 mpan 
 |-  ( F : X --> CC -> ( * o. F ) : X --> CC )
14 13 ad2antrr 
 |-  ( ( ( F : X --> CC /\ X C_ RR ) /\ x e. dom ( RR _D ( * o. F ) ) ) -> ( * o. F ) : X --> CC )
15 simplr 
 |-  ( ( ( F : X --> CC /\ X C_ RR ) /\ x e. dom ( RR _D ( * o. F ) ) ) -> X C_ RR )
16 simpr 
 |-  ( ( ( F : X --> CC /\ X C_ RR ) /\ x e. dom ( RR _D ( * o. F ) ) ) -> x e. dom ( RR _D ( * o. F ) ) )
17 14 15 16 dvcjbr 
 |-  ( ( ( F : X --> CC /\ X C_ RR ) /\ x e. dom ( RR _D ( * o. F ) ) ) -> x ( RR _D ( * o. ( * o. F ) ) ) ( * ` ( ( RR _D ( * o. F ) ) ` x ) ) )
18 vex 
 |-  x e. _V
19 fvex 
 |-  ( * ` ( ( RR _D ( * o. F ) ) ` x ) ) e. _V
20 18 19 breldm 
 |-  ( x ( RR _D ( * o. ( * o. F ) ) ) ( * ` ( ( RR _D ( * o. F ) ) ` x ) ) -> x e. dom ( RR _D ( * o. ( * o. F ) ) ) )
21 17 20 syl 
 |-  ( ( ( F : X --> CC /\ X C_ RR ) /\ x e. dom ( RR _D ( * o. F ) ) ) -> x e. dom ( RR _D ( * o. ( * o. F ) ) ) )
22 21 ex 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> ( x e. dom ( RR _D ( * o. F ) ) -> x e. dom ( RR _D ( * o. ( * o. F ) ) ) ) )
23 22 ssrdv 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> dom ( RR _D ( * o. F ) ) C_ dom ( RR _D ( * o. ( * o. F ) ) ) )
24 ffvelrn 
 |-  ( ( F : X --> CC /\ x e. X ) -> ( F ` x ) e. CC )
25 24 adantlr 
 |-  ( ( ( F : X --> CC /\ X C_ RR ) /\ x e. X ) -> ( F ` x ) e. CC )
26 25 cjcjd 
 |-  ( ( ( F : X --> CC /\ X C_ RR ) /\ x e. X ) -> ( * ` ( * ` ( F ` x ) ) ) = ( F ` x ) )
27 26 mpteq2dva 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> ( x e. X |-> ( * ` ( * ` ( F ` x ) ) ) ) = ( x e. X |-> ( F ` x ) ) )
28 25 cjcld 
 |-  ( ( ( F : X --> CC /\ X C_ RR ) /\ x e. X ) -> ( * ` ( F ` x ) ) e. CC )
29 simpl 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> F : X --> CC )
30 29 feqmptd 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> F = ( x e. X |-> ( F ` x ) ) )
31 11 a1i 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> * : CC --> CC )
32 31 feqmptd 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> * = ( y e. CC |-> ( * ` y ) ) )
33 fveq2 
 |-  ( y = ( F ` x ) -> ( * ` y ) = ( * ` ( F ` x ) ) )
34 25 30 32 33 fmptco 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> ( * o. F ) = ( x e. X |-> ( * ` ( F ` x ) ) ) )
35 fveq2 
 |-  ( y = ( * ` ( F ` x ) ) -> ( * ` y ) = ( * ` ( * ` ( F ` x ) ) ) )
36 28 34 32 35 fmptco 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> ( * o. ( * o. F ) ) = ( x e. X |-> ( * ` ( * ` ( F ` x ) ) ) ) )
37 27 36 30 3eqtr4d 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> ( * o. ( * o. F ) ) = F )
38 37 oveq2d 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> ( RR _D ( * o. ( * o. F ) ) ) = ( RR _D F ) )
39 38 dmeqd 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> dom ( RR _D ( * o. ( * o. F ) ) ) = dom ( RR _D F ) )
40 23 39 sseqtrd 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> dom ( RR _D ( * o. F ) ) C_ dom ( RR _D F ) )
41 fvex 
 |-  ( * ` ( ( RR _D F ) ` x ) ) e. _V
42 18 41 breldm 
 |-  ( x ( RR _D ( * o. F ) ) ( * ` ( ( RR _D F ) ` x ) ) -> x e. dom ( RR _D ( * o. F ) ) )
43 7 42 syl 
 |-  ( ( ( F : X --> CC /\ X C_ RR ) /\ x e. dom ( RR _D F ) ) -> x e. dom ( RR _D ( * o. F ) ) )
44 40 43 eqelssd 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> dom ( RR _D ( * o. F ) ) = dom ( RR _D F ) )
45 44 feq2d 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> ( ( RR _D ( * o. F ) ) : dom ( RR _D ( * o. F ) ) --> CC <-> ( RR _D ( * o. F ) ) : dom ( RR _D F ) --> CC ) )
46 1 45 mpbii 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> ( RR _D ( * o. F ) ) : dom ( RR _D F ) --> CC )
47 46 feqmptd 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> ( RR _D ( * o. F ) ) = ( x e. dom ( RR _D F ) |-> ( ( RR _D ( * o. F ) ) ` x ) ) )
48 dvf 
 |-  ( RR _D F ) : dom ( RR _D F ) --> CC
49 48 ffvelrni 
 |-  ( x e. dom ( RR _D F ) -> ( ( RR _D F ) ` x ) e. CC )
50 49 adantl 
 |-  ( ( ( F : X --> CC /\ X C_ RR ) /\ x e. dom ( RR _D F ) ) -> ( ( RR _D F ) ` x ) e. CC )
51 48 a1i 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> CC )
52 51 feqmptd 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> ( RR _D F ) = ( x e. dom ( RR _D F ) |-> ( ( RR _D F ) ` x ) ) )
53 fveq2 
 |-  ( y = ( ( RR _D F ) ` x ) -> ( * ` y ) = ( * ` ( ( RR _D F ) ` x ) ) )
54 50 52 32 53 fmptco 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> ( * o. ( RR _D F ) ) = ( x e. dom ( RR _D F ) |-> ( * ` ( ( RR _D F ) ` x ) ) ) )
55 10 47 54 3eqtr4d 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> ( RR _D ( * o. F ) ) = ( * o. ( RR _D F ) ) )