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

Metamath Proof Explorer

Theorem dvcnvlem

Description: Lemma for dvcnvre . (Contributed by Mario Carneiro, 25-Feb-2015) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypotheses dvcnv.j 
|- J = ( TopOpen ` CCfld )
dvcnv.k 
|- K = ( J |`t S )
dvcnv.s 
|- ( ph -> S e. { RR , CC } )
dvcnv.y 
|- ( ph -> Y e. K )
dvcnv.f 
|- ( ph -> F : X -1-1-onto-> Y )
dvcnv.i 
|- ( ph -> `' F e. ( Y -cn-> X ) )
dvcnv.d 
|- ( ph -> dom ( S _D F ) = X )
dvcnv.z 
|- ( ph -> -. 0 e. ran ( S _D F ) )
dvcnv.c 
|- ( ph -> C e. X )
Assertion dvcnvlem 
|- ( ph -> ( F ` C ) ( S _D `' F ) ( 1 / ( ( S _D F ) ` C ) ) )

Proof

Step Hyp Ref Expression
1 dvcnv.j 
 |-  J = ( TopOpen ` CCfld )
2 dvcnv.k 
 |-  K = ( J |`t S )
3 dvcnv.s 
 |-  ( ph -> S e. { RR , CC } )
4 dvcnv.y 
 |-  ( ph -> Y e. K )
5 dvcnv.f 
 |-  ( ph -> F : X -1-1-onto-> Y )
6 dvcnv.i 
 |-  ( ph -> `' F e. ( Y -cn-> X ) )
7 dvcnv.d 
 |-  ( ph -> dom ( S _D F ) = X )
8 dvcnv.z 
 |-  ( ph -> -. 0 e. ran ( S _D F ) )
9 dvcnv.c 
 |-  ( ph -> C e. X )
10 f1of 
 |-  ( F : X -1-1-onto-> Y -> F : X --> Y )
11 5 10 syl 
 |-  ( ph -> F : X --> Y )
12 11 9 ffvelcdmd 
 |-  ( ph -> ( F ` C ) e. Y )
13 1 cnfldtopon 
 |-  J e. ( TopOn ` CC )
14 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
15 3 14 syl 
 |-  ( ph -> S C_ CC )
16 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ S C_ CC ) -> ( J |`t S ) e. ( TopOn ` S ) )
17 13 15 16 sylancr 
 |-  ( ph -> ( J |`t S ) e. ( TopOn ` S ) )
18 2 17 eqeltrid 
 |-  ( ph -> K e. ( TopOn ` S ) )
19 topontop 
 |-  ( K e. ( TopOn ` S ) -> K e. Top )
20 18 19 syl 
 |-  ( ph -> K e. Top )
21 isopn3i 
 |-  ( ( K e. Top /\ Y e. K ) -> ( ( int ` K ) ` Y ) = Y )
22 20 4 21 syl2anc 
 |-  ( ph -> ( ( int ` K ) ` Y ) = Y )
23 12 22 eleqtrrd 
 |-  ( ph -> ( F ` C ) e. ( ( int ` K ) ` Y ) )
24 f1ocnv 
 |-  ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X )
25 f1of 
 |-  ( `' F : Y -1-1-onto-> X -> `' F : Y --> X )
26 5 24 25 3syl 
 |-  ( ph -> `' F : Y --> X )
27 eldifi 
 |-  ( z e. ( Y \ { ( F ` C ) } ) -> z e. Y )
