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)

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 sselid
 |-  ( ( 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 sselid
 |-  ( ( 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 ) ) ) )