Metamath Proof Explorer

Theorem dvcjbr

Description: The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj . (This doesn't follow from dvcobr because * is not a function on the reals, and even if we used complex derivatives, * is not complex-differentiable.) (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Hypotheses dvcj.f 
|- ( ph -> F : X --> CC )
dvcj.x 
|- ( ph -> X C_ RR )
dvcj.c 
|- ( ph -> C e. dom ( RR _D F ) )
Assertion dvcjbr 
|- ( ph -> C ( RR _D ( * o. F ) ) ( * ` ( ( RR _D F ) ` C ) ) )

Proof

Step Hyp Ref Expression
1 dvcj.f 
 |-  ( ph -> F : X --> CC )
2 dvcj.x 
 |-  ( ph -> X C_ RR )
3 dvcj.c 
 |-  ( ph -> C e. dom ( RR _D F ) )
4 ax-resscn 
 |-  RR C_ CC
5 4 a1i 
 |-  ( ph -> RR C_ CC )
6 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
7 6 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
8 5 1 2 7 6 dvbssntr 
 |-  ( ph -> dom ( RR _D F ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` X ) )
9 8 3 sseldd 
 |-  ( ph -> C e. ( ( int ` ( topGen ` ran (,) ) ) ` X ) )
10 2 4 sstrdi 
 |-  ( ph -> X C_ CC )
11 4 a1i 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> RR C_ CC )
12 simpl 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> F : X --> CC )
13 simpr 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> X C_ RR )
14 11 12 13 dvbss 
 |-  ( ( F : X --> CC /\ X C_ RR ) -> dom ( RR _D F ) C_ X )
15 1 2 14 syl2anc 
 |-  ( ph -> dom ( RR _D F ) C_ X )
16 15 3 sseldd 
 |-  ( ph -> C e. X )
17 1 10 16 dvlem 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( ( ( F ` x ) - ( F ` C ) ) / ( x - C ) ) e. CC )
18 17 fmpttd 
 |-  ( ph -> ( x e. ( X \ { C } ) |-> ( ( ( F ` x ) - ( F ` C ) ) / ( x - C ) ) ) : ( X \ { C } ) --> CC )
19 ssidd 
 |-  ( ph -> CC C_ CC )
20 6 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
21 20 toponrestid 
 |-  ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
22 dvf 
 |-  ( RR _D F ) : dom ( RR _D F ) --> CC
23 ffun 
 |-  ( ( RR _D F ) : dom ( RR _D F ) --> CC -> Fun ( RR _D F ) )
24 funfvbrb 
 |-  ( Fun ( RR _D F ) -> ( C e. dom ( RR _D F ) <-> C ( RR _D F ) ( ( RR _D F ) ` C ) ) )
25 22 23 24 mp2b 
 |-  ( C e. dom ( RR _D F ) <-> C ( RR _D F ) ( ( RR _D F ) ` C ) )
26 3 25 sylib 
 |-  ( ph -> C ( RR _D F ) ( ( RR _D F ) ` C ) )
27 eqid 
 |-  ( x e. ( X \ { C } ) |-> ( ( ( F ` x ) - ( F ` C ) ) / ( x - C ) ) ) = ( x e. ( X \ { C } ) |-> ( ( ( F ` x ) - ( F ` C ) ) / ( x - C ) ) )
28 7 6 27 5 1 2 eldv 
 |-  ( ph -> ( C ( RR _D F ) ( ( RR _D F ) ` C ) <-> ( C e. ( ( int ` ( topGen ` ran (,) ) ) ` X ) /\ ( ( RR _D F ) ` C ) e. ( ( x e. ( X \ { C } ) |-> ( ( ( F ` x ) - ( F ` C ) ) / ( x - C ) ) ) limCC C ) ) ) )
29 26 28 mpbid 
 |-  ( ph -> ( C e. ( ( int ` ( topGen ` ran (,) ) ) ` X ) /\ ( ( RR _D F ) ` C ) e. ( ( x e. ( X \ { C } ) |-> ( ( ( F ` x ) - ( F ` C ) ) / ( x - C ) ) ) limCC C ) ) )
