let p, q be Point of (TOP-REAL 2); ( p `2 <= q `2 implies proj2 .: (LSeg (p,q)) = [.(p `2),(q `2).] )
assume A1:
p `2 <= q `2
; proj2 .: (LSeg (p,q)) = [.(p `2),(q `2).]
for y being object holds
( y in [.(p `2),(q `2).] iff ex x being object st
( x in dom proj2 & x in LSeg (p,q) & y = proj2 . x ) )
proof
let y be
object ;
( y in [.(p `2),(q `2).] iff ex x being object st
( x in dom proj2 & x in LSeg (p,q) & y = proj2 . x ) )
hereby ( ex x being object st
( x in dom proj2 & x in LSeg (p,q) & y = proj2 . x ) implies y in [.(p `2),(q `2).] )
assume A2:
y in [.(p `2),(q `2).]
;
ex x being object st
( x in dom proj2 & x in LSeg (p,q) & y = proj2 . x )then reconsider r =
y as
Real ;
consider t being
Real such that A3:
0 <= t
and A4:
t <= 1
and A5:
r = (t * (p `2)) + ((1 - t) * (q `2))
by A1, A2, Th51;
set o =
(t * p) + ((1 - t) * q);
reconsider x =
(t * p) + ((1 - t) * q) as
object ;
take x =
x;
( x in dom proj2 & x in LSeg (p,q) & y = proj2 . x )
(t * p) + ((1 - t) * q) in the
carrier of
(TOP-REAL 2)
;
hence
x in dom proj2
by FUNCT_2:def 1;
( x in LSeg (p,q) & y = proj2 . x )
(t * p) + ((1 - t) * q) in LSeg (
q,
p)
by A3, A4;
hence
x in LSeg (
p,
q)
;
y = proj2 . xthus y =
((t * p) `2) + ((1 - t) * (q `2))
by A5, TOPREAL3:4
.=
((t * p) `2) + (((1 - t) * q) `2)
by TOPREAL3:4
.=
((t * p) + ((1 - t) * q)) `2
by TOPREAL3:2
.=
proj2 . x
by PSCOMP_1:def 6
;
verum
end;
given x being
object such that
x in dom proj2
and A6:
x in LSeg (
p,
q)
and A7:
y = proj2 . x
;
y in [.(p `2),(q `2).]
reconsider s =
x as
Point of
(TOP-REAL 2) by A6;
x in LSeg (
q,
p)
by A6;
then consider r being
Real such that A8:
s = ((1 - r) * q) + (r * p)
and A9:
0 <= r
and A10:
r <= 1
;
y =
s `2
by A7, PSCOMP_1:def 6
.=
(((1 - r) * q) `2) + ((r * p) `2)
by A8, TOPREAL3:2
.=
((1 - r) * (q `2)) + ((r * p) `2)
by TOPREAL3:4
.=
((1 - r) * (q `2)) + (r * (p `2))
by TOPREAL3:4
;
hence
y in [.(p `2),(q `2).]
by A1, A9, A10, Th51;
verum
end;
hence
proj2 .: (LSeg (p,q)) = [.(p `2),(q `2).]
by FUNCT_1:def 6; verum