Metamath Proof Explorer

Theorem dvcnv

Description: A weak version of dvcnvre , valid for both real and complex domains but under the hypothesis that the inverse function is already known to be continuous, and the image set is known to be open. A more advanced proof can show that these conditions are unnecessary. (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 ) )
Assertion dvcnv 
|- ( ph -> ( S _D `' F ) = ( x e. Y |-> ( 1 / ( ( S _D F ) ` ( `' F ` x ) ) ) ) )

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 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D `' F ) : dom ( S _D `' F ) --> CC )
10 3 9 syl 
 |-  ( ph -> ( S _D `' F ) : dom ( S _D `' F ) --> CC )
11 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
12 3 11 syl 
 |-  ( ph -> S C_ CC )
13 f1ocnv 
 |-  ( F : X -1-1-onto-> Y -> `' F : Y -1-1-onto-> X )
14 f1of 
 |-  ( `' F : Y -1-1-onto-> X -> `' F : Y --> X )
15 5 13 14 3syl 
 |-  ( ph -> `' F : Y --> X )
16 dvbsss 
 |-  dom ( S _D F ) C_ S
17 7 16 eqsstrrdi 
 |-  ( ph -> X C_ S )
18 17 12 sstrd 
 |-  ( ph -> X C_ CC )
19 15 18 fssd 
 |-  ( ph -> `' F : Y --> CC )
20 1 cnfldtopon 
 |-  J e. ( TopOn ` CC )
21 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ S C_ CC ) -> ( J |`t S ) e. ( TopOn ` S ) )
22 20 12 21 sylancr 
 |-  ( ph -> ( J |`t S ) e. ( TopOn ` S ) )
23 2 22 eqeltrid 
 |-  ( ph -> K e. ( TopOn ` S ) )
24 toponss 
 |-  ( ( K e. ( TopOn ` S ) /\ Y e. K ) -> Y C_ S )
25 23 4 24 syl2anc 
 |-  ( ph -> Y C_ S )
26 12 19 25 dvbss 
 |-  ( ph -> dom ( S _D `' F ) C_ Y )
27 f1ocnvfv2 
 |-  ( ( F : X -1-1-onto-> Y /\ x e. Y ) -> ( F ` ( `' F ` x ) ) = x )
28 5 27 sylan 
 |-  ( ( ph /\ x e. Y ) -> ( F ` ( `' F ` x ) ) = x )
29 3 adantr 
 |-  ( ( ph /\ x e. Y ) -> S e. { RR , CC } )
30 4 adantr 
 |-  ( ( ph /\ x e. Y ) -> Y e. K )
31 5 adantr 
 |-  ( ( ph /\ x e. Y ) -> F : X -1-1-onto-> Y )
32 6 adantr 
 |-  ( ( ph /\ x e. Y ) -> `' F e. ( Y -cn-> X ) )
33 7 adantr 
 |-  ( ( ph /\ x e. Y ) -> dom ( S _D F ) = X )
34 8 adantr 
 |-  ( ( ph /\ x e. Y ) -> -. 0 e. ran ( S _D F ) )
35 15 ffvelrnda 
 |-  ( ( ph /\ x e. Y ) -> ( `' F ` x ) e. X )
36 1 2 29 30 31 32 33 34 35 dvcnvlem 
 |-  ( ( ph /\ x e. Y ) -> ( F ` ( `' F ` x ) ) ( S _D `' F ) ( 1 / ( ( S _D F ) ` ( `' F ` x ) ) ) )
37 28 36 eqbrtrrd 
 |-  ( ( ph /\ x e. Y ) -> x ( S _D `' F ) ( 1 / ( ( S _D F ) ` ( `' F ` x ) ) ) )
38 reldv 
 |-  Rel ( S _D `' F )
39 38 releldmi 
 |-  ( x ( S _D `' F ) ( 1 / ( ( S _D F ) ` ( `' F ` x ) ) ) -> x e. dom ( S _D `' F ) )
40 37 39 syl 
 |-  ( ( ph /\ x e. Y ) -> x e. dom ( S _D `' F ) )
41 26 40 eqelssd 
 |-  ( ph -> dom ( S _D `' F ) = Y )
42 41 feq2d 
 |-  ( ph -> ( ( S _D `' F ) : dom ( S _D `' F ) --> CC <-> ( S _D `' F ) : Y --> CC ) )
43 10 42 mpbid 
 |-  ( ph -> ( S _D `' F ) : Y --> CC )
44 43 feqmptd 
 |-  ( ph -> ( S _D `' F ) = ( x e. Y |-> ( ( S _D `' F ) ` x ) ) )
45 10 adantr 
 |-  ( ( ph /\ x e. Y ) -> ( S _D `' F ) : dom ( S _D `' F ) --> CC )
46 45 ffund 
 |-  ( ( ph /\ x e. Y ) -> Fun ( S _D `' F ) )
47 funbrfv 
 |-  ( Fun ( S _D `' F ) -> ( x ( S _D `' F ) ( 1 / ( ( S _D F ) ` ( `' F ` x ) ) ) -> ( ( S _D `' F ) ` x ) = ( 1 / ( ( S _D F ) ` ( `' F ` x ) ) ) ) )
48 46 37 47 sylc 
 |-  ( ( ph /\ x e. Y ) -> ( ( S _D `' F ) ` x ) = ( 1 / ( ( S _D F ) ` ( `' F ` x ) ) ) )
49 48 mpteq2dva 
 |-  ( ph -> ( x e. Y |-> ( ( S _D `' F ) ` x ) ) = ( x e. Y |-> ( 1 / ( ( S _D F ) ` ( `' F ` x ) ) ) ) )
50 44 49 eqtrd 
 |-  ( ph -> ( S _D `' F ) = ( x e. Y |-> ( 1 / ( ( S _D F ) ` ( `' F ` x ) ) ) ) )