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 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ↦ ( 𝑥 + 𝐶 ) )
Assertion icoshftf1o ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐹 : ( 𝐴 [,) 𝐵 ) –1-1-onto→ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 icoshftf1o.1 ⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ↦ ( 𝑥 + 𝐶 ) )
2 icoshft ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) → ( 𝑥 + 𝐶 ) ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) )
3 2 ralrimiv ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∀ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ( 𝑥 + 𝐶 ) ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) )
4 readdcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐶 ) ∈ ℝ )
5 4 3adant2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐶 ) ∈ ℝ )
6 readdcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
7 6 3adant1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
8 renegcl ⊢ ( 𝐶 ∈ ℝ → - 𝐶 ∈ ℝ )
9 8 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → - 𝐶 ∈ ℝ )
10 icoshft ⊢ ( ( ( 𝐴 + 𝐶 ) ∈ ℝ ∧ ( 𝐵 + 𝐶 ) ∈ ℝ ∧ - 𝐶 ∈ ℝ ) → ( 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) → ( 𝑦 + - 𝐶 ) ∈ ( ( ( 𝐴 + 𝐶 ) + - 𝐶 ) [,) ( ( 𝐵 + 𝐶 ) + - 𝐶 ) ) ) )
11 5 7 9 10 syl3anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) → ( 𝑦 + - 𝐶 ) ∈ ( ( ( 𝐴 + 𝐶 ) + - 𝐶 ) [,) ( ( 𝐵 + 𝐶 ) + - 𝐶 ) ) ) )
12 11 imp ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) → ( 𝑦 + - 𝐶 ) ∈ ( ( ( 𝐴 + 𝐶 ) + - 𝐶 ) [,) ( ( 𝐵 + 𝐶 ) + - 𝐶 ) ) )
13 7 rexrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + 𝐶 ) ∈ ℝ* )
14 icossre ⊢ ( ( ( 𝐴 + 𝐶 ) ∈ ℝ ∧ ( 𝐵 + 𝐶 ) ∈ ℝ* ) → ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ⊆ ℝ )
15 5 13 14 syl2anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ⊆ ℝ )
16 15 sselda ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) → 𝑦 ∈ ℝ )
17 16 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) → 𝑦 ∈ ℂ )
18 simpl3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) → 𝐶 ∈ ℝ )
19 18 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) → 𝐶 ∈ ℂ )
20 17 19 negsubd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) → ( 𝑦 + - 𝐶 ) = ( 𝑦 − 𝐶 ) )
21 5 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐶 ) ∈ ℂ )
22 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
23 22 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℂ )
24 21 23 negsubd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + 𝐶 ) + - 𝐶 ) = ( ( 𝐴 + 𝐶 ) − 𝐶 ) )
25 simp1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
26 25 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℂ )
27 26 23 pncand ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + 𝐶 ) − 𝐶 ) = 𝐴 )
28 24 27 eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + 𝐶 ) + - 𝐶 ) = 𝐴 )
29 7 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + 𝐶 ) ∈ ℂ )
30 29 23 negsubd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 + 𝐶 ) + - 𝐶 ) = ( ( 𝐵 + 𝐶 ) − 𝐶 ) )
31 simp2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
32 31 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℂ )
33 32 23 pncand ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 + 𝐶 ) − 𝐶 ) = 𝐵 )
34 30 33 eqtrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐵 + 𝐶 ) + - 𝐶 ) = 𝐵 )
35 28 34 oveq12d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 + 𝐶 ) + - 𝐶 ) [,) ( ( 𝐵 + 𝐶 ) + - 𝐶 ) ) = ( 𝐴 [,) 𝐵 ) )
36 35 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) → ( ( ( 𝐴 + 𝐶 ) + - 𝐶 ) [,) ( ( 𝐵 + 𝐶 ) + - 𝐶 ) ) = ( 𝐴 [,) 𝐵 ) )
37 12 20 36 3eltr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) → ( 𝑦 − 𝐶 ) ∈ ( 𝐴 [,) 𝐵 ) )
38 reueq ⊢ ( ( 𝑦 − 𝐶 ) ∈ ( 𝐴 [,) 𝐵 ) ↔ ∃! 𝑥 ∈ ( 𝐴 [,) 𝐵 ) 𝑥 = ( 𝑦 − 𝐶 ) )
39 37 38 sylib ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) → ∃! 𝑥 ∈ ( 𝐴 [,) 𝐵 ) 𝑥 = ( 𝑦 − 𝐶 ) )
40 16 adantr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝑦 ∈ ℝ )
41 40 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝑦 ∈ ℂ )
42 simpll3 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐶 ∈ ℝ )
43 42 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐶 ∈ ℂ )
44 simpl1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) → 𝐴 ∈ ℝ )
45 simpl2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) → 𝐵 ∈ ℝ )
46 45 rexrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) → 𝐵 ∈ ℝ* )
47 icossre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 [,) 𝐵 ) ⊆ ℝ )
48 44 46 47 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) → ( 𝐴 [,) 𝐵 ) ⊆ ℝ )
49 48 sselda ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝑥 ∈ ℝ )
50 49 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝑥 ∈ ℂ )
51 41 43 50 subadd2d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → ( ( 𝑦 − 𝐶 ) = 𝑥 ↔ ( 𝑥 + 𝐶 ) = 𝑦 ) )
52 eqcom ⊢ ( 𝑥 = ( 𝑦 − 𝐶 ) ↔ ( 𝑦 − 𝐶 ) = 𝑥 )
53 eqcom ⊢ ( 𝑦 = ( 𝑥 + 𝐶 ) ↔ ( 𝑥 + 𝐶 ) = 𝑦 )
54 51 52 53 3bitr4g ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝑥 = ( 𝑦 − 𝐶 ) ↔ 𝑦 = ( 𝑥 + 𝐶 ) ) )
55 54 reubidva ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) → ( ∃! 𝑥 ∈ ( 𝐴 [,) 𝐵 ) 𝑥 = ( 𝑦 − 𝐶 ) ↔ ∃! 𝑥 ∈ ( 𝐴 [,) 𝐵 ) 𝑦 = ( 𝑥 + 𝐶 ) ) )
56 39 55 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ) → ∃! 𝑥 ∈ ( 𝐴 [,) 𝐵 ) 𝑦 = ( 𝑥 + 𝐶 ) )
57 56 ralrimiva ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ∀ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ∃! 𝑥 ∈ ( 𝐴 [,) 𝐵 ) 𝑦 = ( 𝑥 + 𝐶 ) )
58 1 f1ompt ⊢ ( 𝐹 : ( 𝐴 [,) 𝐵 ) –1-1-onto→ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ↔ ( ∀ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ( 𝑥 + 𝐶 ) ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ∧ ∀ 𝑦 ∈ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) ∃! 𝑥 ∈ ( 𝐴 [,) 𝐵 ) 𝑦 = ( 𝑥 + 𝐶 ) ) )
59 3 57 58 sylanbrc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐹 : ( 𝐴 [,) 𝐵 ) –1-1-onto→ ( ( 𝐴 + 𝐶 ) [,) ( 𝐵 + 𝐶 ) ) )