cnrehmeo

Description: The canonical bijection from ( RR X. RR ) to CC described in cnref1o is in fact a homeomorphism of the usual topologies on these sets. (It is also an isometry, if ( RR X. RR ) is metrized with the l² norm.) (Contributed by Mario Carneiro, 25-Aug-2014)

	Ref	Expression
Hypotheses	cnrehmeo.1	$⊢ F = (x \in ℝ, y \in ℝ ⟼ x + i y)$
	cnrehmeo.2	$⊢ J = topGen (ran (.))$
	cnrehmeo.3	$⊢ K = TopOpen (ℂ_{fld})$
Assertion	cnrehmeo	$⊢ F \in ((J \times_{t} J) Homeo K)$

Proof

Step	Hyp	Ref	Expression
1		cnrehmeo.1	$⊢ F = (x \in ℝ, y \in ℝ ⟼ x + i y)$
2		cnrehmeo.2	$⊢ J = topGen (ran (.))$
3		cnrehmeo.3	$⊢ K = TopOpen (ℂ_{fld})$
4		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
5	2 4	eqeltri	$⊢ J \in TopOn (ℝ)$
6	5	a1i	$⊢ ⊤ \to J \in TopOn (ℝ)$
7	3	cnfldtop	$⊢ K \in Top$
8		cnrest2r	$⊢ K \in Top \to (J \times_{t} J) Cn (K ↾_{𝑡} ℝ) \subseteq (J \times_{t} J) Cn K$
9	7 8	mp1i	$⊢ ⊤ \to (J \times_{t} J) Cn (K ↾_{𝑡} ℝ) \subseteq (J \times_{t} J) Cn K$
10	6 6	cnmpt1st	$⊢ ⊤ \to (x \in ℝ, y \in ℝ ⟼ x) \in ((J \times_{t} J) Cn J)$
11	3	tgioo2	$⊢ topGen (ran (.)) = K ↾_{𝑡} ℝ$
12	2 11	eqtri	$⊢ J = K ↾_{𝑡} ℝ$
13	12	oveq2i	$⊢ (J \times_{t} J) Cn J = (J \times_{t} J) Cn (K ↾_{𝑡} ℝ)$
14	10 13	eleqtrdi	$⊢ ⊤ \to (x \in ℝ, y \in ℝ ⟼ x) \in ((J \times_{t} J) Cn (K ↾_{𝑡} ℝ))$
15	9 14	sseldd	$⊢ ⊤ \to (x \in ℝ, y \in ℝ ⟼ x) \in ((J \times_{t} J) Cn K)$
16	3	cnfldtopon	$⊢ K \in TopOn (ℂ)$
17	16	a1i	$⊢ ⊤ \to K \in TopOn (ℂ)$
18		ax-icn	$⊢ i \in ℂ$
19	18	a1i	$⊢ ⊤ \to i \in ℂ$
20	6 6 17 19	cnmpt2c	$⊢ ⊤ \to (x \in ℝ, y \in ℝ ⟼ i) \in ((J \times_{t} J) Cn K)$
21	6 6	cnmpt2nd	$⊢ ⊤ \to (x \in ℝ, y \in ℝ ⟼ y) \in ((J \times_{t} J) Cn J)$
22	21 13	eleqtrdi	$⊢ ⊤ \to (x \in ℝ, y \in ℝ ⟼ y) \in ((J \times_{t} J) Cn (K ↾_{𝑡} ℝ))$
23	9 22	sseldd	$⊢ ⊤ \to (x \in ℝ, y \in ℝ ⟼ y) \in ((J \times_{t} J) Cn K)$
24	3	mulcn	$⊢ \times \in ((K \times_{t} K) Cn K)$
25	24	a1i	$⊢ ⊤ \to \times \in ((K \times_{t} K) Cn K)$
26	6 6 20 23 25	cnmpt22f	$⊢ ⊤ \to (x \in ℝ, y \in ℝ ⟼ i y) \in ((J \times_{t} J) Cn K)$
27	3	addcn	$⊢ + \in ((K \times_{t} K) Cn K)$
28	27	a1i	$⊢ ⊤ \to + \in ((K \times_{t} K) Cn K)$
29	6 6 15 26 28	cnmpt22f	$⊢ ⊤ \to (x \in ℝ, y \in ℝ ⟼ x + i y) \in ((J \times_{t} J) Cn K)$
30	1 29	eqeltrid	$⊢ ⊤ \to F \in ((J \times_{t} J) Cn K)$
31	1	cnrecnv	$⊢ F^{-1} = (z \in ℂ ⟼ ⟨ℜ (z), ℑ (z)⟩)$
32		ref	$⊢ ℜ : ℂ ⟶ ℝ$
33	32	a1i	$⊢ ⊤ \to ℜ : ℂ ⟶ ℝ$
34	33	feqmptd	$⊢ ⊤ \to ℜ = (z \in ℂ ⟼ ℜ (z))$
35		recncf	$⊢ ℜ : ℂ \underset{cn}{⟶} ℝ$
36		ssid	$⊢ ℂ \subseteq ℂ$
37		ax-resscn	$⊢ ℝ \subseteq ℂ$
38	16	toponrestid	$⊢ K = K ↾_{𝑡} ℂ$
39	3 38 12	cncfcn	$⊢ (ℂ \subseteq ℂ \land ℝ \subseteq ℂ) \to ℂ \underset{cn}{⟶} ℝ = K Cn J$
40	36 37 39	mp2an	$⊢ ℂ \underset{cn}{⟶} ℝ = K Cn J$
41	35 40	eleqtri	$⊢ ℜ \in (K Cn J)$
42	34 41	eqeltrrdi	$⊢ ⊤ \to (z \in ℂ ⟼ ℜ (z)) \in (K Cn J)$
43		imf	$⊢ ℑ : ℂ ⟶ ℝ$
44	43	a1i	$⊢ ⊤ \to ℑ : ℂ ⟶ ℝ$
45	44	feqmptd	$⊢ ⊤ \to ℑ = (z \in ℂ ⟼ ℑ (z))$
46		imcncf	$⊢ ℑ : ℂ \underset{cn}{⟶} ℝ$
47	46 40	eleqtri	$⊢ ℑ \in (K Cn J)$
48	45 47	eqeltrrdi	$⊢ ⊤ \to (z \in ℂ ⟼ ℑ (z)) \in (K Cn J)$
49	17 42 48	cnmpt1t	$⊢ ⊤ \to (z \in ℂ ⟼ ⟨ℜ (z), ℑ (z)⟩) \in (K Cn (J \times_{t} J))$
50	31 49	eqeltrid	$⊢ ⊤ \to F^{-1} \in (K Cn (J \times_{t} J))$
51		ishmeo	$⊢ F \in ((J \times_{t} J) Homeo K) \leftrightarrow (F \in ((J \times_{t} J) Cn K) \land F^{-1} \in (K Cn (J \times_{t} J)))$
52	30 50 51	sylanbrc	$⊢ ⊤ \to F \in ((J \times_{t} J) Homeo K)$
53	52	mptru	$⊢ F \in ((J \times_{t} J) Homeo K)$

Metamath Proof Explorer

Theorem cnrehmeo

Proof