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	icchmeo.j	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
	icchmeo.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) )
Assertion	icchmeo	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐹 ∈ ( II Homeo ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		icchmeo.j	⊢ 𝐽 = ( TopOpen ‘ ℂ_fld )
2		icchmeo.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) )
3		iitopon	⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
4	3	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
5	1	dfii3	⊢ II = ( 𝐽 ↾_t ( 0 [,] 1 ) )
6	5	eqcomi	⊢ ( 𝐽 ↾_t ( 0 [,] 1 ) ) = II
7	6	oveq2i	⊢ ( II Cn ( 𝐽 ↾_t ( 0 [,] 1 ) ) ) = ( II Cn II )
8	1	cnfldtop	⊢ 𝐽 ∈ Top
9		cnrest2r	⊢ ( 𝐽 ∈ Top → ( II Cn ( 𝐽 ↾_t ( 0 [,] 1 ) ) ) ⊆ ( II Cn 𝐽 ) )
10	8 9	ax-mp	⊢ ( II Cn ( 𝐽 ↾_t ( 0 [,] 1 ) ) ) ⊆ ( II Cn 𝐽 )
11	7 10	eqsstrri	⊢ ( II Cn II ) ⊆ ( II Cn 𝐽 )
12	4	cnmptid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 𝑥 ) ∈ ( II Cn II ) )
13	11 12	sselid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 𝑥 ) ∈ ( II Cn 𝐽 ) )
14	1	cnfldtopon	⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
15	14	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐽 ∈ ( TopOn ‘ ℂ ) )
16		simp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ )
17	16	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℂ )
18	4 15 17	cnmptc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 𝐵 ) ∈ ( II Cn 𝐽 ) )
19	1	mpomulcn	⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×_t 𝐽 ) Cn 𝐽 )
20	19	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×_t 𝐽 ) Cn 𝐽 ) )
21		oveq12	⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝐵 ) → ( 𝑢 · 𝑣 ) = ( 𝑥 · 𝐵 ) )
22	4 13 18 15 15 20 21	cnmpt12	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 · 𝐵 ) ) ∈ ( II Cn 𝐽 ) )
23		1cnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 1 ∈ ℂ )
24	4 15 23	cnmptc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 1 ) ∈ ( II Cn 𝐽 ) )
25	1	subcn	⊢ − ∈ ( ( 𝐽 ×_t 𝐽 ) Cn 𝐽 )
26	25	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → − ∈ ( ( 𝐽 ×_t 𝐽 ) Cn 𝐽 ) )
27	4 24 13 26	cnmpt12f	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( 1 − 𝑥 ) ) ∈ ( II Cn 𝐽 ) )
28		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ )
29	28	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℂ )
30	4 15 29	cnmptc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ 𝐴 ) ∈ ( II Cn 𝐽 ) )
31		oveq12	⊢ ( ( 𝑢 = ( 1 − 𝑥 ) ∧ 𝑣 = 𝐴 ) → ( 𝑢 · 𝑣 ) = ( ( 1 − 𝑥 ) · 𝐴 ) )
32	4 27 30 15 15 20 31	cnmpt12	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 1 − 𝑥 ) · 𝐴 ) ) ∈ ( II Cn 𝐽 ) )
33	1	addcn	⊢ + ∈ ( ( 𝐽 ×_t 𝐽 ) Cn 𝐽 )
34	33	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → + ∈ ( ( 𝐽 ×_t 𝐽 ) Cn 𝐽 ) )
35	4 22 32 34	cnmpt12f	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑥 · 𝐵 ) + ( ( 1 − 𝑥 ) · 𝐴 ) ) ) ∈ ( II Cn 𝐽 ) )
36	2 35	eqeltrid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐹 ∈ ( II Cn 𝐽 ) )
37	2	iccf1o	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 𝐴 [,] 𝐵 ) ∧ ^◡ 𝐹 = ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) ) )
38	37	simpld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 𝐴 [,] 𝐵 ) )
39		f1of	⊢ ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 𝐴 [,] 𝐵 ) → 𝐹 : ( 0 [,] 1 ) ⟶ ( 𝐴 [,] 𝐵 ) )
40		frn	⊢ ( 𝐹 : ( 0 [,] 1 ) ⟶ ( 𝐴 [,] 𝐵 ) → ran 𝐹 ⊆ ( 𝐴 [,] 𝐵 ) )
41	38 39 40	3syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ran 𝐹 ⊆ ( 𝐴 [,] 𝐵 ) )
42		iccssre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
43	42	3adant3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
44		ax-resscn	⊢ ℝ ⊆ ℂ
45	43 44	sstrdi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
46		cnrest2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ran 𝐹 ⊆ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℂ ) → ( 𝐹 ∈ ( II Cn 𝐽 ) ↔ 𝐹 ∈ ( II Cn ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) ) ) )
47	14 41 45 46	mp3an2i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐹 ∈ ( II Cn 𝐽 ) ↔ 𝐹 ∈ ( II Cn ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) ) ) )
48	36 47	mpbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐹 ∈ ( II Cn ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) ) )
49	37	simprd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ^◡ 𝐹 = ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) )
50		resttopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℂ ) → ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 [,] 𝐵 ) ) )
51	14 45 50	sylancr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 [,] 𝐵 ) ) )
52		cnrest2r	⊢ ( 𝐽 ∈ Top → ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) ) ⊆ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) )
53	8 52	ax-mp	⊢ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) ) ⊆ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 )
54	51	cnmptid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑦 ) ∈ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) ) )
55	53 54	sselid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝑦 ) ∈ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) )
56	51 15 29	cnmptc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐴 ) ∈ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) )
57	51 55 56 26	cnmpt12f	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝑦 − 𝐴 ) ) ∈ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) )
58		difrp	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( 𝐵 − 𝐴 ) ∈ ℝ⁺ ) )
59	58	biimp3a	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝐵 − 𝐴 ) ∈ ℝ⁺ )
60		rpcnne0	⊢ ( ( 𝐵 − 𝐴 ) ∈ ℝ⁺ → ( ( 𝐵 − 𝐴 ) ∈ ℂ ∧ ( 𝐵 − 𝐴 ) ≠ 0 ) )
61	1	divccn	⊢ ( ( ( 𝐵 − 𝐴 ) ∈ ℂ ∧ ( 𝐵 − 𝐴 ) ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / ( 𝐵 − 𝐴 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
62	59 60 61	3syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / ( 𝐵 − 𝐴 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
63		oveq1	⊢ ( 𝑥 = ( 𝑦 − 𝐴 ) → ( 𝑥 / ( 𝐵 − 𝐴 ) ) = ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) )
64	51 57 15 62 63	cnmpt11	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑦 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) ) ∈ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) )
65	49 64	eqeltrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ^◡ 𝐹 ∈ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) )
66		dfdm4	⊢ dom 𝐹 = ran ^◡ 𝐹
67	66	eqimss2i	⊢ ran ^◡ 𝐹 ⊆ dom 𝐹
68		f1odm	⊢ ( 𝐹 : ( 0 [,] 1 ) –1-1-onto→ ( 𝐴 [,] 𝐵 ) → dom 𝐹 = ( 0 [,] 1 ) )
69	38 68	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → dom 𝐹 = ( 0 [,] 1 ) )
70	67 69	sseqtrid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ran ^◡ 𝐹 ⊆ ( 0 [,] 1 ) )
71		unitsscn	⊢ ( 0 [,] 1 ) ⊆ ℂ
72	71	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( 0 [,] 1 ) ⊆ ℂ )
73		cnrest2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ran ^◡ 𝐹 ⊆ ( 0 [,] 1 ) ∧ ( 0 [,] 1 ) ⊆ ℂ ) → ( ^◡ 𝐹 ∈ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) ↔ ^◡ 𝐹 ∈ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn ( 𝐽 ↾_t ( 0 [,] 1 ) ) ) ) )
74	14 70 72 73	mp3an2i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ( ^◡ 𝐹 ∈ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn 𝐽 ) ↔ ^◡ 𝐹 ∈ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn ( 𝐽 ↾_t ( 0 [,] 1 ) ) ) ) )
75	65 74	mpbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ^◡ 𝐹 ∈ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn ( 𝐽 ↾_t ( 0 [,] 1 ) ) ) )
76	5	oveq2i	⊢ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn II ) = ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn ( 𝐽 ↾_t ( 0 [,] 1 ) ) )
77	75 76	eleqtrrdi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → ^◡ 𝐹 ∈ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn II ) )
78		ishmeo	⊢ ( 𝐹 ∈ ( II Homeo ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) ) ↔ ( 𝐹 ∈ ( II Cn ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) ) ∧ ^◡ 𝐹 ∈ ( ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) Cn II ) ) )
79	48 77 78	sylanbrc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵 ) → 𝐹 ∈ ( II Homeo ( 𝐽 ↾_t ( 𝐴 [,] 𝐵 ) ) ) )

Metamath Proof Explorer

Theorem icchmeo

Proof