Theorem iccf1o 10006

Description: Describe a bijection from [ 0 , 1 ] to an arbitrary nontrivial closed interval [ A , B ]. (Contributed by Mario Carneiro, 8-Sep-2015.)

Hypothesis

Ref	Expression
iccf1o.1	|- F = ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) )

Assertion

Ref	Expression
iccf1o	|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( F : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) /\ `' F = ( y e. ( A [,] B ) |-> ( ( y - A ) / ( B - A ) ) ) ) )

Distinct variable groups:   x, y, A   x, B, y

Allowed substitution hints:   F( x, y)

Proof of Theorem iccf1o

Step	Hyp	Ref	Expression
1		iccf1o.1	. 2 |- F = ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) )
2		0re 7959	. . . . . . . . 9 |- 0 e. RR
3		1re 7958	. . . . . . . . 9 |- 1 e. RR
4	2, 3	elicc2i 9941	. . . . . . . 8 |- ( x e. ( 0 [,] 1 ) <-> ( x e. RR /\ 0 <_ x /\ x <_ 1 ) )
5	4	simp1bi 1012	. . . . . . 7 |- ( x e. ( 0 [,] 1 ) -> x e. RR )
6	5	adantl 277	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> x e. RR )
7	6	recnd 7988	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> x e. CC )
8		simpl2 1001	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> B e. RR )
9	8	recnd 7988	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> B e. CC )
10	7, 9	mulcld 7980	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( x x. B ) e. CC )
11		ax-1cn 7906	. . . . . 6 |- 1 e. CC
12		subcl 8158	. . . . . 6 |- ( ( 1 e. CC /\ x e. CC ) -> ( 1 - x ) e. CC )
13	11, 7, 12	sylancr 414	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( 1 - x ) e. CC )
14		simpl1 1000	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> A e. RR )
15	14	recnd 7988	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> A e. CC )
16	13, 15	mulcld 7980	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( 1 - x ) x. A ) e. CC )
17	10, 16	addcomd 8110	. . 3 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) = ( ( ( 1 - x ) x. A ) + ( x x. B ) ) )
18		lincmb01cmp 10005	. . 3 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( ( 1 - x ) x. A ) + ( x x. B ) ) e. ( A [,] B ) )
19	17, 18	eqeltrd 2254	. 2 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) e. ( A [,] B ) )
20		simpr 110	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> y e. ( A [,] B ) )
21		simpl1 1000	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> A e. RR )
22		simpl2 1001	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> B e. RR )
23		elicc2 9940	. . . . . . . . 9 |- ( ( A e. RR /\ B e. RR ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
24	23	3adant3 1017	. . . . . . . 8 |- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
25	24	biimpa 296	. . . . . . 7 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( y e. RR /\ A <_ y /\ y <_ B ) )
26	25	simp1d 1009	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> y e. RR )
27		eqid 2177	. . . . . . 7 |- ( A - A ) = ( A - A )
28		eqid 2177	. . . . . . 7 |- ( B - A ) = ( B - A )
29	27, 28	iccshftl 9998	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR ) /\ ( y e. RR /\ A e. RR ) ) -> ( y e. ( A [,] B ) <-> ( y - A ) e. ( ( A - A ) [,] ( B - A ) ) ) )
30	21, 22, 26, 21, 29	syl22anc 1239	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( y e. ( A [,] B ) <-> ( y - A ) e. ( ( A - A ) [,] ( B - A ) ) ) )
31	20, 30	mpbid 147	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( y - A ) e. ( ( A - A ) [,] ( B - A ) ) )
32	26, 21	resubcld 8340	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( y - A ) e. RR )
33	32	recnd 7988	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( y - A ) e. CC )
34		difrp 9694	. . . . . . . 8 |- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( B - A ) e. RR+ ) )
35	34	biimp3a 1345	. . . . . . 7 |- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( B - A ) e. RR+ )
36	35	adantr 276	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( B - A ) e. RR+ )
37	36	rpcnd 9700	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( B - A ) e. CC )
38		rpap0 9672	. . . . . 6 |- ( ( B - A ) e. RR+ -> ( B - A ) # 0 )
39	36, 38	syl 14	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( B - A ) # 0 )
40	33, 37, 39	divcanap1d 8750	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( ( ( y - A ) / ( B - A ) ) x. ( B - A ) ) = ( y - A ) )
41	37	mul02d 8351	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( 0 x. ( B - A ) ) = 0 )
42	21	recnd 7988	. . . . . . 7 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> A e. CC )
43	42	subidd 8258	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( A - A ) = 0 )
44	41, 43	eqtr4d 2213	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( 0 x. ( B - A ) ) = ( A - A ) )
45	37	mulid2d 7978	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( 1 x. ( B - A ) ) = ( B - A ) )
46	44, 45	oveq12d 5895	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( ( 0 x. ( B - A ) ) [,] ( 1 x. ( B - A ) ) ) = ( ( A - A ) [,] ( B - A ) ) )
47	31, 40, 46	3eltr4d 2261	. . 3 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( ( ( y - A ) / ( B - A ) ) x. ( B - A ) ) e. ( ( 0 x. ( B - A ) ) [,] ( 1 x. ( B - A ) ) ) )
48		0red 7960	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> 0 e. RR )
49		1red 7974	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> 1 e. RR )
50	32, 36	rerpdivcld 9730	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( ( y - A ) / ( B - A ) ) e. RR )
51		eqid 2177	. . . . 5 |- ( 0 x. ( B - A ) ) = ( 0 x. ( B - A ) )
52		eqid 2177	. . . . 5 |- ( 1 x. ( B - A ) ) = ( 1 x. ( B - A ) )
53	51, 52	iccdil 10000	. . . 4 |- ( ( ( 0 e. RR /\ 1 e. RR ) /\ ( ( ( y - A ) / ( B - A ) ) e. RR /\ ( B - A ) e. RR+ ) ) -> ( ( ( y - A ) / ( B - A ) ) e. ( 0 [,] 1 ) <-> ( ( ( y - A ) / ( B - A ) ) x. ( B - A ) ) e. ( ( 0 x. ( B - A ) ) [,] ( 1 x. ( B - A ) ) ) ) )
54	48, 49, 50, 36, 53	syl22anc 1239	. . 3 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( ( ( y - A ) / ( B - A ) ) e. ( 0 [,] 1 ) <-> ( ( ( y - A ) / ( B - A ) ) x. ( B - A ) ) e. ( ( 0 x. ( B - A ) ) [,] ( 1 x. ( B - A ) ) ) ) )
55	47, 54	mpbird 167	. 2 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ y e. ( A [,] B ) ) -> ( ( y - A ) / ( B - A ) ) e. ( 0 [,] 1 ) )
56		eqcom 2179	. . . 4 |- ( x = ( ( y - A ) / ( B - A ) ) <-> ( ( y - A ) / ( B - A ) ) = x )
57	33	adantrl 478	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( y - A ) e. CC )
58	7	adantrr 479	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> x e. CC )
59	37	adantrl 478	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( B - A ) e. CC )
60	39	adantrl 478	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( B - A ) # 0 )
61	57, 58, 59, 60	divmulap3d 8784	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( ( ( y - A ) / ( B - A ) ) = x <-> ( y - A ) = ( x x. ( B - A ) ) ) )
62	56, 61	bitrid 192	. . 3 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( x = ( ( y - A ) / ( B - A ) ) <-> ( y - A ) = ( x x. ( B - A ) ) ) )
63	26	adantrl 478	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> y e. RR )
64	63	recnd 7988	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> y e. CC )
65	42	adantrl 478	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> A e. CC )
66	8, 14	resubcld 8340	. . . . . . . 8 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( B - A ) e. RR )
67	6, 66	remulcld 7990	. . . . . . 7 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( x x. ( B - A ) ) e. RR )
68	67	adantrr 479	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( x x. ( B - A ) ) e. RR )
69	68	recnd 7988	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( x x. ( B - A ) ) e. CC )
70	64, 65, 69	subadd2d 8289	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( ( y - A ) = ( x x. ( B - A ) ) <-> ( ( x x. ( B - A ) ) + A ) = y ) )
71		eqcom 2179	. . . 4 |- ( ( ( x x. ( B - A ) ) + A ) = y <-> y = ( ( x x. ( B - A ) ) + A ) )
72	70, 71	bitrdi 196	. . 3 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( ( y - A ) = ( x x. ( B - A ) ) <-> y = ( ( x x. ( B - A ) ) + A ) ) )
73	7, 15	mulcld 7980	. . . . . . 7 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( x x. A ) e. CC )
74	10, 73, 15	subadd23d 8292	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( ( x x. B ) - ( x x. A ) ) + A ) = ( ( x x. B ) + ( A - ( x x. A ) ) ) )
75	7, 9, 15	subdid 8373	. . . . . . 7 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( x x. ( B - A ) ) = ( ( x x. B ) - ( x x. A ) ) )
76	75	oveq1d 5892	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( x x. ( B - A ) ) + A ) = ( ( ( x x. B ) - ( x x. A ) ) + A ) )
77		1cnd 7975	. . . . . . . . 9 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> 1 e. CC )
78	77, 7, 15	subdird 8374	. . . . . . . 8 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( 1 - x ) x. A ) = ( ( 1 x. A ) - ( x x. A ) ) )
79	15	mulid2d 7978	. . . . . . . . 9 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( 1 x. A ) = A )
80	79	oveq1d 5892	. . . . . . . 8 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( 1 x. A ) - ( x x. A ) ) = ( A - ( x x. A ) ) )
81	78, 80	eqtrd 2210	. . . . . . 7 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( 1 - x ) x. A ) = ( A - ( x x. A ) ) )
82	81	oveq2d 5893	. . . . . 6 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) = ( ( x x. B ) + ( A - ( x x. A ) ) ) )
83	74, 76, 82	3eqtr4d 2220	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ x e. ( 0 [,] 1 ) ) -> ( ( x x. ( B - A ) ) + A ) = ( ( x x. B ) + ( ( 1 - x ) x. A ) ) )
84	83	adantrr 479	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( ( x x. ( B - A ) ) + A ) = ( ( x x. B ) + ( ( 1 - x ) x. A ) ) )
85	84	eqeq2d 2189	. . 3 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( y = ( ( x x. ( B - A ) ) + A ) <-> y = ( ( x x. B ) + ( ( 1 - x ) x. A ) ) ) )
86	62, 72, 85	3bitrd 214	. 2 |- ( ( ( A e. RR /\ B e. RR /\ A < B ) /\ ( x e. ( 0 [,] 1 ) /\ y e. ( A [,] B ) ) ) -> ( x = ( ( y - A ) / ( B - A ) ) <-> y = ( ( x x. B ) + ( ( 1 - x ) x. A ) ) ) )
87	1, 19, 55, 86	f1ocnv2d 6077	1 |- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( F : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) /\ `' F = ( y e. ( A [,] B ) |-> ( ( y - A ) / ( B - A ) ) ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 978   = wceq 1353   e. wcel 2148   class class class wbr 4005   |-> cmpt 4066   `'ccnv 4627   -1-1-onto->wf1o 5217  (class class class)co 5877   CCcc 7811   RRcr 7812   0cc0 7813   1c1 7814   + caddc 7816   x. cmul 7818   < clt 7994   <_ cle 7995   - cmin 8130   # cap 8540   / cdiv 8631   RR+crp 9655   [,]cicc 9893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-cnex 7904  ax-resscn 7905  ax-1cn 7906  ax-1re 7907  ax-icn 7908  ax-addcl 7909  ax-addrcl 7910  ax-mulcl 7911  ax-mulrcl 7912  ax-addcom 7913  ax-mulcom 7914  ax-addass 7915  ax-mulass 7916  ax-distr 7917  ax-i2m1 7918  ax-0lt1 7919  ax-1rid 7920  ax-0id 7921  ax-rnegex 7922  ax-precex 7923  ax-cnre 7924  ax-pre-ltirr 7925  ax-pre-ltwlin 7926  ax-pre-lttrn 7927  ax-pre-apti 7928  ax-pre-ltadd 7929  ax-pre-mulgt0 7930  ax-pre-mulext 7931

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2741  df-sbc 2965  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-po 4298  df-iso 4299  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-riota 5833  df-ov 5880  df-oprab 5881  df-mpo 5882  df-pnf 7996  df-mnf 7997  df-xr 7998  df-ltxr 7999  df-le 8000  df-sub 8132  df-neg 8133  df-reap 8534  df-ap 8541  df-div 8632  df-rp 9656  df-icc 9897

This theorem is referenced by:  iccen  10008