cncfcnvcn

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

	Ref	Expression
Hypotheses	cncfcnvcn.j	$⊢ J = TopOpen (ℂ_{fld})$
	cncfcnvcn.k	$⊢ K = J ↾_{𝑡} X$
Assertion	cncfcnvcn	$⊢ (K \in Comp \land F : X \underset{cn}{⟶} Y) \to (F : X \underset{1-1 onto}{⟶} Y \leftrightarrow F^{-1} : Y \underset{cn}{⟶} X)$

Proof

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

Metamath Proof Explorer

Theorem cncfcnvcn

Proof