28 ffvelcdm 
 |-  ( ( `' F : Y --> X /\ z e. Y ) -> ( `' F ` z ) e. X )
29 26 27 28 syl2an 
 |-  ( ( ph /\ z e. ( Y \ { ( F ` C ) } ) ) -> ( `' F ` z ) e. X )
30 29 anim1i 
 |-  ( ( ( ph /\ z e. ( Y \ { ( F ` C ) } ) ) /\ ( `' F ` z ) =/= C ) -> ( ( `' F ` z ) e. X /\ ( `' F ` z ) =/= C ) )
31 eldifsn 
 |-  ( ( `' F ` z ) e. ( X \ { C } ) <-> ( ( `' F ` z ) e. X /\ ( `' F ` z ) =/= C ) )
32 30 31 sylibr 
 |-  ( ( ( ph /\ z e. ( Y \ { ( F ` C ) } ) ) /\ ( `' F ` z ) =/= C ) -> ( `' F ` z ) e. ( X \ { C } ) )
33 32 anasss 
 |-  ( ( ph /\ ( z e. ( Y \ { ( F ` C ) } ) /\ ( `' F ` z ) =/= C ) ) -> ( `' F ` z ) e. ( X \ { C } ) )
34 eldifi 
 |-  ( y e. ( X \ { C } ) -> y e. X )
35 dvbsss 
 |-  dom ( S _D F ) C_ S
36 7 35 eqsstrrdi 
 |-  ( ph -> X C_ S )
37 36 15 sstrd 
 |-  ( ph -> X C_ CC )
38 37 sselda 
 |-  ( ( ph /\ y e. X ) -> y e. CC )
39 34 38 sylan2 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> y e. CC )
40 36 9 sseldd 
 |-  ( ph -> C e. S )
41 15 40 sseldd 
 |-  ( ph -> C e. CC )
42 41 adantr 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> C e. CC )
43 39 42 subcld 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> ( y - C ) e. CC )
44 toponss 
 |-  ( ( K e. ( TopOn ` S ) /\ Y e. K ) -> Y C_ S )
45 18 4 44 syl2anc 
 |-  ( ph -> Y C_ S )
46 45 15 sstrd 
 |-  ( ph -> Y C_ CC )
47 11 46 fssd 
 |-  ( ph -> F : X --> CC )
48 ffvelcdm 
 |-  ( ( F : X --> CC /\ y e. X ) -> ( F ` y ) e. CC )
49 47 34 48 syl2an 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> ( F ` y ) e. CC )
50 46 12 sseldd 
 |-  ( ph -> ( F ` C ) e. CC )
51 50 adantr 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> ( F ` C ) e. CC )
52 49 51 subcld 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> ( ( F ` y ) - ( F ` C ) ) e. CC )
53 eldifsni 
 |-  ( y e. ( X \ { C } ) -> y =/= C )
54 53 adantl 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> y =/= C )
55 49 51 subeq0ad 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> ( ( ( F ` y ) - ( F ` C ) ) = 0 <-> ( F ` y ) = ( F ` C ) ) )
56 f1of1 
 |-  ( F : X -1-1-onto-> Y -> F : X -1-1-> Y )
57 5 56 syl 
 |-  ( ph -> F : X -1-1-> Y )
58 57 adantr 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> F : X -1-1-> Y )
59 34 adantl 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> y e. X )
60 9 adantr 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> C e. X )
61 f1fveq 
 |-  ( ( F : X -1-1-> Y /\ ( y e. X /\ C e. X ) ) -> ( ( F ` y ) = ( F ` C ) <-> y = C ) )
62 58 59 60 61 syl12anc 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> ( ( F ` y ) = ( F ` C ) <-> y = C ) )
63 55 62 bitrd 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> ( ( ( F ` y ) - ( F ` C ) ) = 0 <-> y = C ) )
64 63 necon3bid 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> ( ( ( F ` y ) - ( F ` C ) ) =/= 0 <-> y =/= C ) )
65 54 64 mpbird 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> ( ( F ` y ) - ( F ` C ) ) =/= 0 )
66 43 52 65 divcld 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> ( ( y - C ) / ( ( F ` y ) - ( F ` C ) ) ) e. CC )
67 limcresi 
 |-  ( `' F limCC ( F ` C ) ) C_ ( ( `' F |` ( Y \ { ( F ` C ) } ) ) limCC ( F ` C ) )
68 26 feqmptd 
 |-  ( ph -> `' F = ( z e. Y |-> ( `' F ` z ) ) )
69 68 reseq1d 
 |-  ( ph -> ( `' F |` ( Y \ { ( F ` C ) } ) ) = ( ( z e. Y |-> ( `' F ` z ) ) |` ( Y \ { ( F ` C ) } ) ) )
70 difss 
 |-  ( Y \ { ( F ` C ) } ) C_ Y
71 resmpt 
 |-  ( ( Y \ { ( F ` C ) } ) C_ Y -> ( ( z e. Y |-> ( `' F ` z ) ) |` ( Y \ { ( F ` C ) } ) ) = ( z e. ( Y \ { ( F ` C ) } ) |-> ( `' F ` z ) ) )
72 70 71 ax-mp 
 |-  ( ( z e. Y |-> ( `' F ` z ) ) |` ( Y \ { ( F ` C ) } ) ) = ( z e. ( Y \ { ( F ` C ) } ) |-> ( `' F ` z ) )
73 69 72 eqtrdi 
 |-  ( ph -> ( `' F |` ( Y \ { ( F ` C ) } ) ) = ( z e. ( Y \ { ( F ` C ) } ) |-> ( `' F ` z ) ) )
74 73 oveq1d 
 |-  ( ph -> ( ( `' F |` ( Y \ { ( F ` C ) } ) ) limCC ( F ` C ) ) = ( ( z e. ( Y \ { ( F ` C ) } ) |-> ( `' F ` z ) ) limCC ( F ` C ) ) )
75 67 74 sseqtrid 
 |-  ( ph -> ( `' F limCC ( F ` C ) ) C_ ( ( z e. ( Y \ { ( F ` C ) } ) |-> ( `' F ` z ) ) limCC ( F ` C ) ) )
76 f1ocnvfv1 
 |-  ( ( F : X -1-1-onto-> Y /\ C e. X ) -> ( `' F ` ( F ` C ) ) = C )
77 5 9 76 syl2anc 
 |-  ( ph -> ( `' F ` ( F ` C ) ) = C )
78 6 12 cnlimci 
 |-  ( ph -> ( `' F ` ( F ` C ) ) e. ( `' F limCC ( F ` C ) ) )
79 77 78 eqeltrrd 
 |-  ( ph -> C e. ( `' F limCC ( F ` C ) ) )
80 75 79 sseldd 
 |-  ( ph -> C e. ( ( z e. ( Y \ { ( F ` C ) } ) |-> ( `' F ` z ) ) limCC ( F ` C ) ) )
81 47 37 9 dvlem 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) e. CC )
82 39 42 54 subne0d 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> ( y - C ) =/= 0 )
83 52 43 65 82 divne0d 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) =/= 0 )
84 eldifsn 
 |-  ( ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) e. ( CC \ { 0 } ) <-> ( ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) e. CC /\ ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) =/= 0 ) )
85 81 83 84 sylanbrc 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) e. ( CC \ { 0 } ) )
86 85 fmpttd 
 |-  ( ph -> ( y e. ( X \ { C } ) |-> ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) ) : ( X \ { C } ) --> ( CC \ { 0 } ) )
87 difss 
 |-  ( CC \ { 0 } ) C_ CC
88 87 a1i 
 |-  ( ph -> ( CC \ { 0 } ) C_ CC )
89 eqid 
 |-  ( J |`t ( CC \ { 0 } ) ) = ( J |`t ( CC \ { 0 } ) )
90 9 7 eleqtrrd 
 |-  ( ph -> C e. dom ( S _D F ) )
91 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D F ) : dom ( S _D F ) --> CC )
92 ffun 
 |-  ( ( S _D F ) : dom ( S _D F ) --> CC -> Fun ( S _D F ) )
93 funfvbrb 
 |-  ( Fun ( S _D F ) -> ( C e. dom ( S _D F ) <-> C ( S _D F ) ( ( S _D F ) ` C ) ) )
94 3 91 92 93 4syl 
 |-  ( ph -> ( C e. dom ( S _D F ) <-> C ( S _D F ) ( ( S _D F ) ` C ) ) )
95 90 94 mpbid 
 |-  ( ph -> C ( S _D F ) ( ( S _D F ) ` C ) )
96 eqid 
 |-  ( y e. ( X \ { C } ) |-> ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) ) = ( y e. ( X \ { C } ) |-> ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) )
97 2 1 96 15 47 36 eldv 
 |-  ( ph -> ( C ( S _D F ) ( ( S _D F ) ` C ) <-> ( C e. ( ( int ` K ) ` X ) /\ ( ( S _D F ) ` C ) e. ( ( y e. ( X \ { C } ) |-> ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) ) limCC C ) ) ) )
98 95 97 mpbid 
 |-  ( ph -> ( C e. ( ( int ` K ) ` X ) /\ ( ( S _D F ) ` C ) e. ( ( y e. ( X \ { C } ) |-> ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) ) limCC C ) ) )
99 98 simprd 
 |-  ( ph -> ( ( S _D F ) ` C ) e. ( ( y e. ( X \ { C } ) |-> ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) ) limCC C ) )
100 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ ( CC \ { 0 } ) C_ CC ) -> ( J |`t ( CC \ { 0 } ) ) e. ( TopOn ` ( CC \ { 0 } ) ) )
101 13 87 100 mp2an 
 |-  ( J |`t ( CC \ { 0 } ) ) e. ( TopOn ` ( CC \ { 0 } ) )
102 101 a1i 
 |-  ( ph -> ( J |`t ( CC \ { 0 } ) ) e. ( TopOn ` ( CC \ { 0 } ) ) )
103 13 a1i 
 |-  ( ph -> J e. ( TopOn ` CC ) )
104 1cnd 
 |-  ( ph -> 1 e. CC )
105 102 103 104 cnmptc 
 |-  ( ph -> ( x e. ( CC \ { 0 } ) |-> 1 ) e. ( ( J |`t ( CC \ { 0 } ) ) Cn J ) )
106 102 cnmptid 
 |-  ( ph -> ( x e. ( CC \ { 0 } ) |-> x ) e. ( ( J |`t ( CC \ { 0 } ) ) Cn ( J |`t ( CC \ { 0 } ) ) ) )
107 1 89 divcn 
 |-  / e. ( ( J tX ( J |`t ( CC \ { 0 } ) ) ) Cn J )
108 107 a1i 
 |-  ( ph -> / e. ( ( J tX ( J |`t ( CC \ { 0 } ) ) ) Cn J ) )
109 102 105 106 108 cnmpt12f 
 |-  ( ph -> ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) e. ( ( J |`t ( CC \ { 0 } ) ) Cn J ) )
110 3 91 syl 
 |-  ( ph -> ( S _D F ) : dom ( S _D F ) --> CC )
111 7 feq2d 
 |-  ( ph -> ( ( S _D F ) : dom ( S _D F ) --> CC <-> ( S _D F ) : X --> CC ) )
112 110 111 mpbid 
 |-  ( ph -> ( S _D F ) : X --> CC )
113 112 9 ffvelcdmd 
 |-  ( ph -> ( ( S _D F ) ` C ) e. CC )
114 110 ffnd 
 |-  ( ph -> ( S _D F ) Fn dom ( S _D F ) )
115 fnfvelrn 
 |-  ( ( ( S _D F ) Fn dom ( S _D F ) /\ C e. dom ( S _D F ) ) -> ( ( S _D F ) ` C ) e. ran ( S _D F ) )
116 114 90 115 syl2anc 
 |-  ( ph -> ( ( S _D F ) ` C ) e. ran ( S _D F ) )
117 nelne2 
 |-  ( ( ( ( S _D F ) ` C ) e. ran ( S _D F ) /\ -. 0 e. ran ( S _D F ) ) -> ( ( S _D F ) ` C ) =/= 0 )
118 116 8 117 syl2anc 
 |-  ( ph -> ( ( S _D F ) ` C ) =/= 0 )
119 eldifsn 
 |-  ( ( ( S _D F ) ` C ) e. ( CC \ { 0 } ) <-> ( ( ( S _D F ) ` C ) e. CC /\ ( ( S _D F ) ` C ) =/= 0 ) )
120 113 118 119 sylanbrc 
 |-  ( ph -> ( ( S _D F ) ` C ) e. ( CC \ { 0 } ) )
121 101 toponunii 
 |-  ( CC \ { 0 } ) = U. ( J |`t ( CC \ { 0 } ) )
122 121 cncnpi 
 |-  ( ( ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) e. ( ( J |`t ( CC \ { 0 } ) ) Cn J ) /\ ( ( S _D F ) ` C ) e. ( CC \ { 0 } ) ) -> ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) e. ( ( ( J |`t ( CC \ { 0 } ) ) CnP J ) ` ( ( S _D F ) ` C ) ) )
123 109 120 122 syl2anc 
 |-  ( ph -> ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) e. ( ( ( J |`t ( CC \ { 0 } ) ) CnP J ) ` ( ( S _D F ) ` C ) ) )
124 86 88 1 89 99 123 limccnp 
 |-  ( ph -> ( ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) ` ( ( S _D F ) ` C ) ) e. ( ( ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) o. ( y e. ( X \ { C } ) |-> ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) ) ) limCC C ) )
125 oveq2 
 |-  ( x = ( ( S _D F ) ` C ) -> ( 1 / x ) = ( 1 / ( ( S _D F ) ` C ) ) )
126 eqid 
 |-  ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) = ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) )
127 ovex 
 |-  ( 1 / ( ( S _D F ) ` C ) ) e. _V
128 125 126 127 fvmpt 
 |-  ( ( ( S _D F ) ` C ) e. ( CC \ { 0 } ) -> ( ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) ` ( ( S _D F ) ` C ) ) = ( 1 / ( ( S _D F ) ` C ) ) )
129 120 128 syl 
 |-  ( ph -> ( ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) ` ( ( S _D F ) ` C ) ) = ( 1 / ( ( S _D F ) ` C ) ) )
130 eqidd 
 |-  ( ph -> ( y e. ( X \ { C } ) |-> ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) ) = ( y e. ( X \ { C } ) |-> ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) ) )
131 eqidd 
 |-  ( ph -> ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) = ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) )
132 oveq2 
 |-  ( x = ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) -> ( 1 / x ) = ( 1 / ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) ) )
133 85 130 131 132 fmptco 
 |-  ( ph -> ( ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) o. ( y e. ( X \ { C } ) |-> ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) ) ) = ( y e. ( X \ { C } ) |-> ( 1 / ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) ) ) )
134 52 43 65 82 recdivd 
 |-  ( ( ph /\ y e. ( X \ { C } ) ) -> ( 1 / ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) ) = ( ( y - C ) / ( ( F ` y ) - ( F ` C ) ) ) )
135 134 mpteq2dva 
 |-  ( ph -> ( y e. ( X \ { C } ) |-> ( 1 / ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) ) ) = ( y e. ( X \ { C } ) |-> ( ( y - C ) / ( ( F ` y ) - ( F ` C ) ) ) ) )
136 133 135 eqtrd 
 |-  ( ph -> ( ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) o. ( y e. ( X \ { C } ) |-> ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) ) ) = ( y e. ( X \ { C } ) |-> ( ( y - C ) / ( ( F ` y ) - ( F ` C ) ) ) ) )
137 136 oveq1d 
 |-  ( ph -> ( ( ( x e. ( CC \ { 0 } ) |-> ( 1 / x ) ) o. ( y e. ( X \ { C } ) |-> ( ( ( F ` y ) - ( F ` C ) ) / ( y - C ) ) ) ) limCC C ) = ( ( y e. ( X \ { C } ) |-> ( ( y - C ) / ( ( F ` y ) - ( F ` C ) ) ) ) limCC C ) )
138 124 129 137 3eltr3d 
 |-  ( ph -> ( 1 / ( ( S _D F ) ` C ) ) e. ( ( y e. ( X \ { C } ) |-> ( ( y - C ) / ( ( F ` y ) - ( F ` C ) ) ) ) limCC C ) )
139 oveq1 
 |-  ( y = ( `' F ` z ) -> ( y - C ) = ( ( `' F ` z ) - C ) )
140 fveq2 
 |-  ( y = ( `' F ` z ) -> ( F ` y ) = ( F ` ( `' F ` z ) ) )
141 140 oveq1d 
 |-  ( y = ( `' F ` z ) -> ( ( F ` y ) - ( F ` C ) ) = ( ( F ` ( `' F ` z ) ) - ( F ` C ) ) )
142 139 141 oveq12d 
 |-  ( y = ( `' F ` z ) -> ( ( y - C ) / ( ( F ` y ) - ( F ` C ) ) ) = ( ( ( `' F ` z ) - C ) / ( ( F ` ( `' F ` z ) ) - ( F ` C ) ) ) )
143 eldifsni 
 |-  ( z e. ( Y \ { ( F ` C ) } ) -> z =/= ( F ` C ) )
144 143 adantl 
 |-  ( ( ph /\ z e. ( Y \ { ( F ` C ) } ) ) -> z =/= ( F ` C ) )
145 144 necomd 
 |-  ( ( ph /\ z e. ( Y \ { ( F ` C ) } ) ) -> ( F ` C ) =/= z )
146 f1ocnvfvb 
 |-  ( ( F : X -1-1-onto-> Y /\ C e. X /\ z e. Y ) -> ( ( F ` C ) = z <-> ( `' F ` z ) = C ) )
147 5 9 27 146 syl2an3an 
 |-  ( ( ph /\ z e. ( Y \ { ( F ` C ) } ) ) -> ( ( F ` C ) = z <-> ( `' F ` z ) = C ) )
148 147 necon3abid 
 |-  ( ( ph /\ z e. ( Y \ { ( F ` C ) } ) ) -> ( ( F ` C ) =/= z <-> -. ( `' F ` z ) = C ) )
149 145 148 mpbid 
 |-  ( ( ph /\ z e. ( Y \ { ( F ` C ) } ) ) -> -. ( `' F ` z ) = C )
150 149 pm2.21d 
 |-  ( ( ph /\ z e. ( Y \ { ( F ` C ) } ) ) -> ( ( `' F ` z ) = C -> ( ( ( `' F ` z ) - C ) / ( ( F ` ( `' F ` z ) ) - ( F ` C ) ) ) = ( 1 / ( ( S _D F ) ` C ) ) ) )
151 150 impr 
 |-  ( ( ph /\ ( z e. ( Y \ { ( F ` C ) } ) /\ ( `' F ` z ) = C ) ) -> ( ( ( `' F ` z ) - C ) / ( ( F ` ( `' F ` z ) ) - ( F ` C ) ) ) = ( 1 / ( ( S _D F ) ` C ) ) )
152 33 66 80 138 142 151 limcco 
 |-  ( ph -> ( 1 / ( ( S _D F ) ` C ) ) e. ( ( z e. ( Y \ { ( F ` C ) } ) |-> ( ( ( `' F ` z ) - C ) / ( ( F ` ( `' F ` z ) ) - ( F ` C ) ) ) ) limCC ( F ` C ) ) )
153 77 eqcomd 
 |-  ( ph -> C = ( `' F ` ( F ` C ) ) )
154 153 adantr 
 |-  ( ( ph /\ z e. ( Y \ { ( F ` C ) } ) ) -> C = ( `' F ` ( F ` C ) ) )
155 154 oveq2d 
 |-  ( ( ph /\ z e. ( Y \ { ( F ` C ) } ) ) -> ( ( `' F ` z ) - C ) = ( ( `' F ` z ) - ( `' F ` ( F ` C ) ) ) )
156 f1ocnvfv2 
 |-  ( ( F : X -1-1-onto-> Y /\ z e. Y ) -> ( F ` ( `' F ` z ) ) = z )
157 5 27 156 syl2an 
 |-  ( ( ph /\ z e. ( Y \ { ( F ` C ) } ) ) -> ( F ` ( `' F ` z ) ) = z )
158 157 oveq1d 
 |-  ( ( ph /\ z e. ( Y \ { ( F ` C ) } ) ) -> ( ( F ` ( `' F ` z ) ) - ( F ` C ) ) = ( z - ( F ` C ) ) )
159 155 158 oveq12d 
 |-  ( ( ph /\ z e. ( Y \ { ( F ` C ) } ) ) -> ( ( ( `' F ` z ) - C ) / ( ( F ` ( `' F ` z ) ) - ( F ` C ) ) ) = ( ( ( `' F ` z ) - ( `' F ` ( F ` C ) ) ) / ( z - ( F ` C ) ) ) )
160 159 mpteq2dva 
 |-  ( ph -> ( z e. ( Y \ { ( F ` C ) } ) |-> ( ( ( `' F ` z ) - C ) / ( ( F ` ( `' F ` z ) ) - ( F ` C ) ) ) ) = ( z e. ( Y \ { ( F ` C ) } ) |-> ( ( ( `' F ` z ) - ( `' F ` ( F ` C ) ) ) / ( z - ( F ` C ) ) ) ) )
161 160 oveq1d 
 |-  ( ph -> ( ( z e. ( Y \ { ( F ` C ) } ) |-> ( ( ( `' F ` z ) - C ) / ( ( F ` ( `' F ` z ) ) - ( F ` C ) ) ) ) limCC ( F ` C ) ) = ( ( z e. ( Y \ { ( F ` C ) } ) |-> ( ( ( `' F ` z ) - ( `' F ` ( F ` C ) ) ) / ( z - ( F ` C ) ) ) ) limCC ( F ` C ) ) )
162 152 161 eleqtrd 
 |-  ( ph -> ( 1 / ( ( S _D F ) ` C ) ) e. ( ( z e. ( Y \ { ( F ` C ) } ) |-> ( ( ( `' F ` z ) - ( `' F ` ( F ` C ) ) ) / ( z - ( F ` C ) ) ) ) limCC ( F ` C ) ) )
163 eqid 
 |-  ( z e. ( Y \ { ( F ` C ) } ) |-> ( ( ( `' F ` z ) - ( `' F ` ( F ` C ) ) ) / ( z - ( F ` C ) ) ) ) = ( z e. ( Y \ { ( F ` C ) } ) |-> ( ( ( `' F ` z ) - ( `' F ` ( F ` C ) ) ) / ( z - ( F ` C ) ) ) )
164 26 37 fssd 
 |-  ( ph -> `' F : Y --> CC )
165 2 1 163 15 164 45 eldv 
 |-  ( ph -> ( ( F ` C ) ( S _D `' F ) ( 1 / ( ( S _D F ) ` C ) ) <-> ( ( F ` C ) e. ( ( int ` K ) ` Y ) /\ ( 1 / ( ( S _D F ) ` C ) ) e. ( ( z e. ( Y \ { ( F ` C ) } ) |-> ( ( ( `' F ` z ) - ( `' F ` ( F ` C ) ) ) / ( z - ( F ` C ) ) ) ) limCC ( F ` C ) ) ) ) )
166 23 162 165 mpbir2and 
 |-  ( ph -> ( F ` C ) ( S _D `' F ) ( 1 / ( ( S _D F ) ` C ) ) )