let V be RealLinearSpace; for OAS being OAffinSpace st OAS = OASpace V holds
OAS is satisfying_DES_1
let OAS be OAffinSpace; ( OAS = OASpace V implies OAS is satisfying_DES_1 )
assume A1:
OAS = OASpace V
; 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 o,a,b are_collinear & not o,a,c are_collinear & 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;
( a,o // o,a1 & b,o // o,b1 & c,o // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // b1,a1 & a,c // c1,a1 implies b,c // c1,b1 )
assume that A2:
a,
o // o,
a1
and A3:
b,
o // o,
b1
and A4:
c,
o // o,
c1
and A5:
not
o,
a,
b are_collinear
and A6:
not
o,
a,
c are_collinear
and A7:
a,
b // b1,
a1
and A8:
a,
c // c1,
a1
;
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, Th3;
A9:
o <> a
by A5, DIRAF:31;
A10:
now ( o <> a1 implies b,c // c1,b1 )A11:
( not
y,
u '||' y,
v & not
y,
u '||' y,
w )
proof
assume
(
y,
u '||' y,
v or
y,
u '||' y,
w )
;
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 A5, A6, DIRAF:def 5;
verum
end;
o,
c // c1,
o
by A4, DIRAF:2;
then
y,
w // w1,
y
by A1, GEOMTRAP:2;
then A12:
y,
w '||' y,
w1
by GEOMTRAP:def 1;
o,
b // b1,
o
by A3, DIRAF:2;
then
y,
v // v1,
y
by A1, GEOMTRAP:2;
then A13:
y,
v '||' y,
v1
by GEOMTRAP:def 1;
assume A14:
o <> a1
;
b,c // c1,b1
u,
y // y,
u1
by A1, A2, GEOMTRAP:2;
then consider r being
Real such that A15:
y - u = r * (u1 - y)
and A16:
0 < r
by A9, A14, Lm1;
u,
w // w1,
u1
by A1, A8, GEOMTRAP:2;
then
u,
w '||' u1,
w1
by GEOMTRAP:def 1;
then A17:
w1 = u1 + (((- r) ") * (w - u))
by A15, A16, A12, A11, Th10;
u,
v // v1,
u1
by A1, A7, GEOMTRAP:2;
then
u,
v '||' u1,
v1
by GEOMTRAP:def 1;
then
v1 = u1 + (((- r) ") * (v - u))
by A15, A16, A13, A11, Th10;
then A18: 1
* (w1 - v1) =
(u1 + (((- r) ") * (w - u))) - (u1 + (((- r) ") * (v - u)))
by A17, RLVECT_1:def 8
.=
(((((- r) ") * (w - u)) + u1) - u1) - (((- r) ") * (v - u))
by RLVECT_1:27
.=
(((- r) ") * (w - u)) - (((- r) ") * (v - u))
by RLSUB_2:61
.=
((- r) ") * ((w - u) - (v - u))
by RLVECT_1:34
.=
((- r) ") * (w - ((v - u) + u))
by RLVECT_1:27
.=
((- r) ") * (w - v)
by RLSUB_2:61
.=
(- (r ")) * (w - v)
by XCMPLX_1:222
.=
(r ") * (- (w - v))
by RLVECT_1:24
.=
(r ") * (v - w)
by RLVECT_1:33
;
0 < r "
by A16, XREAL_1:122;
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:2;
verum end;
now ( o = a1 implies b,c // c1,b1 )assume A19:
o = a1
;
b,c // c1,b1A20:
o = c1
proof
c,
o '||' o,
c1
by A4, DIRAF:def 4;
then
o,
c1 '||' o,
c
by DIRAF:22;
then A21:
o,
c1,
c are_collinear
by DIRAF:def 5;
A22:
o,
c1,
o are_collinear
by DIRAF:31;
assume A23:
o <> c1
;
contradiction
a,
c '||' c1,
o
by A8, A19, DIRAF:def 4;
then
o,
c1 '||' c,
a
by DIRAF:22;
then
o,
c1,
a are_collinear
by A23, A21, DIRAF:33;
hence
contradiction
by A6, A23, A21, A22, DIRAF:32;
verum
end;
o = b1
proof
b,
o '||' o,
b1
by A3, DIRAF:def 4;
then
o,
b1 '||' o,
b
by DIRAF:22;
then A24:
o,
b1,
b are_collinear
by DIRAF:def 5;
A25:
o,
b1,
o are_collinear
by DIRAF:31;
assume A26:
o <> b1
;
contradiction
a,
b '||' b1,
o
by A7, A19, DIRAF:def 4;
then
o,
b1 '||' b,
a
by DIRAF:22;
then
o,
b1,
a are_collinear
by A26, A24, DIRAF:33;
hence
contradiction
by A5, A26, A24, A25, DIRAF:32;
verum
end; hence
b,
c // c1,
b1
by A20, DIRAF:4;
verum end;
hence
b,
c // c1,
b1
by A10;
verum
end;
hence
OAS is satisfying_DES_1
; verum