Theorem 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 ` CCfld )
	icchmeo.f	|- F = ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) )
Assertion	icchmeo	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> F e. ( II Homeo ( J |`t ( A [,] B ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		icchmeo.j	|- J = ( TopOpen ` CCfld )
2		icchmeo.f	|- F = ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) )
3		iitopon	|- II e. ( TopOn ` ( 0 [,] 1 ) )
4	3	a1i	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
5	1	dfii3	|- II = ( J |`t ( 0 [,] 1 ) )
6	5	oveq2i	|- ( II Cn II ) = ( II Cn ( J |`t ( 0 [,] 1 ) ) )
7	1	cnfldtop	|- J e. Top
8		cnrest2r	|- ( J e. Top -> ( II Cn ( J |`t ( 0 [,] 1 ) ) ) C_ ( II Cn J ) )
9	7 8	ax-mp	|- ( II Cn ( J |`t ( 0 [,] 1 ) ) ) C_ ( II Cn J )
10	6 9	eqsstri	|- ( II Cn II ) C_ ( II Cn J )
11	4	cnmptid	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> x ) e. ( II Cn II ) )
12	10 11	sseldi	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> x ) e. ( II Cn J ) )
13	1	cnfldtopon	|- J e. ( TopOn ` CC )
14	13	a1i	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> J e. ( TopOn ` CC ) )
15		simp2	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> B e. RR )
16	15	recnd	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> B e. CC )
17	4 14 16	cnmptc	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> B ) e. ( II Cn J ) )
18	1	mulcn	|- x. e. ( ( J tX J ) Cn J )
19	18	a1i	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> x. e. ( ( J tX J ) Cn J ) )
20	4 12 17 19	cnmpt12f	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> ( x x. B ) ) e. ( II Cn J ) )
21		1cnd	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> 1 e. CC )
22	4 14 21	cnmptc	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> 1 ) e. ( II Cn J ) )
23	1	subcn	|- - e. ( ( J tX J ) Cn J )
24	23	a1i	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> - e. ( ( J tX J ) Cn J ) )
25	4 22 12 24	cnmpt12f	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> ( 1 - x ) ) e. ( II Cn J ) )
26		simp1	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> A e. RR )
27	26	recnd	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> A e. CC )
28	4 14 27	cnmptc	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> A ) e. ( II Cn J ) )
29	4 25 28 19	cnmpt12f	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> ( ( 1 - x ) x. A ) ) e. ( II Cn J ) )
30	1	addcn	|- + e. ( ( J tX J ) Cn J )
31	30	a1i	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> + e. ( ( J tX J ) Cn J ) )
32	4 20 29 31	cnmpt12f	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) ) e. ( II Cn J ) )
33	2 32	eqeltrid	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> F e. ( II Cn J ) )
34	2	iccf1o	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( F : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) /\ `' F = ( y e. ( A [,] B ) |-> ( ( y - A ) / ( B - A ) ) ) ) )
35	34	simpld	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> F : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) )
36		f1of	|- ( F : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) -> F : ( 0 [,] 1 ) --> ( A [,] B ) )
37		frn	|- ( F : ( 0 [,] 1 ) --> ( A [,] B ) -> ran F C_ ( A [,] B ) )
38	35 36 37	3syl	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ran F C_ ( A [,] B ) )
39		iccssre	|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
40	39	3adant3	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( A [,] B ) C_ RR )
41		ax-resscn	|- RR C_ CC
42	40 41	sstrdi	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( A [,] B ) C_ CC )
43		cnrest2	|- ( ( J e. ( TopOn ` CC ) /\ ran F C_ ( A [,] B ) /\ ( A [,] B ) C_ CC ) -> ( F e. ( II Cn J ) <-> F e. ( II Cn ( J |`t ( A [,] B ) ) ) ) )
44	13 38 42 43	mp3an2i	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( F e. ( II Cn J ) <-> F e. ( II Cn ( J |`t ( A [,] B ) ) ) ) )
45	33 44	mpbid	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> F e. ( II Cn ( J |`t ( A [,] B ) ) ) )
46	34	simprd	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> `' F = ( y e. ( A [,] B ) |-> ( ( y - A ) / ( B - A ) ) ) )
47		resttopon	|- ( ( J e. ( TopOn ` CC ) /\ ( A [,] B ) C_ CC ) -> ( J |`t ( A [,] B ) ) e. ( TopOn ` ( A [,] B ) ) )
48	13 42 47	sylancr	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( J |`t ( A [,] B ) ) e. ( TopOn ` ( A [,] B ) ) )
49		cnrest2r	|- ( J e. Top -> ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( A [,] B ) ) ) C_ ( ( J |`t ( A [,] B ) ) Cn J ) )
50	7 49	ax-mp	|- ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( A [,] B ) ) ) C_ ( ( J |`t ( A [,] B ) ) Cn J )
51	48	cnmptid	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) |-> y ) e. ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( A [,] B ) ) ) )
52	50 51	sseldi	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) |-> y ) e. ( ( J |`t ( A [,] B ) ) Cn J ) )
53	48 14 27	cnmptc	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) |-> A ) e. ( ( J |`t ( A [,] B ) ) Cn J ) )
54	48 52 53 24	cnmpt12f	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) |-> ( y - A ) ) e. ( ( J |`t ( A [,] B ) ) Cn J ) )
55		difrp	|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( B - A ) e. RR+ ) )
56	55	biimp3a	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( B - A ) e. RR+ )
57	56	rpcnd	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( B - A ) e. CC )
58	56	rpne0d	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( B - A ) =/= 0 )
59	1	divccn	|- ( ( ( B - A ) e. CC /\ ( B - A ) =/= 0 ) -> ( x e. CC |-> ( x / ( B - A ) ) ) e. ( J Cn J ) )
60	57 58 59	syl2anc	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. CC |-> ( x / ( B - A ) ) ) e. ( J Cn J ) )
61		oveq1	|- ( x = ( y - A ) -> ( x / ( B - A ) ) = ( ( y - A ) / ( B - A ) ) )
62	48 54 14 60 61	cnmpt11	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) |-> ( ( y - A ) / ( B - A ) ) ) e. ( ( J |`t ( A [,] B ) ) Cn J ) )
63	46 62	eqeltrd	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> `' F e. ( ( J |`t ( A [,] B ) ) Cn J ) )
64		dfdm4	|- dom F = ran `' F
65	64	eqimss2i	|- ran `' F C_ dom F
66		f1odm	|- ( F : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) -> dom F = ( 0 [,] 1 ) )
67	35 66	syl	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> dom F = ( 0 [,] 1 ) )
68	65 67	sseqtrid	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ran `' F C_ ( 0 [,] 1 ) )
69		unitssre	|- ( 0 [,] 1 ) C_ RR
70	69	a1i	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( 0 [,] 1 ) C_ RR )
71	70 41	sstrdi	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( 0 [,] 1 ) C_ CC )
72		cnrest2	|- ( ( J e. ( TopOn ` CC ) /\ ran `' F C_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) C_ CC ) -> ( `' F e. ( ( J |`t ( A [,] B ) ) Cn J ) <-> `' F e. ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( 0 [,] 1 ) ) ) ) )
73	13 68 71 72	mp3an2i	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( `' F e. ( ( J |`t ( A [,] B ) ) Cn J ) <-> `' F e. ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( 0 [,] 1 ) ) ) ) )
74	63 73	mpbid	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> `' F e. ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( 0 [,] 1 ) ) ) )
75	5	oveq2i	|- ( ( J |`t ( A [,] B ) ) Cn II ) = ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( 0 [,] 1 ) ) )
76	74 75	eleqtrrdi	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> `' F e. ( ( J |`t ( A [,] B ) ) Cn II ) )
77		ishmeo	|- ( F e. ( II Homeo ( J |`t ( A [,] B ) ) ) <-> ( F e. ( II Cn ( J |`t ( A [,] B ) ) ) /\ `' F e. ( ( J |`t ( A [,] B ) ) Cn II ) ) )
78	45 76 77	sylanbrc	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> F e. ( II Homeo ( J |`t ( A [,] B ) ) ) )