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