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 ) ) )