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) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

	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	mpomulcn	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) \in ((K \times_{t} K) Cn K)$
25	24	a1i	$⊢ ⊤ \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((K \times_{t} K) Cn K)$
26		oveq12	$⊢ (u = i \land v = y) \to u v = i y$
27	6 6 20 23 17 17 25 26	cnmpt22	$⊢ ⊤ \to (x \in ℝ, y \in ℝ ⟼ i y) \in ((J \times_{t} J) Cn K)$
28	3	addcn	$⊢ + \in ((K \times_{t} K) Cn K)$
29	28	a1i	$⊢ ⊤ \to + \in ((K \times_{t} K) Cn K)$
30	6 6 15 27 29	cnmpt22f	$⊢ ⊤ \to (x \in ℝ, y \in ℝ ⟼ x + i y) \in ((J \times_{t} J) Cn K)$
31	1 30	eqeltrid	$⊢ ⊤ \to F \in ((J \times_{t} J) Cn K)$
32	1	cnrecnv	$⊢ F^{-1} = (z \in ℂ ⟼ ⟨ℜ (z), ℑ (z)⟩)$
33		ref	$⊢ ℜ : ℂ ⟶ ℝ$
34	33	a1i	$⊢ ⊤ \to ℜ : ℂ ⟶ ℝ$
35	34	feqmptd	$⊢ ⊤ \to ℜ = (z \in ℂ ⟼ ℜ (z))$
36		recncf	$⊢ ℜ : ℂ \underset{cn}{⟶} ℝ$
37		ssid	$⊢ ℂ \subseteq ℂ$
38		ax-resscn	$⊢ ℝ \subseteq ℂ$
39	16	toponrestid	$⊢ K = K ↾_{𝑡} ℂ$
40	3 39 12	cncfcn	$⊢ (ℂ \subseteq ℂ \land ℝ \subseteq ℂ) \to ℂ \underset{cn}{⟶} ℝ = K Cn J$
41	37 38 40	mp2an	$⊢ ℂ \underset{cn}{⟶} ℝ = K Cn J$
42	36 41	eleqtri	$⊢ ℜ \in (K Cn J)$
43	35 42	eqeltrrdi	$⊢ ⊤ \to (z \in ℂ ⟼ ℜ (z)) \in (K Cn J)$
44		imf	$⊢ ℑ : ℂ ⟶ ℝ$
45	44	a1i	$⊢ ⊤ \to ℑ : ℂ ⟶ ℝ$
46	45	feqmptd	$⊢ ⊤ \to ℑ = (z \in ℂ ⟼ ℑ (z))$
47		imcncf	$⊢ ℑ : ℂ \underset{cn}{⟶} ℝ$
48	47 41	eleqtri	$⊢ ℑ \in (K Cn J)$
49	46 48	eqeltrrdi	$⊢ ⊤ \to (z \in ℂ ⟼ ℑ (z)) \in (K Cn J)$
50	17 43 49	cnmpt1t	$⊢ ⊤ \to (z \in ℂ ⟼ ⟨ℜ (z), ℑ (z)⟩) \in (K Cn (J \times_{t} J))$
51	32 50	eqeltrid	$⊢ ⊤ \to F^{-1} \in (K Cn (J \times_{t} J))$
52		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)))$
53	31 51 52	sylanbrc	$⊢ ⊤ \to F \in ((J \times_{t} J) Homeo K)$
54	53	mptru	$⊢ F \in ((J \times_{t} J) Homeo K)$

Metamath Proof Explorer

Theorem cnrehmeo

Proof