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)

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

Proof

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

Metamath Proof Explorer

Theorem icchmeo

Proof