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

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 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
cncfcnvcn.k ⊢ 𝐾 = ( 𝐽 ↾t 𝑋 )
Assertion cncfcnvcn ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ ◡ 𝐹 ∈ ( 𝑌 –cn→ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 cncfcnvcn.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2 cncfcnvcn.k ⊢ 𝐾 = ( 𝐽 ↾t 𝑋 )
3 simpr ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) )
4 cncfrss ⊢ ( 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) → 𝑋 ⊆ ℂ )
5 4 adantl ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝑋 ⊆ ℂ )
6 cncfrss2 ⊢ ( 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) → 𝑌 ⊆ ℂ )
7 6 adantl ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝑌 ⊆ ℂ )
8 eqid ⊢ ( 𝐽 ↾t 𝑌 ) = ( 𝐽 ↾t 𝑌 )
9 1 2 8 cncfcn ⊢ ( ( 𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ ) → ( 𝑋 –cn→ 𝑌 ) = ( 𝐾 Cn ( 𝐽 ↾t 𝑌 ) ) )
10 5 7 9 syl2anc ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝑋 –cn→ 𝑌 ) = ( 𝐾 Cn ( 𝐽 ↾t 𝑌 ) ) )
11 3 10 eleqtrd ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝐹 ∈ ( 𝐾 Cn ( 𝐽 ↾t 𝑌 ) ) )
12 ishmeo ⊢ ( 𝐹 ∈ ( 𝐾 Homeo ( 𝐽 ↾t 𝑌 ) ) ↔ ( 𝐹 ∈ ( 𝐾 Cn ( 𝐽 ↾t 𝑌 ) ) ∧ ◡ 𝐹 ∈ ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) ) )
13 12 baib ⊢ ( 𝐹 ∈ ( 𝐾 Cn ( 𝐽 ↾t 𝑌 ) ) → ( 𝐹 ∈ ( 𝐾 Homeo ( 𝐽 ↾t 𝑌 ) ) ↔ ◡ 𝐹 ∈ ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) ) )
14 11 13 syl ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐾 Homeo ( 𝐽 ↾t 𝑌 ) ) ↔ ◡ 𝐹 ∈ ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) ) )
15 1 cnfldtop ⊢ 𝐽 ∈ Top
16 1 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
17 16 toponunii ⊢ ℂ = ∪ 𝐽
18 17 restuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ℂ ) → 𝑋 = ∪ ( 𝐽 ↾t 𝑋 ) )
19 15 5 18 sylancr ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝑋 = ∪ ( 𝐽 ↾t 𝑋 ) )
20 2 unieqi ⊢ ∪ 𝐾 = ∪ ( 𝐽 ↾t 𝑋 )
21 19 20 eqtr4di ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝑋 = ∪ 𝐾 )
22 21 f1oeq2d ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ ∪ ( 𝐽 ↾t 𝑌 ) ↔ 𝐹 : ∪ 𝐾 –1-1-onto→ ∪ ( 𝐽 ↾t 𝑌 ) ) )
23 17 restuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ ℂ ) → 𝑌 = ∪ ( 𝐽 ↾t 𝑌 ) )
24 15 7 23 sylancr ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝑌 = ∪ ( 𝐽 ↾t 𝑌 ) )
25 24 f1oeq3d ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ 𝐹 : 𝑋 –1-1-onto→ ∪ ( 𝐽 ↾t 𝑌 ) ) )
26 simpl ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝐾 ∈ Comp )
27 1 cnfldhaus ⊢ 𝐽 ∈ Haus
28 cnex ⊢ ℂ ∈ V
29 28 ssex ⊢ ( 𝑌 ⊆ ℂ → 𝑌 ∈ V )
30 7 29 syl ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → 𝑌 ∈ V )
31 resthaus ⊢ ( ( 𝐽 ∈ Haus ∧ 𝑌 ∈ V ) → ( 𝐽 ↾t 𝑌 ) ∈ Haus )
32 27 30 31 sylancr ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐽 ↾t 𝑌 ) ∈ Haus )
33 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
34 eqid ⊢ ∪ ( 𝐽 ↾t 𝑌 ) = ∪ ( 𝐽 ↾t 𝑌 )
35 33 34 cmphaushmeo ⊢ ( ( 𝐾 ∈ Comp ∧ ( 𝐽 ↾t 𝑌 ) ∈ Haus ∧ 𝐹 ∈ ( 𝐾 Cn ( 𝐽 ↾t 𝑌 ) ) ) → ( 𝐹 ∈ ( 𝐾 Homeo ( 𝐽 ↾t 𝑌 ) ) ↔ 𝐹 : ∪ 𝐾 –1-1-onto→ ∪ ( 𝐽 ↾t 𝑌 ) ) )
36 26 32 11 35 syl3anc ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐾 Homeo ( 𝐽 ↾t 𝑌 ) ) ↔ 𝐹 : ∪ 𝐾 –1-1-onto→ ∪ ( 𝐽 ↾t 𝑌 ) ) )
37 22 25 36 3bitr4d ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ 𝐹 ∈ ( 𝐾 Homeo ( 𝐽 ↾t 𝑌 ) ) ) )
38 1 8 2 cncfcn ⊢ ( ( 𝑌 ⊆ ℂ ∧ 𝑋 ⊆ ℂ ) → ( 𝑌 –cn→ 𝑋 ) = ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) )
39 7 5 38 syl2anc ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝑌 –cn→ 𝑋 ) = ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) )
40 39 eleq2d ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( ◡ 𝐹 ∈ ( 𝑌 –cn→ 𝑋 ) ↔ ◡ 𝐹 ∈ ( ( 𝐽 ↾t 𝑌 ) Cn 𝐾 ) ) )
41 14 37 40 3bitr4d ⊢ ( ( 𝐾 ∈ Comp ∧ 𝐹 ∈ ( 𝑋 –cn→ 𝑌 ) ) → ( 𝐹 : 𝑋 –1-1-onto→ 𝑌 ↔ ◡ 𝐹 ∈ ( 𝑌 –cn→ 𝑋 ) ) )