30 29 simprd 
 |-  ( ph -> ( ( RR _D F ) ` C ) e. ( ( x e. ( X \ { C } ) |-> ( ( ( F ` x ) - ( F ` C ) ) / ( x - C ) ) ) limCC C ) )
31 cjcncf 
 |-  * e. ( CC -cn-> CC )
32 6 cncfcn1 
 |-  ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
33 31 32 eleqtri 
 |-  * e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) )
34 22 ffvelrni 
 |-  ( C e. dom ( RR _D F ) -> ( ( RR _D F ) ` C ) e. CC )
35 3 34 syl 
 |-  ( ph -> ( ( RR _D F ) ` C ) e. CC )
36 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
37 36 cncnpi 
 |-  ( ( * e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) /\ ( ( RR _D F ) ` C ) e. CC ) -> * e. ( ( ( TopOpen ` CCfld ) CnP ( TopOpen ` CCfld ) ) ` ( ( RR _D F ) ` C ) ) )
38 33 35 37 sylancr 
 |-  ( ph -> * e. ( ( ( TopOpen ` CCfld ) CnP ( TopOpen ` CCfld ) ) ` ( ( RR _D F ) ` C ) ) )
39 18 19 6 21 30 38 limccnp 
 |-  ( ph -> ( * ` ( ( RR _D F ) ` C ) ) e. ( ( * o. ( x e. ( X \ { C } ) |-> ( ( ( F ` x ) - ( F ` C ) ) / ( x - C ) ) ) ) limCC C ) )
40 cjf 
 |-  * : CC --> CC
41 40 a1i 
 |-  ( ph -> * : CC --> CC )
42 41 17 cofmpt 
 |-  ( ph -> ( * o. ( x e. ( X \ { C } ) |-> ( ( ( F ` x ) - ( F ` C ) ) / ( x - C ) ) ) ) = ( x e. ( X \ { C } ) |-> ( * ` ( ( ( F ` x ) - ( F ` C ) ) / ( x - C ) ) ) ) )
43 1 adantr 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> F : X --> CC )
44 eldifi 
 |-  ( x e. ( X \ { C } ) -> x e. X )
45 44 adantl 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> x e. X )
46 43 45 ffvelrnd 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( F ` x ) e. CC )
47 1 16 ffvelrnd 
 |-  ( ph -> ( F ` C ) e. CC )
48 47 adantr 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( F ` C ) e. CC )
49 46 48 subcld 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( ( F ` x ) - ( F ` C ) ) e. CC )
50 2 sselda 
 |-  ( ( ph /\ x e. X ) -> x e. RR )
51 44 50 sylan2 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> x e. RR )
52 2 16 sseldd 
 |-  ( ph -> C e. RR )
53 52 adantr 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> C e. RR )
54 51 53 resubcld 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( x - C ) e. RR )
55 54 recnd 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( x - C ) e. CC )
56 51 recnd 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> x e. CC )
57 53 recnd 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> C e. CC )
58 eldifsni 
 |-  ( x e. ( X \ { C } ) -> x =/= C )
59 58 adantl 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> x =/= C )
60 56 57 59 subne0d 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( x - C ) =/= 0 )
61 49 55 60 cjdivd 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( * ` ( ( ( F ` x ) - ( F ` C ) ) / ( x - C ) ) ) = ( ( * ` ( ( F ` x ) - ( F ` C ) ) ) / ( * ` ( x - C ) ) ) )
62 cjsub 
 |-  ( ( ( F ` x ) e. CC /\ ( F ` C ) e. CC ) -> ( * ` ( ( F ` x ) - ( F ` C ) ) ) = ( ( * ` ( F ` x ) ) - ( * ` ( F ` C ) ) ) )
63 46 48 62 syl2anc 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( * ` ( ( F ` x ) - ( F ` C ) ) ) = ( ( * ` ( F ` x ) ) - ( * ` ( F ` C ) ) ) )
64 fvco3 
 |-  ( ( F : X --> CC /\ x e. X ) -> ( ( * o. F ) ` x ) = ( * ` ( F ` x ) ) )
65 1 44 64 syl2an 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( ( * o. F ) ` x ) = ( * ` ( F ` x ) ) )
66 fvco3 
 |-  ( ( F : X --> CC /\ C e. X ) -> ( ( * o. F ) ` C ) = ( * ` ( F ` C ) ) )
