Metamath Proof Explorer

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

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