Metamath Proof Explorer

Theorem cncfcnvcn

Description: Rewrite cmphaushmeo for functions on the complex numbers. (Contributed by Mario Carneiro, 19-Feb-2015)

Ref Expression
Hypotheses cncfcnvcn.j 
|- J = ( TopOpen ` CCfld )
cncfcnvcn.k 
|- K = ( J |`t X )
Assertion cncfcnvcn 
|- ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( F : X -1-1-onto-> Y <-> `' F e. ( Y -cn-> X ) ) )

Proof

Step Hyp Ref Expression
1 cncfcnvcn.j 
 |-  J = ( TopOpen ` CCfld )
2 cncfcnvcn.k 
 |-  K = ( J |`t X )
3 simpr 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> F e. ( X -cn-> Y ) )
4 cncfrss 
 |-  ( F e. ( X -cn-> Y ) -> X C_ CC )
5 4 adantl 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> X C_ CC )
6 cncfrss2 
 |-  ( F e. ( X -cn-> Y ) -> Y C_ CC )
7 6 adantl 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> Y C_ CC )
8 eqid 
 |-  ( J |`t Y ) = ( J |`t Y )
9 1 2 8 cncfcn 
 |-  ( ( X C_ CC /\ Y C_ CC ) -> ( X -cn-> Y ) = ( K Cn ( J |`t Y ) ) )
10 5 7 9 syl2anc 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( X -cn-> Y ) = ( K Cn ( J |`t Y ) ) )
11 3 10 eleqtrd 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> F e. ( K Cn ( J |`t Y ) ) )
12 ishmeo 
 |-  ( F e. ( K Homeo ( J |`t Y ) ) <-> ( F e. ( K Cn ( J |`t Y ) ) /\ `' F e. ( ( J |`t Y ) Cn K ) ) )
13 12 baib 
 |-  ( F e. ( K Cn ( J |`t Y ) ) -> ( F e. ( K Homeo ( J |`t Y ) ) <-> `' F e. ( ( J |`t Y ) Cn K ) ) )
14 11 13 syl 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( F e. ( K Homeo ( J |`t Y ) ) <-> `' F e. ( ( J |`t Y ) Cn K ) ) )
15 1 cnfldtop 
 |-  J e. Top
16 1 cnfldtopon 
 |-  J e. ( TopOn ` CC )
17 16 toponunii 
 |-  CC = U. J
18 17 restuni 
 |-  ( ( J e. Top /\ X C_ CC ) -> X = U. ( J |`t X ) )
19 15 5 18 sylancr 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> X = U. ( J |`t X ) )
20 2 unieqi 
 |-  U. K = U. ( J |`t X )
21 19 20 eqtr4di 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> X = U. K )
22 21 f1oeq2d 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( F : X -1-1-onto-> U. ( J |`t Y ) <-> F : U. K -1-1-onto-> U. ( J |`t Y ) ) )
23 17 restuni 
 |-  ( ( J e. Top /\ Y C_ CC ) -> Y = U. ( J |`t Y ) )
24 15 7 23 sylancr 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> Y = U. ( J |`t Y ) )
25 24 f1oeq3d 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( F : X -1-1-onto-> Y <-> F : X -1-1-onto-> U. ( J |`t Y ) ) )
26 simpl 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> K e. Comp )
27 1 cnfldhaus 
 |-  J e. Haus
28 cnex 
 |-  CC e. _V
29 28 ssex 
 |-  ( Y C_ CC -> Y e. _V )
30 7 29 syl 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> Y e. _V )
31 resthaus 
 |-  ( ( J e. Haus /\ Y e. _V ) -> ( J |`t Y ) e. Haus )
32 27 30 31 sylancr 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( J |`t Y ) e. Haus )
33 eqid 
 |-  U. K = U. K
34 eqid 
 |-  U. ( J |`t Y ) = U. ( J |`t Y )
35 33 34 cmphaushmeo 
 |-  ( ( K e. Comp /\ ( J |`t Y ) e. Haus /\ F e. ( K Cn ( J |`t Y ) ) ) -> ( F e. ( K Homeo ( J |`t Y ) ) <-> F : U. K -1-1-onto-> U. ( J |`t Y ) ) )
36 26 32 11 35 syl3anc 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( F e. ( K Homeo ( J |`t Y ) ) <-> F : U. K -1-1-onto-> U. ( J |`t Y ) ) )
37 22 25 36 3bitr4d 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( F : X -1-1-onto-> Y <-> F e. ( K Homeo ( J |`t Y ) ) ) )
38 1 8 2 cncfcn 
 |-  ( ( Y C_ CC /\ X C_ CC ) -> ( Y -cn-> X ) = ( ( J |`t Y ) Cn K ) )
39 7 5 38 syl2anc 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( Y -cn-> X ) = ( ( J |`t Y ) Cn K ) )
40 39 eleq2d 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( `' F e. ( Y -cn-> X ) <-> `' F e. ( ( J |`t Y ) Cn K ) ) )
41 14 37 40 3bitr4d 
 |-  ( ( K e. Comp /\ F e. ( X -cn-> Y ) ) -> ( F : X -1-1-onto-> Y <-> `' F e. ( Y -cn-> X ) ) )