67 1 16 66 syl2anc 
 |-  ( ph -> ( ( * o. F ) ` C ) = ( * ` ( F ` C ) ) )
68 67 adantr 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( ( * o. F ) ` C ) = ( * ` ( F ` C ) ) )
69 65 68 oveq12d 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( ( ( * o. F ) ` x ) - ( ( * o. F ) ` C ) ) = ( ( * ` ( F ` x ) ) - ( * ` ( F ` C ) ) ) )
70 63 69 eqtr4d 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( * ` ( ( F ` x ) - ( F ` C ) ) ) = ( ( ( * o. F ) ` x ) - ( ( * o. F ) ` C ) ) )
71 54 cjred 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( * ` ( x - C ) ) = ( x - C ) )
72 70 71 oveq12d 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( ( * ` ( ( F ` x ) - ( F ` C ) ) ) / ( * ` ( x - C ) ) ) = ( ( ( ( * o. F ) ` x ) - ( ( * o. F ) ` C ) ) / ( x - C ) ) )
73 61 72 eqtrd 
 |-  ( ( ph /\ x e. ( X \ { C } ) ) -> ( * ` ( ( ( F ` x ) - ( F ` C ) ) / ( x - C ) ) ) = ( ( ( ( * o. F ) ` x ) - ( ( * o. F ) ` C ) ) / ( x - C ) ) )
74 73 mpteq2dva 
 |-  ( ph -> ( x e. ( X \ { C } ) |-> ( * ` ( ( ( F ` x ) - ( F ` C ) ) / ( x - C ) ) ) ) = ( x e. ( X \ { C } ) |-> ( ( ( ( * o. F ) ` x ) - ( ( * o. F ) ` C ) ) / ( x - C ) ) ) )
75 42 74 eqtrd 
 |-  ( ph -> ( * o. ( x e. ( X \ { C } ) |-> ( ( ( F ` x ) - ( F ` C ) ) / ( x - C ) ) ) ) = ( x e. ( X \ { C } ) |-> ( ( ( ( * o. F ) ` x ) - ( ( * o. F ) ` C ) ) / ( x - C ) ) ) )
76 75 oveq1d 
 |-  ( ph -> ( ( * o. ( x e. ( X \ { C } ) |-> ( ( ( F ` x ) - ( F ` C ) ) / ( x - C ) ) ) ) limCC C ) = ( ( x e. ( X \ { C } ) |-> ( ( ( ( * o. F ) ` x ) - ( ( * o. F ) ` C ) ) / ( x - C ) ) ) limCC C ) )
77 39 76 eleqtrd 
 |-  ( ph -> ( * ` ( ( RR _D F ) ` C ) ) e. ( ( x e. ( X \ { C } ) |-> ( ( ( ( * o. F ) ` x ) - ( ( * o. F ) ` C ) ) / ( x - C ) ) ) limCC C ) )
78 eqid 
 |-  ( x e. ( X \ { C } ) |-> ( ( ( ( * o. F ) ` x ) - ( ( * o. F ) ` C ) ) / ( x - C ) ) ) = ( x e. ( X \ { C } ) |-> ( ( ( ( * o. F ) ` x ) - ( ( * o. F ) ` C ) ) / ( x - C ) ) )
79 fco 
 |-  ( ( * : CC --> CC /\ F : X --> CC ) -> ( * o. F ) : X --> CC )
80 40 1 79 sylancr 
 |-  ( ph -> ( * o. F ) : X --> CC )
81 7 6 78 5 80 2 eldv 
 |-  ( ph -> ( C ( RR _D ( * o. F ) ) ( * ` ( ( RR _D F ) ` C ) ) <-> ( C e. ( ( int ` ( topGen ` ran (,) ) ) ` X ) /\ ( * ` ( ( RR _D F ) ` C ) ) e. ( ( x e. ( X \ { C } ) |-> ( ( ( ( * o. F ) ` x ) - ( ( * o. F ) ` C ) ) / ( x - C ) ) ) limCC C ) ) ) )
82 9 77 81 mpbir2and 
 |-  ( ph -> C ( RR _D ( * o. F ) ) ( * ` ( ( RR _D F ) ` C ) ) )