Step |
Hyp |
Ref |
Expression |
1 |
|
icchmeo.j |
|- J = ( TopOpen ` CCfld ) |
2 |
|
icchmeo.f |
|- F = ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) ) |
3 |
|
iitopon |
|- II e. ( TopOn ` ( 0 [,] 1 ) ) |
4 |
3
|
a1i |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> II e. ( TopOn ` ( 0 [,] 1 ) ) ) |
5 |
1
|
dfii3 |
|- II = ( J |`t ( 0 [,] 1 ) ) |
6 |
5
|
oveq2i |
|- ( II Cn II ) = ( II Cn ( J |`t ( 0 [,] 1 ) ) ) |
7 |
1
|
cnfldtop |
|- J e. Top |
8 |
|
cnrest2r |
|- ( J e. Top -> ( II Cn ( J |`t ( 0 [,] 1 ) ) ) C_ ( II Cn J ) ) |
9 |
7 8
|
ax-mp |
|- ( II Cn ( J |`t ( 0 [,] 1 ) ) ) C_ ( II Cn J ) |
10 |
6 9
|
eqsstri |
|- ( II Cn II ) C_ ( II Cn J ) |
11 |
4
|
cnmptid |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> x ) e. ( II Cn II ) ) |
12 |
10 11
|
sselid |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> x ) e. ( II Cn J ) ) |
13 |
1
|
cnfldtopon |
|- J e. ( TopOn ` CC ) |
14 |
13
|
a1i |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> J e. ( TopOn ` CC ) ) |
15 |
|
simp2 |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> B e. RR ) |
16 |
15
|
recnd |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> B e. CC ) |
17 |
4 14 16
|
cnmptc |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> B ) e. ( II Cn J ) ) |
18 |
1
|
mulcn |
|- x. e. ( ( J tX J ) Cn J ) |
19 |
18
|
a1i |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> x. e. ( ( J tX J ) Cn J ) ) |
20 |
4 12 17 19
|
cnmpt12f |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> ( x x. B ) ) e. ( II Cn J ) ) |
21 |
|
1cnd |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> 1 e. CC ) |
22 |
4 14 21
|
cnmptc |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> 1 ) e. ( II Cn J ) ) |
23 |
1
|
subcn |
|- - e. ( ( J tX J ) Cn J ) |
24 |
23
|
a1i |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> - e. ( ( J tX J ) Cn J ) ) |
25 |
4 22 12 24
|
cnmpt12f |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> ( 1 - x ) ) e. ( II Cn J ) ) |
26 |
|
simp1 |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> A e. RR ) |
27 |
26
|
recnd |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> A e. CC ) |
28 |
4 14 27
|
cnmptc |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> A ) e. ( II Cn J ) ) |
29 |
4 25 28 19
|
cnmpt12f |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> ( ( 1 - x ) x. A ) ) e. ( II Cn J ) ) |
30 |
1
|
addcn |
|- + e. ( ( J tX J ) Cn J ) |
31 |
30
|
a1i |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> + e. ( ( J tX J ) Cn J ) ) |
32 |
4 20 29 31
|
cnmpt12f |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. ( 0 [,] 1 ) |-> ( ( x x. B ) + ( ( 1 - x ) x. A ) ) ) e. ( II Cn J ) ) |
33 |
2 32
|
eqeltrid |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> F e. ( II Cn J ) ) |
34 |
2
|
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 ) ) ) ) ) |
35 |
34
|
simpld |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> F : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) ) |
36 |
|
f1of |
|- ( F : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) -> F : ( 0 [,] 1 ) --> ( A [,] B ) ) |
37 |
|
frn |
|- ( F : ( 0 [,] 1 ) --> ( A [,] B ) -> ran F C_ ( A [,] B ) ) |
38 |
35 36 37
|
3syl |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ran F C_ ( A [,] B ) ) |
39 |
|
iccssre |
|- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR ) |
40 |
39
|
3adant3 |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( A [,] B ) C_ RR ) |
41 |
|
ax-resscn |
|- RR C_ CC |
42 |
40 41
|
sstrdi |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( A [,] B ) C_ CC ) |
43 |
|
cnrest2 |
|- ( ( J e. ( TopOn ` CC ) /\ ran F C_ ( A [,] B ) /\ ( A [,] B ) C_ CC ) -> ( F e. ( II Cn J ) <-> F e. ( II Cn ( J |`t ( A [,] B ) ) ) ) ) |
44 |
13 38 42 43
|
mp3an2i |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( F e. ( II Cn J ) <-> F e. ( II Cn ( J |`t ( A [,] B ) ) ) ) ) |
45 |
33 44
|
mpbid |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> F e. ( II Cn ( J |`t ( A [,] B ) ) ) ) |
46 |
34
|
simprd |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> `' F = ( y e. ( A [,] B ) |-> ( ( y - A ) / ( B - A ) ) ) ) |
47 |
|
resttopon |
|- ( ( J e. ( TopOn ` CC ) /\ ( A [,] B ) C_ CC ) -> ( J |`t ( A [,] B ) ) e. ( TopOn ` ( A [,] B ) ) ) |
48 |
13 42 47
|
sylancr |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( J |`t ( A [,] B ) ) e. ( TopOn ` ( A [,] B ) ) ) |
49 |
|
cnrest2r |
|- ( J e. Top -> ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( A [,] B ) ) ) C_ ( ( J |`t ( A [,] B ) ) Cn J ) ) |
50 |
7 49
|
ax-mp |
|- ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( A [,] B ) ) ) C_ ( ( J |`t ( A [,] B ) ) Cn J ) |
51 |
48
|
cnmptid |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) |-> y ) e. ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( A [,] B ) ) ) ) |
52 |
50 51
|
sselid |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) |-> y ) e. ( ( J |`t ( A [,] B ) ) Cn J ) ) |
53 |
48 14 27
|
cnmptc |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) |-> A ) e. ( ( J |`t ( A [,] B ) ) Cn J ) ) |
54 |
48 52 53 24
|
cnmpt12f |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) |-> ( y - A ) ) e. ( ( J |`t ( A [,] B ) ) Cn J ) ) |
55 |
|
difrp |
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( B - A ) e. RR+ ) ) |
56 |
55
|
biimp3a |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( B - A ) e. RR+ ) |
57 |
56
|
rpcnd |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( B - A ) e. CC ) |
58 |
56
|
rpne0d |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( B - A ) =/= 0 ) |
59 |
1
|
divccn |
|- ( ( ( B - A ) e. CC /\ ( B - A ) =/= 0 ) -> ( x e. CC |-> ( x / ( B - A ) ) ) e. ( J Cn J ) ) |
60 |
57 58 59
|
syl2anc |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( x e. CC |-> ( x / ( B - A ) ) ) e. ( J Cn J ) ) |
61 |
|
oveq1 |
|- ( x = ( y - A ) -> ( x / ( B - A ) ) = ( ( y - A ) / ( B - A ) ) ) |
62 |
48 54 14 60 61
|
cnmpt11 |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( y e. ( A [,] B ) |-> ( ( y - A ) / ( B - A ) ) ) e. ( ( J |`t ( A [,] B ) ) Cn J ) ) |
63 |
46 62
|
eqeltrd |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> `' F e. ( ( J |`t ( A [,] B ) ) Cn J ) ) |
64 |
|
dfdm4 |
|- dom F = ran `' F |
65 |
64
|
eqimss2i |
|- ran `' F C_ dom F |
66 |
|
f1odm |
|- ( F : ( 0 [,] 1 ) -1-1-onto-> ( A [,] B ) -> dom F = ( 0 [,] 1 ) ) |
67 |
35 66
|
syl |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> dom F = ( 0 [,] 1 ) ) |
68 |
65 67
|
sseqtrid |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ran `' F C_ ( 0 [,] 1 ) ) |
69 |
|
unitssre |
|- ( 0 [,] 1 ) C_ RR |
70 |
69
|
a1i |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( 0 [,] 1 ) C_ RR ) |
71 |
70 41
|
sstrdi |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( 0 [,] 1 ) C_ CC ) |
72 |
|
cnrest2 |
|- ( ( J e. ( TopOn ` CC ) /\ ran `' F C_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) C_ CC ) -> ( `' F e. ( ( J |`t ( A [,] B ) ) Cn J ) <-> `' F e. ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( 0 [,] 1 ) ) ) ) ) |
73 |
13 68 71 72
|
mp3an2i |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> ( `' F e. ( ( J |`t ( A [,] B ) ) Cn J ) <-> `' F e. ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( 0 [,] 1 ) ) ) ) ) |
74 |
63 73
|
mpbid |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> `' F e. ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( 0 [,] 1 ) ) ) ) |
75 |
5
|
oveq2i |
|- ( ( J |`t ( A [,] B ) ) Cn II ) = ( ( J |`t ( A [,] B ) ) Cn ( J |`t ( 0 [,] 1 ) ) ) |
76 |
74 75
|
eleqtrrdi |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> `' F e. ( ( J |`t ( A [,] B ) ) Cn II ) ) |
77 |
|
ishmeo |
|- ( F e. ( II Homeo ( J |`t ( A [,] B ) ) ) <-> ( F e. ( II Cn ( J |`t ( A [,] B ) ) ) /\ `' F e. ( ( J |`t ( A [,] B ) ) Cn II ) ) ) |
78 |
45 76 77
|
sylanbrc |
|- ( ( A e. RR /\ B e. RR /\ A < B ) -> F e. ( II Homeo ( J |`t ( A [,] B ) ) ) ) |