let V be RealLinearSpace; :: thesis: for p, v, w, u being VECTOR of V st p <> v & v,p // p,w holds
ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )
let p, v, w, u be VECTOR of V; :: thesis: ( p <> v & v,p // p,w implies ex y being VECTOR of V st
( u,p // p,y & u,v // w,y ) )
assume that
A1:
p <> v
and
A2:
v,p // p,w
; :: thesis: ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )
A3:
now assume A4:
p = w
;
:: thesis: ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )take y =
p;
:: thesis: ( u,p // p,y & u,v // w,y )thus
(
u,
p // p,
y &
u,
v // w,
y )
by A4, Def1;
:: thesis: verum end;
now assume
p <> w
;
:: thesis: ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )then consider a,
b being
Real such that A5:
(
a * (p - v) = b * (w - p) &
0 < a &
0 < b )
by A1, A2, Th16;
set y =
(((b " ) * a) * (p - u)) + p;
A6: 1
* (((((b " ) * a) * (p - u)) + p) - p) =
((((b " ) * a) * (p - u)) + p) - p
by RLVECT_1:def 9
.=
((b " ) * a) * (p - u)
by RLSUB_2:78
;
0 < b "
by A5, XREAL_1:124;
then
(
0 < (b " ) * a &
0 < 1 )
by A5, XREAL_1:131;
then A7:
u,
p // p,
(((b " ) * a) * (p - u)) + p
by A6, Def1;
A8:
((((b " ) * a) * (p - u)) + p) - p =
((b " ) * a) * (p - u)
by RLSUB_2:78
.=
(b " ) * (a * (p - u))
by RLVECT_1:def 9
;
A9:
v - u =
(p - u) + (v - p)
by Th4
.=
(p - u) - (p - v)
by RLVECT_1:47
;
A10:
((((b " ) * a) * (p - u)) + p) - w =
(((((b " ) * a) * (p - u)) + p) - p) + (p - w)
by Th4
.=
(((((b " ) * a) * (p - u)) + p) - p) - (w - p)
by RLVECT_1:47
;
a * (v - u) =
(a * (p - u)) - (a * (p - v))
by A9, RLVECT_1:48
.=
(b * (((((b " ) * a) * (p - u)) + p) - p)) - (b * (w - p))
by A5, A8, Th13
.=
b * (((((b " ) * a) * (p - u)) + p) - w)
by A10, RLVECT_1:48
;
then
u,
v // w,
(((b " ) * a) * (p - u)) + p
by A5, Def1;
hence
ex
y being
VECTOR of
V st
(
u,
p // p,
y &
u,
v // w,
y )
by A7;
:: thesis: verum end;
hence
ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )
by A3; :: thesis: verum