let a, b, c, d be real number ; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st a < b & c < d & p1 in LSeg |[a,c]|,|[a,d]| & p2 in LSeg |[a,c]|,|[a,d]| holds
( LE p1,p2, rectangle a,b,c,d iff p1 `2 <= p2 `2 )
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( a < b & c < d & p1 in LSeg |[a,c]|,|[a,d]| & p2 in LSeg |[a,c]|,|[a,d]| implies ( LE p1,p2, rectangle a,b,c,d iff p1 `2 <= p2 `2 ) )
set K = rectangle a,b,c,d;
assume A1:
( a < b & c < d & p1 in LSeg |[a,c]|,|[a,d]| & p2 in LSeg |[a,c]|,|[a,d]| )
; :: thesis: ( LE p1,p2, rectangle a,b,c,d iff p1 `2 <= p2 `2 )
then A2:
rectangle a,b,c,d is being_simple_closed_curve
by Th60;
A3:
( p1 `1 = a & c <= p1 `2 & p1 `2 <= d )
by A1, Th9;
A4:
( p2 `1 = a & c <= p2 `2 & p2 `2 <= d )
by A1, Th9;
A5:
E-max (rectangle a,b,c,d) = |[b,d]|
by A1, Th56;
A6:
Upper_Arc (rectangle a,b,c,d) = (LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|)
by A1, Th61;
then A7:
LSeg |[a,c]|,|[a,d]| c= Upper_Arc (rectangle a,b,c,d)
by XBOOLE_1:7;
A8:
(Upper_Arc (rectangle a,b,c,d)) /\ (Lower_Arc (rectangle a,b,c,d)) = {(W-min (rectangle a,b,c,d)),(E-max (rectangle a,b,c,d))}
by A2, JORDAN6:def 9;
A9:
now assume
p2 in Lower_Arc (rectangle a,b,c,d)
;
:: thesis: p2 = W-min (rectangle a,b,c,d)then A10:
p2 in (Upper_Arc (rectangle a,b,c,d)) /\ (Lower_Arc (rectangle a,b,c,d))
by A1, A7, XBOOLE_0:def 4;
hence
p2 = W-min (rectangle a,b,c,d)
by A8, A10, TARSKI:def 2;
:: thesis: verum end;
thus
( LE p1,p2, rectangle a,b,c,d implies p1 `2 <= p2 `2 )
:: thesis: ( p1 `2 <= p2 `2 implies LE p1,p2, rectangle a,b,c,d )proof
assume
LE p1,
p2,
rectangle a,
b,
c,
d
;
:: thesis: p1 `2 <= p2 `2
then A11:
( (
p1 in Upper_Arc (rectangle a,b,c,d) &
p2 in Lower_Arc (rectangle a,b,c,d) & not
p2 = W-min (rectangle a,b,c,d) ) or (
p1 in Upper_Arc (rectangle a,b,c,d) &
p2 in Upper_Arc (rectangle a,b,c,d) &
LE p1,
p2,
Upper_Arc (rectangle a,b,c,d),
W-min (rectangle a,b,c,d),
E-max (rectangle a,b,c,d) ) or (
p1 in Lower_Arc (rectangle a,b,c,d) &
p2 in Lower_Arc (rectangle a,b,c,d) & not
p2 = W-min (rectangle a,b,c,d) &
LE p1,
p2,
Lower_Arc (rectangle a,b,c,d),
E-max (rectangle a,b,c,d),
W-min (rectangle a,b,c,d) ) )
by JORDAN6:def 10;
consider f being
Function of
I[01] ,
((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) such that A12:
(
f is
being_homeomorphism &
f . 0 = W-min (rectangle a,b,c,d) &
f . 1
= E-max (rectangle a,b,c,d) &
rng f = Upper_Arc (rectangle a,b,c,d) & ( for
r being
Real st
r in [.0 ,(1 / 2).] holds
f . r = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) ) & ( for
r being
Real st
r in [.(1 / 2),1.] holds
f . r = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) ) & ( for
p being
Point of
(TOP-REAL 2) st
p in LSeg |[a,c]|,
|[a,d]| holds
(
0 <= (((p `2 ) - c) / (d - c)) / 2 &
(((p `2 ) - c) / (d - c)) / 2
<= 1 &
f . ((((p `2 ) - c) / (d - c)) / 2) = p ) ) & ( for
p being
Point of
(TOP-REAL 2) st
p in LSeg |[a,d]|,
|[b,d]| holds
(
0 <= ((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) &
((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) <= 1 &
f . (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2)) = p ) ) )
by A1, Th63;
reconsider s1 =
(((p1 `2 ) - c) / (d - c)) / 2,
s2 =
(((p2 `2 ) - c) / (d - c)) / 2 as
Real ;
A13:
f . s1 = p1
by A1, A12;
A14:
f . s2 = p2
by A1, A12;
A15:
d - c > 0
by A1, XREAL_1:52;
A16:
(
0 <= s1 &
s1 <= 1 )
by A1, A12;
(
0 <= s2 &
s2 <= 1 )
by A1, A12;
then
s1 <= s2
by A9, A11, A12, A13, A14, A16, JORDAN5C:def 3;
then
((((p1 `2 ) - c) / (d - c)) / 2) * 2
<= ((((p2 `2 ) - c) / (d - c)) / 2) * 2
by XREAL_1:66;
then
(((p1 `2 ) - c) / (d - c)) * (d - c) <= (((p2 `2 ) - c) / (d - c)) * (d - c)
by A15, XREAL_1:66;
then
(p1 `2 ) - c <= (((p2 `2 ) - c) / (d - c)) * (d - c)
by A15, XCMPLX_1:88;
then
(p1 `2 ) - c <= (p2 `2 ) - c
by A15, XCMPLX_1:88;
then
((p1 `2 ) - c) + c <= ((p2 `2 ) - c) + c
by XREAL_1:9;
hence
p1 `2 <= p2 `2
;
:: thesis: verum
end;
thus
( p1 `2 <= p2 `2 implies LE p1,p2, rectangle a,b,c,d )
:: thesis: verumproof
assume A17:
p1 `2 <= p2 `2
;
:: thesis: LE p1,p2, rectangle a,b,c,d
for
g being
Function of
I[01] ,
((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) for
s1,
s2 being
Real st
g is
being_homeomorphism &
g . 0 = W-min (rectangle a,b,c,d) &
g . 1
= E-max (rectangle a,b,c,d) &
g . s1 = p1 &
0 <= s1 &
s1 <= 1 &
g . s2 = p2 &
0 <= s2 &
s2 <= 1 holds
s1 <= s2
proof
let g be
Function of
I[01] ,
((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d)));
:: thesis: for s1, s2 being Real st g is being_homeomorphism & g . 0 = W-min (rectangle a,b,c,d) & g . 1 = E-max (rectangle a,b,c,d) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 holds
s1 <= s2let s1,
s2 be
Real;
:: thesis: ( g is being_homeomorphism & g . 0 = W-min (rectangle a,b,c,d) & g . 1 = E-max (rectangle a,b,c,d) & g . s1 = p1 & 0 <= s1 & s1 <= 1 & g . s2 = p2 & 0 <= s2 & s2 <= 1 implies s1 <= s2 )
assume A18:
(
g is
being_homeomorphism &
g . 0 = W-min (rectangle a,b,c,d) &
g . 1
= E-max (rectangle a,b,c,d) &
g . s1 = p1 &
0 <= s1 &
s1 <= 1 &
g . s2 = p2 &
0 <= s2 &
s2 <= 1 )
;
:: thesis: s1 <= s2
A19:
dom g = the
carrier of
I[01]
by FUNCT_2:def 1;
A20:
g is
one-to-one
by A18, TOPS_2:def 5;
A21:
the
carrier of
((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) = Upper_Arc (rectangle a,b,c,d)
by PRE_TOPC:29;
then reconsider g1 =
g as
Function of
I[01] ,
(TOP-REAL 2) by FUNCT_2:9;
g is
continuous
by A18, TOPS_2:def 5;
then A22:
g1 is
continuous
by PRE_TOPC:56;
reconsider h1 =
proj1 as
Function of
(TOP-REAL 2),
R^1 by TOPMETR:24;
reconsider h2 =
proj2 as
Function of
(TOP-REAL 2),
R^1 by TOPMETR:24;
reconsider hh1 =
h1 as
Function of
TopStruct(# the
carrier of
(TOP-REAL 2),the
topology of
(TOP-REAL 2) #),
R^1 ;
reconsider hh2 =
h2 as
Function of
TopStruct(# the
carrier of
(TOP-REAL 2),the
topology of
(TOP-REAL 2) #),
R^1 ;
A23:
TopStruct(# the
carrier of
(TOP-REAL 2),the
topology of
(TOP-REAL 2) #) =
TopStruct(# the
carrier of
(TOP-REAL 2),the
topology of
(TOP-REAL 2) #)
| ([#] TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #))
by TSEP_1:3
.=
TopStruct(# the
carrier of
((TOP-REAL 2) | ([#] (TOP-REAL 2))),the
topology of
((TOP-REAL 2) | ([#] (TOP-REAL 2))) #)
by PRE_TOPC:66
.=
(TOP-REAL 2) | ([#] (TOP-REAL 2))
;
then B24:
( ( for
p being
Point of
((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds
hh1 . p = proj1 . p ) implies
hh1 is
continuous )
by JGRAPH_2:39;
A24:
( ( for
p being
Point of
((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds
hh1 . p = proj1 . p ) implies
h1 is
continuous )
by B24, PRE_TOPC:62;
BB:
( ( for
p being
Point of
((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds
hh2 . p = proj2 . p ) implies
hh2 is
continuous )
by A23, JGRAPH_2:40;
( ( for
p being
Point of
((TOP-REAL 2) | ([#] (TOP-REAL 2))) holds
hh2 . p = proj2 . p ) implies
h2 is
continuous )
by BB, PRE_TOPC:62;
then consider h being
Function of
(TOP-REAL 2),
R^1 such that A25:
( ( for
p being
Point of
(TOP-REAL 2) for
r1,
r2 being
real number st
hh1 . p = r1 &
hh2 . p = r2 holds
h . p = r1 + r2 ) &
h is
continuous )
by A24, JGRAPH_2:29;
reconsider k =
h * g1 as
Function of
I[01] ,
R^1 ;
A26:
k is
continuous Function of
I[01] ,
R^1
by A22, A25;
A27:
W-min (rectangle a,b,c,d) = |[a,c]|
by A1, Th56;
now assume A28:
s1 > s2
;
:: thesis: contradictionA29:
dom g = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
0 in [.0 ,1.]
by XXREAL_1:1;
then A30:
k . 0 =
h . (W-min (rectangle a,b,c,d))
by A18, A29, FUNCT_1:23
.=
(h1 . (W-min (rectangle a,b,c,d))) + (h2 . (W-min (rectangle a,b,c,d)))
by A25
.=
((W-min (rectangle a,b,c,d)) `1 ) + (proj2 . (W-min (rectangle a,b,c,d)))
by PSCOMP_1:def 28
.=
((W-min (rectangle a,b,c,d)) `1 ) + ((W-min (rectangle a,b,c,d)) `2 )
by PSCOMP_1:def 29
.=
a + ((W-min (rectangle a,b,c,d)) `2 )
by A27, EUCLID:56
.=
a + c
by A27, EUCLID:56
;
s1 in [.0 ,1.]
by A18, XXREAL_1:1;
then A31:
k . s1 =
h . p1
by A18, A29, FUNCT_1:23
.=
(h1 . p1) + (h2 . p1)
by A25
.=
(p1 `1 ) + (proj2 . p1)
by PSCOMP_1:def 28
.=
a + (p1 `2 )
by A3, PSCOMP_1:def 29
;
A32:
s2 in [.0 ,1.]
by A18, XXREAL_1:1;
then k . s2 =
h . p2
by A18, A29, FUNCT_1:23
.=
(h1 . p2) + (h2 . p2)
by A25
.=
(p2 `1 ) + (proj2 . p2)
by PSCOMP_1:def 28
.=
a + (p2 `2 )
by A4, PSCOMP_1:def 29
;
then A33:
(
k . 0 <= k . s1 &
k . s1 <= k . s2 )
by A3, A17, A30, A31, XREAL_1:9;
A34:
0 in [.0 ,1.]
by XXREAL_1:1;
then A35:
[.0 ,s2.] c= [.0 ,1.]
by A32, XXREAL_2:def 12;
reconsider B =
[.0 ,s2.] as
Subset of
I[01] by A32, A34, BORSUK_1:83, XXREAL_2:def 12;
A36:
B is
connected
by A18, A32, A34, BORSUK_1:83, BORSUK_4:49;
A37:
0 in B
by A18, XXREAL_1:1;
A38:
s2 in B
by A18, XXREAL_1:1;
A39:
k . 0 is
Real
by XREAL_0:def 1;
A40:
k . s2 is
Real
by XREAL_0:def 1;
k . s1 is
Real
by XREAL_0:def 1;
then consider xc being
Point of
I[01] such that A41:
(
xc in B &
k . xc = k . s1 )
by A26, A33, A36, A37, A38, A39, A40, TOPREAL5:11;
xc in [.0 ,1.]
by BORSUK_1:83;
then reconsider rxc =
xc as
Real ;
A42:
k is
one-to-one
proof
for
x1,
x2 being
set st
x1 in dom k &
x2 in dom k &
k . x1 = k . x2 holds
x1 = x2
proof
let x1,
x2 be
set ;
:: thesis: ( x1 in dom k & x2 in dom k & k . x1 = k . x2 implies x1 = x2 )
assume A43:
(
x1 in dom k &
x2 in dom k &
k . x1 = k . x2 )
;
:: thesis: x1 = x2
then reconsider r1 =
x1 as
Point of
I[01] ;
reconsider r2 =
x2 as
Point of
I[01] by A43;
A44:
k . x1 =
h . (g1 . x1)
by A43, FUNCT_1:22
.=
(h1 . (g1 . r1)) + (h2 . (g1 . r1))
by A25
.=
((g1 . r1) `1 ) + (proj2 . (g1 . r1))
by PSCOMP_1:def 28
.=
((g1 . r1) `1 ) + ((g1 . r1) `2 )
by PSCOMP_1:def 29
;
A45:
k . x2 =
h . (g1 . x2)
by A43, FUNCT_1:22
.=
(h1 . (g1 . r2)) + (h2 . (g1 . r2))
by A25
.=
((g1 . r2) `1 ) + (proj2 . (g1 . r2))
by PSCOMP_1:def 28
.=
((g1 . r2) `1 ) + ((g1 . r2) `2 )
by PSCOMP_1:def 29
;
A46:
g . r1 in Upper_Arc (rectangle a,b,c,d)
by A21;
A47:
g . r2 in Upper_Arc (rectangle a,b,c,d)
by A21;
reconsider gr1 =
g . r1 as
Point of
(TOP-REAL 2) by A46;
reconsider gr2 =
g . r2 as
Point of
(TOP-REAL 2) by A47;
now per cases
( ( g . r1 in LSeg |[a,c]|,|[a,d]| & g . r2 in LSeg |[a,c]|,|[a,d]| ) or ( g . r1 in LSeg |[a,c]|,|[a,d]| & g . r2 in LSeg |[a,d]|,|[b,d]| ) or ( g . r1 in LSeg |[a,d]|,|[b,d]| & g . r2 in LSeg |[a,c]|,|[a,d]| ) or ( g . r1 in LSeg |[a,d]|,|[b,d]| & g . r2 in LSeg |[a,d]|,|[b,d]| ) )
by A6, A21, XBOOLE_0:def 3;
case A48:
(
g . r1 in LSeg |[a,c]|,
|[a,d]| &
g . r2 in LSeg |[a,c]|,
|[a,d]| )
;
:: thesis: x1 = x2then A49:
(
gr1 `1 = a &
c <= gr1 `2 &
gr1 `2 <= d )
by A1, Th9;
(
gr2 `1 = a &
c <= gr2 `2 &
gr2 `2 <= d )
by A1, A48, Th9;
then
|[(gr1 `1 ),(gr1 `2 )]| = g . r2
by A43, A44, A45, A49, EUCLID:57;
then
g . r1 = g . r2
by EUCLID:57;
hence
x1 = x2
by A19, A20, FUNCT_1:def 8;
:: thesis: verum end; case A50:
(
g . r1 in LSeg |[a,c]|,
|[a,d]| &
g . r2 in LSeg |[a,d]|,
|[b,d]| )
;
:: thesis: x1 = x2then A51:
(
gr1 `1 = a &
c <= gr1 `2 &
gr1 `2 <= d )
by A1, Th9;
A52:
(
gr2 `2 = d &
a <= gr2 `1 &
gr2 `1 <= b )
by A1, A50, Th11;
A53:
a + (gr1 `2 ) = (gr2 `1 ) + d
by A1, A43, A44, A45, A50, A51, Th11;
then
|[(gr1 `1 ),(gr1 `2 )]| = g . r2
by A51, A52, A54, EUCLID:57;
then
g . r1 = g . r2
by EUCLID:57;
hence
x1 = x2
by A19, A20, FUNCT_1:def 8;
:: thesis: verum end; case A55:
(
g . r1 in LSeg |[a,d]|,
|[b,d]| &
g . r2 in LSeg |[a,c]|,
|[a,d]| )
;
:: thesis: x1 = x2then A56:
(
gr2 `1 = a &
c <= gr2 `2 &
gr2 `2 <= d )
by A1, Th9;
A57:
(
gr1 `2 = d &
a <= gr1 `1 &
gr1 `1 <= b )
by A1, A55, Th11;
A58:
a + (gr2 `2 ) = (gr1 `1 ) + d
by A1, A43, A44, A45, A55, A56, Th11;
then
|[(gr2 `1 ),(gr2 `2 )]| = g . r1
by A56, A57, A59, EUCLID:57;
then
g . r1 = g . r2
by EUCLID:57;
hence
x1 = x2
by A19, A20, FUNCT_1:def 8;
:: thesis: verum end; case A60:
(
g . r1 in LSeg |[a,d]|,
|[b,d]| &
g . r2 in LSeg |[a,d]|,
|[b,d]| )
;
:: thesis: x1 = x2then A61:
(
gr1 `2 = d &
a <= gr1 `1 &
gr1 `1 <= b )
by A1, Th11;
(
gr2 `2 = d &
a <= gr2 `1 &
gr2 `1 <= b )
by A1, A60, Th11;
then
|[(gr1 `1 ),(gr1 `2 )]| = g . r2
by A43, A44, A45, A61, EUCLID:57;
then
g . r1 = g . r2
by EUCLID:57;
hence
x1 = x2
by A19, A20, FUNCT_1:def 8;
:: thesis: verum end;
hence
x1 = x2
;
:: thesis: verum
end;
hence
k is
one-to-one
by FUNCT_1:def 8;
:: thesis: verum
end; A62:
dom k = [.0 ,1.]
by BORSUK_1:83, FUNCT_2:def 1;
then
s1 in dom k
by A18, XXREAL_1:1;
then
rxc = s1
by A35, A41, A42, A62, FUNCT_1:def 8;
hence
contradiction
by A28, A41, XXREAL_1:1;
:: thesis: verum end;
hence
s1 <= s2
;
:: thesis: verum
end;
then
(
p1 in Upper_Arc (rectangle a,b,c,d) &
p2 in Upper_Arc (rectangle a,b,c,d) &
LE p1,
p2,
Upper_Arc (rectangle a,b,c,d),
W-min (rectangle a,b,c,d),
E-max (rectangle a,b,c,d) )
by A1, A7, JORDAN5C:def 3;
hence
LE p1,
p2,
rectangle a,
b,
c,
d
by JORDAN6:def 10;
:: thesis: verum
end;