set pq = {p,q};
per cases
( p = q or p <> q )
;
suppose A2:
p <> q
;
halfline (p,q) is closed A3:
rng <*p,q*> = {p,q}
by FINSEQ_2:127;
<*p,q*> is
one-to-one
by A2, FINSEQ_3:94;
then reconsider E =
<*p,q*> as
Enumeration of
{p,q} by A3, Def1;
set Apq =
Affin {p,q};
set TRn =
TOP-REAL n;
set TR1 =
TOP-REAL 1;
set L =
].-infty,1.];
A4:
E . 1
= p
;
reconsider L =
].-infty,1.] as
Subset of
R^1 by TOPMETR:17;
consider h being
Function of
(TOP-REAL 1),
R^1 such that A5:
for
p being
Point of
(TOP-REAL 1) holds
h . p = p /. 1
by JORDAN2B:1;
set B =
{ w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } ;
{ w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } c= [#] ((TOP-REAL n) | (Affin {p,q}))
then reconsider B =
{ w where w is Element of ((TOP-REAL n) | (Affin {p,q})) : (w |-- E) | 1 in h " L } as
Subset of
((TOP-REAL n) | (Affin {p,q})) ;
A6:
[#] ((TOP-REAL n) | (Affin {p,q})) = Affin {p,q}
by PRE_TOPC:def 5;
A7:
card {p,q} = 2
by A2, CARD_2:57;
A8:
h is
being_homeomorphism
by A5, JORDAN2B:28;
then A9:
dom h = [#] (TOP-REAL 1)
by TOPGRP_1:24;
A10:
halfline (
p,
q)
c= B
proof
Carrier (q |-- {q}) c= {q}
by RLVECT_2:def 6;
then
not
p in Carrier (q |-- {q})
by A2, TARSKI:def 1;
then A11:
(q |-- {q}) . p = 0
by RLVECT_2:19;
{q} is
Affine
by RUSUB_4:23;
then A12:
Affin {q} = {q}
by RLAFFIN1:50;
let x be
object ;
TARSKI:def 3 ( not x in halfline (p,q) or x in B )
set W =
x |-- {p,q};
set wE =
x |-- E;
A13:
p in {p,q}
by TARSKI:def 2;
assume
x in halfline (
p,
q)
;
x in B
then consider a being
Real such that A14:
x = ((1 - a) * p) + (a * q)
and A15:
0 <= a
by TOPREAL9:26;
reconsider a =
a as
Real ;
(
q in {q} &
{q} c= {p,q} )
by TARSKI:def 1, ZFMISC_1:36;
then
0 = (q |-- {p,q}) . p
by A11, A12, RLAFFIN1:77;
then A16:
(a * (q |-- {p,q})) . p =
a * 0
by RLVECT_2:def 11
.=
0
;
{p,q} c= conv {p,q}
by CONVEX1:41;
then A17:
(p |-- {p,q}) . p = 1
by A13, RLAFFIN1:72;
A18:
(
q in {p,q} &
{p,q} c= Affin {p,q} )
by RLAFFIN1:49, TARSKI:def 2;
then
x |-- {p,q} = ((1 - a) * (p |-- {p,q})) + (a * (q |-- {p,q}))
by A14, A13, RLAFFIN1:70;
then (x |-- {p,q}) . p =
(((1 - a) * (p |-- {p,q})) . p) + ((a * (q |-- {p,q})) . p)
by RLVECT_2:def 10
.=
((1 - a) * ((p |-- {p,q}) . p)) + 0
by A16, RLVECT_2:def 11
.=
1
- a
by A17
;
then
(x |-- {p,q}) . p <= 1
- 0
by A15, XREAL_1:10;
then A19:
(x |-- {p,q}) . p in L
by XXREAL_1:234;
(1 - a) + a = 1
;
then reconsider w =
x as
Element of
((TOP-REAL n) | (Affin {p,q})) by A6, A14, A13, A18, RLAFFIN1:78;
len (x |-- E) = 2
by A7, Th16;
then A20:
len ((x |-- E) | 1) = 1
by FINSEQ_1:59;
then reconsider wE1 =
(x |-- E) | 1 as
Point of
(TOP-REAL 1) by TOPREAL3:46;
A21:
1
in dom wE1
by A20, FINSEQ_3:25;
then A22:
(
wE1 /. 1
= wE1 . 1 &
wE1 . 1
= (x |-- E) . 1 )
by FUNCT_1:47, PARTFUN1:def 6;
A23:
1
in dom (x |-- E)
by A21, RELAT_1:57;
h . wE1 = wE1 /. 1
by A5;
then
h . wE1 in L
by A4, A19, A22, A23, FUNCT_1:12;
then
wE1 in h " L
by A9, FUNCT_1:def 7;
then
w in B
;
hence
x in B
;
verum
end;
L is
closed
by BORSUK_5:41;
then
h " L is
closed
by A8, TOPGRP_1:24;
then A24:
B is
closed
by A7, Th28;
B c= halfline (
p,
q)
proof
let x be
object ;
TARSKI:def 3 ( not x in B or x in halfline (p,q) )
assume
x in B
;
x in halfline (p,q)
then consider w being
Element of
((TOP-REAL n) | (Affin {p,q})) such that A25:
x = w
and A26:
(w |-- E) | 1
in h " L
;
set W =
w |-- {p,q};
set wE =
w |-- E;
reconsider wE1 =
(w |-- E) | 1 as
Point of
(TOP-REAL 1) by A26;
A27:
h . wE1 = wE1 /. 1
by A5;
len wE1 = 1
by CARD_1:def 7;
then A28:
1
in dom wE1
by FINSEQ_3:25;
then A29:
(
wE1 /. 1
= wE1 . 1 &
wE1 . 1
= (w |-- E) . 1 )
by FUNCT_1:47, PARTFUN1:def 6;
A30:
1
in dom (w |-- E)
by A28, RELAT_1:57;
h . ((w |-- E) | 1) in L
by A26, FUNCT_1:def 7;
then
(w |-- {p,q}) . p in L
by A4, A27, A29, A30, FUNCT_1:12;
then
(w |-- {p,q}) . p <= 1
by XXREAL_1:234;
then A31:
((w |-- {p,q}) . p) - ((w |-- {p,q}) . p) <= 1
- ((w |-- {p,q}) . p)
by XREAL_1:9;
A32:
sum (w |-- {p,q}) = 1
by A6, RLAFFIN1:def 7;
Carrier (w |-- {p,q}) c= {p,q}
by RLVECT_2:def 6;
then A33:
sum (w |-- {p,q}) = ((w |-- {p,q}) . p) + ((w |-- {p,q}) . q)
by A2, RLAFFIN1:33;
Sum (w |-- {p,q}) = w
by A6, RLAFFIN1:def 7;
then
w = ((1 - ((w |-- {p,q}) . q)) * p) + (((w |-- {p,q}) . q) * q)
by A2, A33, A32, RLVECT_2:33;
hence
x in halfline (
p,
q)
by A25, A33, A32, A31, TOPREAL9:26;
verum
end; then
halfline (
p,
q)
= B
by A10;
hence
halfline (
p,
q) is
closed
by A6, A24, TSEP_1:8;
verum end;