Metamath Proof Explorer

Theorem icoshftf1o

Description: Shifting a closed-below, open-above interval is one-to-one onto. (Contributed by Paul Chapman, 25-Mar-2008) (Proof shortened by Mario Carneiro, 1-Sep-2015)

Ref Expression
Hypothesis icoshftf1o.1 
|- F = ( x e. ( A [,) B ) |-> ( x + C ) )
Assertion icoshftf1o 
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> F : ( A [,) B ) -1-1-onto-> ( ( A + C ) [,) ( B + C ) ) )

Proof

Step Hyp Ref Expression
1 icoshftf1o.1 
 |-  F = ( x e. ( A [,) B ) |-> ( x + C ) )
2 icoshft 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( x e. ( A [,) B ) -> ( x + C ) e. ( ( A + C ) [,) ( B + C ) ) ) )
3 2 ralrimiv 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A. x e. ( A [,) B ) ( x + C ) e. ( ( A + C ) [,) ( B + C ) ) )
4 readdcl 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A + C ) e. RR )
5 4 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A + C ) e. RR )
6 readdcl 
 |-  ( ( B e. RR /\ C e. RR ) -> ( B + C ) e. RR )
7 6 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B + C ) e. RR )
8 renegcl 
 |-  ( C e. RR -> -u C e. RR )
9 8 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> -u C e. RR )
10 icoshft 
 |-  ( ( ( A + C ) e. RR /\ ( B + C ) e. RR /\ -u C e. RR ) -> ( y e. ( ( A + C ) [,) ( B + C ) ) -> ( y + -u C ) e. ( ( ( A + C ) + -u C ) [,) ( ( B + C ) + -u C ) ) ) )
11 5 7 9 10 syl3anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( y e. ( ( A + C ) [,) ( B + C ) ) -> ( y + -u C ) e. ( ( ( A + C ) + -u C ) [,) ( ( B + C ) + -u C ) ) ) )
12 11 imp 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) -> ( y + -u C ) e. ( ( ( A + C ) + -u C ) [,) ( ( B + C ) + -u C ) ) )
13 7 rexrd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B + C ) e. RR* )
14 icossre 
 |-  ( ( ( A + C ) e. RR /\ ( B + C ) e. RR* ) -> ( ( A + C ) [,) ( B + C ) ) C_ RR )
15 5 13 14 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + C ) [,) ( B + C ) ) C_ RR )
16 15 sselda 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) -> y e. RR )
17 16 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) -> y e. CC )
18 simpl3 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) -> C e. RR )
19 18 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) -> C e. CC )
20 17 19 negsubd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) -> ( y + -u C ) = ( y - C ) )
21 5 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A + C ) e. CC )
22 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
23 22 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. CC )
24 21 23 negsubd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + C ) + -u C ) = ( ( A + C ) - C ) )
25 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
26 25 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. CC )
27 26 23 pncand 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + C ) - C ) = A )
28 24 27 eqtrd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A + C ) + -u C ) = A )
29 7 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B + C ) e. CC )
30 29 23 negsubd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( B + C ) + -u C ) = ( ( B + C ) - C ) )
31 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
32 31 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. CC )
33 32 23 pncand 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( B + C ) - C ) = B )
34 30 33 eqtrd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( B + C ) + -u C ) = B )
35 28 34 oveq12d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( A + C ) + -u C ) [,) ( ( B + C ) + -u C ) ) = ( A [,) B ) )
36 35 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) -> ( ( ( A + C ) + -u C ) [,) ( ( B + C ) + -u C ) ) = ( A [,) B ) )
37 12 20 36 3eltr3d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) -> ( y - C ) e. ( A [,) B ) )
38 reueq 
 |-  ( ( y - C ) e. ( A [,) B ) <-> E! x e. ( A [,) B ) x = ( y - C ) )
39 37 38 sylib 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) -> E! x e. ( A [,) B ) x = ( y - C ) )
40 16 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) /\ x e. ( A [,) B ) ) -> y e. RR )
41 40 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) /\ x e. ( A [,) B ) ) -> y e. CC )
42 simpll3 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) /\ x e. ( A [,) B ) ) -> C e. RR )
43 42 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) /\ x e. ( A [,) B ) ) -> C e. CC )
44 simpl1 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) -> A e. RR )
45 simpl2 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) -> B e. RR )
46 45 rexrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) -> B e. RR* )
47 icossre 
 |-  ( ( A e. RR /\ B e. RR* ) -> ( A [,) B ) C_ RR )
48 44 46 47 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) -> ( A [,) B ) C_ RR )
49 48 sselda 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) /\ x e. ( A [,) B ) ) -> x e. RR )
50 49 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) /\ x e. ( A [,) B ) ) -> x e. CC )
51 41 43 50 subadd2d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) /\ x e. ( A [,) B ) ) -> ( ( y - C ) = x <-> ( x + C ) = y ) )
52 eqcom 
 |-  ( x = ( y - C ) <-> ( y - C ) = x )
53 eqcom 
 |-  ( y = ( x + C ) <-> ( x + C ) = y )
54 51 52 53 3bitr4g 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) /\ x e. ( A [,) B ) ) -> ( x = ( y - C ) <-> y = ( x + C ) ) )
55 54 reubidva 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) -> ( E! x e. ( A [,) B ) x = ( y - C ) <-> E! x e. ( A [,) B ) y = ( x + C ) ) )
56 39 55 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ y e. ( ( A + C ) [,) ( B + C ) ) ) -> E! x e. ( A [,) B ) y = ( x + C ) )
57 56 ralrimiva 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A. y e. ( ( A + C ) [,) ( B + C ) ) E! x e. ( A [,) B ) y = ( x + C ) )
58 1 f1ompt 
 |-  ( F : ( A [,) B ) -1-1-onto-> ( ( A + C ) [,) ( B + C ) ) <-> ( A. x e. ( A [,) B ) ( x + C ) e. ( ( A + C ) [,) ( B + C ) ) /\ A. y e. ( ( A + C ) [,) ( B + C ) ) E! x e. ( A [,) B ) y = ( x + C ) ) )
59 3 57 58 sylanbrc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> F : ( A [,) B ) -1-1-onto-> ( ( A + C ) [,) ( B + C ) ) )