# 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}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
cncfcnvcn.k ${⊢}{K}={J}{↾}_{𝑡}{X}$
Assertion cncfcnvcn ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to \left({F}:{X}\underset{1-1 onto}{⟶}{Y}↔{{F}}^{-1}:{Y}\underset{cn}{⟶}{X}\right)$

### Proof

Step Hyp Ref Expression
1 cncfcnvcn.j ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 cncfcnvcn.k ${⊢}{K}={J}{↾}_{𝑡}{X}$
3 simpr ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to {F}:{X}\underset{cn}{⟶}{Y}$
4 cncfrss ${⊢}{F}:{X}\underset{cn}{⟶}{Y}\to {X}\subseteq ℂ$
5 4 adantl ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to {X}\subseteq ℂ$
6 cncfrss2 ${⊢}{F}:{X}\underset{cn}{⟶}{Y}\to {Y}\subseteq ℂ$
7 6 adantl ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to {Y}\subseteq ℂ$
8 eqid ${⊢}{J}{↾}_{𝑡}{Y}={J}{↾}_{𝑡}{Y}$
9 1 2 8 cncfcn
10 5 7 9 syl2anc
11 3 10 eleqtrd ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to {F}\in \left({K}\mathrm{Cn}\left({J}{↾}_{𝑡}{Y}\right)\right)$
12 ishmeo ${⊢}{F}\in \left({K}\mathrm{Homeo}\left({J}{↾}_{𝑡}{Y}\right)\right)↔\left({F}\in \left({K}\mathrm{Cn}\left({J}{↾}_{𝑡}{Y}\right)\right)\wedge {{F}}^{-1}\in \left(\left({J}{↾}_{𝑡}{Y}\right)\mathrm{Cn}{K}\right)\right)$
13 12 baib ${⊢}{F}\in \left({K}\mathrm{Cn}\left({J}{↾}_{𝑡}{Y}\right)\right)\to \left({F}\in \left({K}\mathrm{Homeo}\left({J}{↾}_{𝑡}{Y}\right)\right)↔{{F}}^{-1}\in \left(\left({J}{↾}_{𝑡}{Y}\right)\mathrm{Cn}{K}\right)\right)$
14 11 13 syl ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to \left({F}\in \left({K}\mathrm{Homeo}\left({J}{↾}_{𝑡}{Y}\right)\right)↔{{F}}^{-1}\in \left(\left({J}{↾}_{𝑡}{Y}\right)\mathrm{Cn}{K}\right)\right)$
15 1 cnfldtop ${⊢}{J}\in \mathrm{Top}$
16 1 cnfldtopon ${⊢}{J}\in \mathrm{TopOn}\left(ℂ\right)$
17 16 toponunii ${⊢}ℂ=\bigcup {J}$
18 17 restuni ${⊢}\left({J}\in \mathrm{Top}\wedge {X}\subseteq ℂ\right)\to {X}=\bigcup \left({J}{↾}_{𝑡}{X}\right)$
19 15 5 18 sylancr ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to {X}=\bigcup \left({J}{↾}_{𝑡}{X}\right)$
20 2 unieqi ${⊢}\bigcup {K}=\bigcup \left({J}{↾}_{𝑡}{X}\right)$
21 19 20 eqtr4di ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to {X}=\bigcup {K}$
22 21 f1oeq2d ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to \left({F}:{X}\underset{1-1 onto}{⟶}\bigcup \left({J}{↾}_{𝑡}{Y}\right)↔{F}:\bigcup {K}\underset{1-1 onto}{⟶}\bigcup \left({J}{↾}_{𝑡}{Y}\right)\right)$
23 17 restuni ${⊢}\left({J}\in \mathrm{Top}\wedge {Y}\subseteq ℂ\right)\to {Y}=\bigcup \left({J}{↾}_{𝑡}{Y}\right)$
24 15 7 23 sylancr ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to {Y}=\bigcup \left({J}{↾}_{𝑡}{Y}\right)$
25 24 f1oeq3d ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to \left({F}:{X}\underset{1-1 onto}{⟶}{Y}↔{F}:{X}\underset{1-1 onto}{⟶}\bigcup \left({J}{↾}_{𝑡}{Y}\right)\right)$
26 simpl ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to {K}\in \mathrm{Comp}$
27 1 cnfldhaus ${⊢}{J}\in \mathrm{Haus}$
28 cnex ${⊢}ℂ\in \mathrm{V}$
29 28 ssex ${⊢}{Y}\subseteq ℂ\to {Y}\in \mathrm{V}$
30 7 29 syl ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to {Y}\in \mathrm{V}$
31 resthaus ${⊢}\left({J}\in \mathrm{Haus}\wedge {Y}\in \mathrm{V}\right)\to {J}{↾}_{𝑡}{Y}\in \mathrm{Haus}$
32 27 30 31 sylancr ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to {J}{↾}_{𝑡}{Y}\in \mathrm{Haus}$
33 eqid ${⊢}\bigcup {K}=\bigcup {K}$
34 eqid ${⊢}\bigcup \left({J}{↾}_{𝑡}{Y}\right)=\bigcup \left({J}{↾}_{𝑡}{Y}\right)$
35 33 34 cmphaushmeo ${⊢}\left({K}\in \mathrm{Comp}\wedge {J}{↾}_{𝑡}{Y}\in \mathrm{Haus}\wedge {F}\in \left({K}\mathrm{Cn}\left({J}{↾}_{𝑡}{Y}\right)\right)\right)\to \left({F}\in \left({K}\mathrm{Homeo}\left({J}{↾}_{𝑡}{Y}\right)\right)↔{F}:\bigcup {K}\underset{1-1 onto}{⟶}\bigcup \left({J}{↾}_{𝑡}{Y}\right)\right)$
36 26 32 11 35 syl3anc ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to \left({F}\in \left({K}\mathrm{Homeo}\left({J}{↾}_{𝑡}{Y}\right)\right)↔{F}:\bigcup {K}\underset{1-1 onto}{⟶}\bigcup \left({J}{↾}_{𝑡}{Y}\right)\right)$
37 22 25 36 3bitr4d ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to \left({F}:{X}\underset{1-1 onto}{⟶}{Y}↔{F}\in \left({K}\mathrm{Homeo}\left({J}{↾}_{𝑡}{Y}\right)\right)\right)$
38 1 8 2 cncfcn
39 7 5 38 syl2anc
40 39 eleq2d ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to \left({{F}}^{-1}:{Y}\underset{cn}{⟶}{X}↔{{F}}^{-1}\in \left(\left({J}{↾}_{𝑡}{Y}\right)\mathrm{Cn}{K}\right)\right)$
41 14 37 40 3bitr4d ${⊢}\left({K}\in \mathrm{Comp}\wedge {F}:{X}\underset{cn}{⟶}{Y}\right)\to \left({F}:{X}\underset{1-1 onto}{⟶}{Y}↔{{F}}^{-1}:{Y}\underset{cn}{⟶}{X}\right)$