Metamath Proof Explorer

Theorem iccf1o

Description: Describe a bijection from [ 0 , 1 ] to an arbitrary nontrivial closed interval [ A , B ] . (Contributed by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypothesis iccf1o.1 
|- F = ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) )
Assertion 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 iccf1o.1 
 |-  F = ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) )
2 elicc01 
 |-  ( x e. ( 0 [,] 1 ) <-> ( x e. RR /\ 0 <_ x /\ x <_ 1 ) )
3 2 simp1bi 
 |-  ( x e. ( 0 [,] 1 ) -> x e. RR )
4 3 adantl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> x e. RR )
5 4 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> x e. CC )
6 simpl2 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> B e. RR )
7 6 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> B e. CC )
8 5 7 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( x x. B ) e. CC )
9 ax-1cn 
 |-  1 e. CC
10 subcl 
 |-  ( ( 1 e. CC /\ x e. CC ) -> ( 1 - x ) e. CC )
11 9 5 10 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( 1 - x ) e. CC )
12 simpl1 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> A e. RR )
13 12 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> A e. CC )
14 11 13 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( 1 - x ) x. A ) e. CC )
15 8 14 addcomd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) = ( ( ( 1 - x ) x. A ) + ( x x. B ) ) )
16 lincmb01cmp 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( ( 1 - x ) x. A ) + ( x x. B ) ) e. ( A [,] B ) )
17 15 16 eqeltrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) e. ( A [,] B ) )
18 simpr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> y e. ( A [,] B ) )
19 simpl1 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> A e. RR )
20 simpl2 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> B e. RR )
21 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
22 21 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
23 22 biimpa 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( y e. RR /\ A <_ y /\ y <_ B ) )
24 23 simp1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> y e. RR )
25 eqid 
 |-  ( A - A ) = ( A - A )
26 eqid 
 |-  ( B - A ) = ( B - A )
27 25 26 iccshftl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( y e. RR /\ A e. RR ) ) -> ( y e. ( A [,] B ) <-> ( y - A ) e. ( ( A - A ) [,] ( B - A ) ) ) )
28 19 20 24 19 27 syl22anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( y e. ( A [,] B ) <-> ( y - A ) e. ( ( A - A ) [,] ( B - A ) ) ) )
29 18 28 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( y - A ) e. ( ( A - A ) [,] ( B - A ) ) )
30 24 19 resubcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( y - A ) e. RR )
31 30 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( y - A ) e. CC )
32 difrp 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( B - A ) e. RR+ ) )
33 32 biimp3a 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( B - A ) e. RR+ )
34 33 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( B - A ) e. RR+ )
35 34 rpcnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( B - A ) e. CC )
36 34 rpne0d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( B - A ) =/= 0 )
37 31 35 36 divcan1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( ( ( y - A ) / ( B - A ) ) x. ( B - A ) ) = ( y - A ) )
38 35 mul02d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( 0 x. ( B - A ) ) = 0 )
39 19 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> A e. CC )
40 39 subidd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( A - A ) = 0 )
41 38 40 eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( 0 x. ( B - A ) ) = ( A - A ) )
42 35 mulid2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( 1 x. ( B - A ) ) = ( B - A ) )
43 41 42 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( ( 0 x. ( B - A ) ) [,] ( 1 x. ( B - A ) ) ) = ( ( A - A ) [,] ( B - A ) ) )
44 29 37 43 3eltr4d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( ( ( y - A ) / ( B - A ) ) x. ( B - A ) ) e. ( ( 0 x. ( B - A ) ) [,] ( 1 x. ( B - A ) ) ) )
45 0red 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> 0 e. RR )
46 1red 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> 1 e. RR )
47 30 34 rerpdivcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( ( y - A ) / ( B - A ) ) e. RR )
48 eqid 
 |-  ( 0 x. ( B - A ) ) = ( 0 x. ( B - A ) )
49 eqid 
 |-  ( 1 x. ( B - A ) ) = ( 1 x. ( B - A ) )
