let V be RealLinearSpace; for p, u, v, w 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, u, v, w be VECTOR of V; ( p <> v & v,p // p,w implies ex y being VECTOR of V st
( u,p // p,y & u,v // w,y ) )
assume A1:
( p <> v & v,p // p,w )
; ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )
A2:
now ( p <> w implies ex y being VECTOR of V st
( u,p // p,y & u,v // w,y ) )assume
p <> w
;
ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )then consider a,
b being
Real such that A3:
a * (p - v) = b * (w - p)
and A4:
0 < a
and A5:
0 < b
by A1;
set y =
(((b ") * a) * (p - u)) + p;
A6:
((((b ") * a) * (p - u)) + p) - p =
((b ") * a) * (p - u)
by RLSUB_2:61
.=
(b ") * (a * (p - u))
by RLVECT_1:def 7
;
A7:
((((b ") * a) * (p - u)) + p) - w =
(((((b ") * a) * (p - u)) + p) - p) + (p - w)
by Th1
.=
(((((b ") * a) * (p - u)) + p) - p) - (w - p)
by RLVECT_1:33
;
v - u =
(p - u) + (v - p)
by Th1
.=
(p - u) - (p - v)
by RLVECT_1:33
;
then a * (v - u) =
(a * (p - u)) - (a * (p - v))
by RLVECT_1:34
.=
(b * (((((b ") * a) * (p - u)) + p) - p)) - (b * (w - p))
by A3, A5, A6, Th6
.=
b * (((((b ") * a) * (p - u)) + p) - w)
by A7, RLVECT_1:34
;
then A8:
u,
v // w,
(((b ") * a) * (p - u)) + p
by A4, A5;
0 < b "
by A5;
then A9:
0 < (b ") * a
by A4, XREAL_1:129;
jj * (((((b ") * a) * (p - u)) + p) - p) =
((((b ") * a) * (p - u)) + p) - p
by RLVECT_1:def 8
.=
((b ") * a) * (p - u)
by RLSUB_2:61
;
then
u,
p // p,
(((b ") * a) * (p - u)) + p
by A9;
hence
ex
y being
VECTOR of
V st
(
u,
p // p,
y &
u,
v // w,
y )
by A8;
verum end;
now ( p = w implies ex y being VECTOR of V st
( u,p // p,y & u,v // w,y ) )assume A10:
p = w
;
ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )take y =
p;
( u,p // p,y & u,v // w,y )thus
(
u,
p // p,
y &
u,
v // w,
y )
by A10;
verum end;
hence
ex y being VECTOR of V st
( u,p // p,y & u,v // w,y )
by A2; verum