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 \in [0, 1] ⟼ x B + (1 - x) A)$
	Assertion	iccf1o	$⊢ (A \in ℝ \land B \in ℝ \land A < B) \to (F : [0, 1] \underset{1-1 onto}{⟶} [A, B] \land F^{-1} = (y \in [A, B] ⟼ \frac{y - A}{B - A}))$

Proof

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

Metamath Proof Explorer

Theorem iccf1o

Proof