50 48 49 iccdil 
 |-  ( ( ( 0 e. RR /\ 1 e. RR ) /\ ( ( ( y - A ) / ( B - A ) ) e. RR /\ ( B - A ) e. RR+ ) ) -> ( ( ( y - A ) / ( B - A ) ) e. ( 0 [,] 1 ) <-> ( ( ( y - A ) / ( B - A ) ) x. ( B - A ) ) e. ( ( 0 x. ( B - A ) ) [,] ( 1 x. ( B - A ) ) ) ) )
51 45 46 47 34 50 syl22anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( ( ( y - A ) / ( B - A ) ) e. ( 0 [,] 1 ) <-> ( ( ( y - A ) / ( B - A ) ) x. ( B - A ) ) e. ( ( 0 x. ( B - A ) ) [,] ( 1 x. ( B - A ) ) ) ) )
52 44 51 mpbird 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( ( y - A ) / ( B - A ) ) e. ( 0 [,] 1 ) )
53 eqcom 
 |-  ( x = ( ( y - A ) / ( B - A ) ) <-> ( ( y - A ) / ( B - A ) ) = x )
54 31 adantrl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( y - A ) e. CC )
55 5 adantrr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> x e. CC )
56 35 adantrl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( B - A ) e. CC )
57 36 adantrl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( B - A ) =/= 0 )
58 54 55 56 57 divmul3d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( ( ( y - A ) / ( B - A ) ) = x <-> ( y - A ) = ( x x. ( B - A ) ) ) )
59 53 58 syl5bb 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( x = ( ( y - A ) / ( B - A ) ) <-> ( y - A ) = ( x x. ( B - A ) ) ) )
60 24 adantrl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> y e. RR )
61 60 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> y e. CC )
62 39 adantrl 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> A e. CC )
63 6 12 resubcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( B - A ) e. RR )
64 4 63 remulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( x x. ( B - A ) ) e. RR )
65 64 adantrr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( x x. ( B - A ) ) e. RR )
66 65 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( x x. ( B - A ) ) e. CC )
67 61 62 66 subadd2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( ( y - A ) = ( x x. ( B - A ) ) <-> ( ( x x. ( B - A ) ) + A ) = y ) )
68 eqcom 
 |-  ( ( ( x x. ( B - A ) ) + A ) = y <-> y = ( ( x x. ( B - A ) ) + A ) )
69 67 68 bitrdi 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( ( y - A ) = ( x x. ( B - A ) ) <-> y = ( ( x x. ( B - A ) ) + A ) ) )
70 5 13 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( x x. A ) e. CC )
71 8 70 13 subadd23d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( ( x x. B ) - ( x x. A ) ) + A ) = ( ( x x. B ) + ( A - ( x x. A ) ) ) )
72 5 7 13 subdid 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( x x. ( B - A ) ) = ( ( x x. B ) - ( x x. A ) ) )
73 72 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( x x. ( B - A ) ) + A ) = ( ( ( x x. B ) - ( x x. A ) ) + A ) )
74 1cnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> 1 e. CC )
75 74 5 13 subdird 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( 1 - x ) x. A ) = ( ( 1 x. A ) - ( x x. A ) ) )
76 13 mulid2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( 1 x. A ) = A )
77 76 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( 1 x. A ) - ( x x. A ) ) = ( A - ( x x. A ) ) )
78 75 77 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( 1 - x ) x. A ) = ( A - ( x x. A ) ) )
79 78 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) = ( ( x x. B ) + ( A - ( x x. A ) ) ) )
80 71 73 79 3eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( x x. ( B - A ) ) + A ) = ( ( x x. B ) + ( ( 1 - x ) x. A ) ) )
81 80 adantrr 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( ( x x. ( B - A ) ) + A ) = ( ( x x. B ) + ( ( 1 - x ) x. A ) ) )
82 81 eqeq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( y = ( ( x x. ( B - A ) ) + A ) <-> y = ( ( x x. B ) + ( ( 1 - x ) x. A ) ) ) )
83 59 69 82 3bitrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( x = ( ( y - A ) / ( B - A ) ) <-> y = ( ( x x. B ) + ( ( 1 - x ) x. A ) ) ) )
84 1 17 52 83 f1ocnv2d 
 |-  ( ( 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 ) ) ) ) )