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