let V be RealLinearSpace; :: thesis: for OAS being OAffinSpace st OAS = OASpace V holds
OAS is satisfying_DES_1
let OAS be OAffinSpace; :: thesis: ( OAS = OASpace V implies OAS is satisfying_DES_1 )
assume A1:
OAS = OASpace V
; :: thesis: OAS is satisfying_DES_1
for o, a, b, c, a1, b1, c1 being Element of OAS st a,o // o,a1 & b,o // o,b1 & c,o // o,c1 & not LIN o,a,b & not LIN o,a,c & a,b // b1,a1 & a,c // c1,a1 holds
b,c // c1,b1
proof
let o,
a,
b,
c,
a1,
b1,
c1 be
Element of
OAS;
:: thesis: ( a,o // o,a1 & b,o // o,b1 & c,o // o,c1 & not LIN o,a,b & not LIN o,a,c & a,b // b1,a1 & a,c // c1,a1 implies b,c // c1,b1 )
assume that A2:
(
a,
o // o,
a1 &
b,
o // o,
b1 &
c,
o // o,
c1 )
and A3:
( not
LIN o,
a,
b & not
LIN o,
a,
c )
and A4:
(
a,
b // b1,
a1 &
a,
c // c1,
a1 )
;
:: thesis: b,c // c1,b1
reconsider y =
o,
u =
a,
v =
b,
w =
c,
u1 =
a1,
v1 =
b1,
w1 =
c1 as
VECTOR of
V by A1, Th4;
A5:
(
o <> a &
o <> b &
o <> c &
a <> b &
a <> c )
by A3, DIRAF:37;
A6:
now assume A7:
o = a1
;
:: thesis: b,c // c1,b1A8:
o = b1
proof
assume A9:
o <> b1
;
:: thesis: contradiction
a,
b '||' b1,
o
by A4, A7, DIRAF:def 4;
then A10:
o,
b1 '||' b,
a
by DIRAF:27;
b,
o '||' o,
b1
by A2, DIRAF:def 4;
then
o,
b1 '||' o,
b
by DIRAF:27;
then
LIN o,
b1,
b
by DIRAF:def 5;
then
(
LIN o,
b1,
a &
LIN o,
b1,
b &
LIN o,
b1,
o )
by A9, A10, DIRAF:37, DIRAF:39;
hence
contradiction
by A3, A9, DIRAF:38;
:: thesis: verum
end;
o = c1
proof
assume A11:
o <> c1
;
:: thesis: contradiction
a,
c '||' c1,
o
by A4, A7, DIRAF:def 4;
then A12:
o,
c1 '||' c,
a
by DIRAF:27;
c,
o '||' o,
c1
by A2, DIRAF:def 4;
then
o,
c1 '||' o,
c
by DIRAF:27;
then
LIN o,
c1,
c
by DIRAF:def 5;
then
(
LIN o,
c1,
a &
LIN o,
c1,
c &
LIN o,
c1,
o )
by A11, A12, DIRAF:37, DIRAF:39;
hence
contradiction
by A3, A11, DIRAF:38;
:: thesis: verum
end; hence
b,
c // c1,
b1
by A8, DIRAF:7;
:: thesis: verum end;
now assume A13:
o <> a1
;
:: thesis: b,c // c1,b1
u,
y // y,
u1
by A1, A2, GEOMTRAP:2;
then consider r being
Real such that A14:
y - u = r * (u1 - y)
and A15:
0 < r
by A5, A13, Lm1;
(
o,
b // b1,
o &
o,
c // c1,
o )
by A2, DIRAF:5;
then
(
y,
v // v1,
y &
y,
w // w1,
y )
by A1, GEOMTRAP:2;
then A16:
(
y,
v '||' y,
v1 &
y,
w '||' y,
w1 )
by GEOMTRAP:def 1;
(
u,
v // v1,
u1 &
u,
w // w1,
u1 )
by A1, A4, GEOMTRAP:2;
then A17:
(
u,
v '||' u1,
v1 &
u,
w '||' u1,
w1 )
by GEOMTRAP:def 1;
( not
y,
u '||' y,
v & not
y,
u '||' y,
w )
proof
assume
(
y,
u '||' y,
v or
y,
u '||' y,
w )
;
:: thesis: contradiction
then
(
y,
u // y,
v or
y,
u // v,
y or
y,
u // y,
w or
y,
u // w,
y )
by GEOMTRAP:def 1;
then
(
o,
a // o,
b or
o,
a // b,
o or
o,
a // o,
c or
o,
a // c,
o )
by A1, GEOMTRAP:2;
then
(
o,
a '||' o,
b or
o,
a '||' o,
c )
by DIRAF:def 4;
hence
contradiction
by A3, DIRAF:def 5;
:: thesis: verum
end; then
(
v1 = u1 + (((- r) " ) * (v - u)) &
w1 = u1 + (((- r) " ) * (w - u)) )
by A14, A15, A16, A17, Th15;
then A18: 1
* (w1 - v1) =
(u1 + (((- r) " ) * (w - u))) - (u1 + (((- r) " ) * (v - u)))
by RLVECT_1:def 9
.=
(((((- r) " ) * (w - u)) + u1) - u1) - (((- r) " ) * (v - u))
by RLVECT_1:41
.=
(((- r) " ) * (w - u)) - (((- r) " ) * (v - u))
by RLSUB_2:78
.=
((- r) " ) * ((w - u) - (v - u))
by RLVECT_1:48
.=
((- r) " ) * (w - ((v - u) + u))
by RLVECT_1:41
.=
((- r) " ) * (w - v)
by RLSUB_2:78
.=
(- (r " )) * (w - v)
by XCMPLX_1:224
.=
(r " ) * (- (w - v))
by RLVECT_1:38
.=
(r " ) * (v - w)
by RLVECT_1:47
;
(
0 < 1 &
0 < r " )
by A15, XREAL_1:124;
then
w,
v // v1,
w1
by A18, ANALOAF:def 1;
then
c,
b // b1,
c1
by A1, GEOMTRAP:2;
hence
b,
c // c1,
b1
by DIRAF:5;
:: thesis: verum end;
hence
b,
c // c1,
b1
by A6;
:: thesis: verum
end;
hence
OAS is satisfying_DES_1
by Def16; :: thesis: verum