gg-icchmeo

Description: The natural bijection from [ 0 , 1 ] to an arbitrary nontrivial closed interval [ A , B ] is a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

	Ref	Expression
Hypotheses	gg-icchmeo.j	$⊢ J = TopOpen (ℂ_{fld})$
	gg-icchmeo.f	$⊢ F = (x \in [0, 1] ⟼ x B + (1 - x) A)$
Assertion	gg-icchmeo	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to F \in (II Homeo (J ↾_{𝑡} [A, B]))$

Proof

Step	Hyp	Ref	Expression
1		gg-icchmeo.j	$⊢ J = TopOpen (ℂ_{fld})$
2		gg-icchmeo.f	$⊢ F = (x \in [0, 1] ⟼ x B + (1 - x) A)$
3		iitopon	$⊢ II \in TopOn ([0, 1])$
4	3	a1i	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to II \in TopOn ([0, 1])$
5	1	dfii3	$⊢ II = J ↾_{𝑡} [0, 1]$
6	5	eqcomi	$⊢ J ↾_{𝑡} [0, 1] = II$
7	6	oveq2i	$⊢ II Cn (J ↾_{𝑡} [0, 1]) = II Cn II$
8	1	cnfldtop	$⊢ J \in Top$
9		cnrest2r	$⊢ J \in Top \to II Cn (J ↾_{𝑡} [0, 1]) \subseteq II Cn J$
10	8 9	ax-mp	$⊢ II Cn (J ↾_{𝑡} [0, 1]) \subseteq II Cn J$
11	7 10	eqsstrri	$⊢ II Cn II \subseteq II Cn J$
12	4	cnmptid	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (x \in [0, 1] ⟼ x) \in (II Cn II)$
13	11 12	sselid	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (x \in [0, 1] ⟼ x) \in (II Cn J)$
14	1	cnfldtopon	$⊢ J \in TopOn (ℂ)$
15	14	a1i	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to J \in TopOn (ℂ)$
16		simp2	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to B \in ℝ$
17	16	recnd	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to B \in ℂ$
18	4 15 17	cnmptc	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (x \in [0, 1] ⟼ B) \in (II Cn J)$
19	1	mpomulcn	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J)$
20	19	a1i	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J)$
21		oveq12	$⊢ (u = x \land v = B) \to u v = x B$
22	4 13 18 15 15 20 21	cnmpt12	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (x \in [0, 1] ⟼ x B) \in (II Cn J)$
23		1cnd	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to 1 \in ℂ$
24	4 15 23	cnmptc	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (x \in [0, 1] ⟼ 1) \in (II Cn J)$
25	1	subcn	$⊢ - \in ((J \times_{t} J) Cn J)$
26	25	a1i	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to - \in ((J \times_{t} J) Cn J)$
27	4 24 13 26	cnmpt12f	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (x \in [0, 1] ⟼ 1 - x) \in (II Cn J)$
28		simp1	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to A \in ℝ$
29	28	recnd	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to A \in ℂ$
30	4 15 29	cnmptc	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (x \in [0, 1] ⟼ A) \in (II Cn J)$
31		oveq12	$⊢ (u = 1 - x \land v = A) \to u v = (1 - x) A$
32	4 27 30 15 15 20 31	cnmpt12	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (x \in [0, 1] ⟼ (1 - x) A) \in (II Cn J)$
33	1	addcn	$⊢ + \in ((J \times_{t} J) Cn J)$
34	33	a1i	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to + \in ((J \times_{t} J) Cn J)$
35	4 22 32 34	cnmpt12f	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (x \in [0, 1] ⟼ x B + (1 - x) A) \in (II Cn J)$
36	2 35	eqeltrid	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to F \in (II Cn J)$
37	2	iccf1o	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (F : [0, 1] \underset{1-1 onto}{⟶} [A, B] \land F^{-1} = (y \in [A, B] ⟼ \frac{y - A}{B - A}))$
38	37	simpld	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to F : [0, 1] \underset{1-1 onto}{⟶} [A, B]$
39		f1of	$⊢ F : [0, 1] \underset{1-1 onto}{⟶} [A, B] \to F : [0, 1] ⟶ [A, B]$
40		frn	$⊢ F : [0, 1] ⟶ [A, B] \to ran F \subseteq [A, B]$
41	38 39 40	3syl	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to ran F \subseteq [A, B]$
42		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
43	42	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to [A, B] \subseteq ℝ$
44		ax-resscn	$⊢ ℝ \subseteq ℂ$
45	43 44	sstrdi	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to [A, B] \subseteq ℂ$
46		cnrest2	$⊢ (J \in TopOn (ℂ) \land ran F \subseteq [A, B] \land [A, B] \subseteq ℂ) \to (F \in (II Cn J) \leftrightarrow F \in (II Cn (J ↾_{𝑡} [A, B])))$
47	14 41 45 46	mp3an2i	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (F \in (II Cn J) \leftrightarrow F \in (II Cn (J ↾_{𝑡} [A, B])))$
48	36 47	mpbid	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to F \in (II Cn (J ↾_{𝑡} [A, B]))$
49	37	simprd	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to F^{-1} = (y \in [A, B] ⟼ \frac{y - A}{B - A})$
50		resttopon	$⊢ (J \in TopOn (ℂ) \land [A, B] \subseteq ℂ) \to J ↾_{𝑡} [A, B] \in TopOn ([A, B])$
51	14 45 50	sylancr	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to J ↾_{𝑡} [A, B] \in TopOn ([A, B])$
52		cnrest2r	$⊢ J \in Top \to (J ↾_{𝑡} [A, B]) Cn (J ↾_{𝑡} [A, B]) \subseteq (J ↾_{𝑡} [A, B]) Cn J$
53	8 52	ax-mp	$⊢ (J ↾_{𝑡} [A, B]) Cn (J ↾_{𝑡} [A, B]) \subseteq (J ↾_{𝑡} [A, B]) Cn J$
54	51	cnmptid	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (y \in [A, B] ⟼ y) \in ((J ↾_{𝑡} [A, B]) Cn (J ↾_{𝑡} [A, B]))$
55	53 54	sselid	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (y \in [A, B] ⟼ y) \in ((J ↾_{𝑡} [A, B]) Cn J)$
56	51 15 29	cnmptc	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (y \in [A, B] ⟼ A) \in ((J ↾_{𝑡} [A, B]) Cn J)$
57	51 55 56 26	cnmpt12f	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (y \in [A, B] ⟼ y - A) \in ((J ↾_{𝑡} [A, B]) Cn J)$
58		difrp	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \leftrightarrow B - A \in ℝ^{+})$
59	58	biimp3a	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to B - A \in ℝ^{+}$
60	59	rpcnd	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to B - A \in ℂ$
61	59	rpne0d	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to B - A \neq 0$
62	1	gg-divccn	$⊢ (B - A \in ℂ \land B - A \neq 0) \to (x \in ℂ ⟼ \frac{x}{B - A}) \in (J Cn J)$
63	60 61 62	syl2anc	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (x \in ℂ ⟼ \frac{x}{B - A}) \in (J Cn J)$
64		oveq1	$⊢ x = y - A \to \frac{x}{B - A} = \frac{y - A}{B - A}$
65	51 57 15 63 64	cnmpt11	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (y \in [A, B] ⟼ \frac{y - A}{B - A}) \in ((J ↾_{𝑡} [A, B]) Cn J)$
66	49 65	eqeltrd	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to F^{-1} \in ((J ↾_{𝑡} [A, B]) Cn J)$
67		dfdm4	$⊢ dom F = ran F^{-1}$
68	67	eqimss2i	$⊢ ran F^{-1} \subseteq dom F$
69		f1odm	$⊢ F : [0, 1] \underset{1-1 onto}{⟶} [A, B] \to dom F = [0, 1]$
70	38 69	syl	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to dom F = [0, 1]$
71	68 70	sseqtrid	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to ran F^{-1} \subseteq [0, 1]$
72		unitssre	$⊢ [0, 1] \subseteq ℝ$
73	72	a1i	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to [0, 1] \subseteq ℝ$
74	73 44	sstrdi	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to [0, 1] \subseteq ℂ$
75		cnrest2	$⊢ (J \in TopOn (ℂ) \land ran F^{-1} \subseteq [0, 1] \land [0, 1] \subseteq ℂ) \to (F^{-1} \in ((J ↾_{𝑡} [A, B]) Cn J) \leftrightarrow F^{-1} \in ((J ↾_{𝑡} [A, B]) Cn (J ↾_{𝑡} [0, 1])))$
76	14 71 74 75	mp3an2i	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (F^{-1} \in ((J ↾_{𝑡} [A, B]) Cn J) \leftrightarrow F^{-1} \in ((J ↾_{𝑡} [A, B]) Cn (J ↾_{𝑡} [0, 1])))$
77	66 76	mpbid	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to F^{-1} \in ((J ↾_{𝑡} [A, B]) Cn (J ↾_{𝑡} [0, 1]))$
78	5	oveq2i	$⊢ (J ↾_{𝑡} [A, B]) Cn II = (J ↾_{𝑡} [A, B]) Cn (J ↾_{𝑡} [0, 1])$
79	77 78	eleqtrrdi	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to F^{-1} \in ((J ↾_{𝑡} [A, B]) Cn II)$
80		ishmeo	$⊢ F \in (II Homeo (J ↾_{𝑡} [A, B])) \leftrightarrow (F \in (II Cn (J ↾_{𝑡} [A, B])) \land F^{-1} \in ((J ↾_{𝑡} [A, B]) Cn II))$
81	48 79 80	sylanbrc	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to F \in (II Homeo (J ↾_{𝑡} [A, B]))$

Metamath Proof Explorer

Theorem gg-icchmeo

Proof