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 \in [A, B) ⟼ x + C)$
	Assertion	icoshftf1o	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to F : [A, B) \underset{1-1 onto}{⟶} [A + C, B + C)$

Proof

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

Metamath Proof Explorer

Theorem icoshftf1o

Proof