let V be RealLinearSpace; for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is translational
let OAS be OAffinSpace; ( OAS = OASpace V implies Lambda OAS is translational )
assume A1:
OAS = OASpace V
; Lambda OAS is translational
set AS = Lambda OAS;
for A, P, C being Subset of (Lambda OAS)
for a, b, c, a9, b9, c9 being Element of (Lambda OAS) st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9
proof
let A,
P,
C be
Subset of
(Lambda OAS);
for a, b, c, a9, b9, c9 being Element of (Lambda OAS) st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 holds
b,c // b9,c9let a,
b,
c,
a9,
b9,
c9 be
Element of
(Lambda OAS);
( A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
assume that A2:
A // P
and A3:
A // C
and A4:
a in A
and A5:
a9 in A
and A6:
b in P
and A7:
b9 in P
and A8:
c in C
and A9:
c9 in C
and A10:
A is
being_line
and A11:
P is
being_line
and A12:
C is
being_line
and A13:
A <> P
and A14:
A <> C
and A15:
a,
b // a9,
b9
and A16:
a,
c // a9,
c9
;
b,c // b9,c9
reconsider a1 =
a,
b1 =
b,
c1 =
c,
a19 =
a9,
b19 =
b9,
c19 =
c9 as
Element of
OAS by Th1;
reconsider u =
a1,
v =
b1,
w =
c1,
u9 =
a19 as
VECTOR of
V by A1, Th3;
A17:
now ( a <> a9 implies b,c // b9,c9 )assume A18:
a <> a9
;
b,c // b9,c9A19:
not
a1,
a19,
b1 are_collinear
proof
assume
a1,
a19,
b1 are_collinear
;
contradiction
then
LIN a,
a9,
b
by Th2;
then
b in A
by A4, A5, A10, A18, AFF_1:25;
hence
contradiction
by A2, A6, A13, AFF_1:45;
verum
end; A20:
not
a1,
a19,
c1 are_collinear
proof
assume
a1,
a19,
c1 are_collinear
;
contradiction
then
LIN a,
a9,
c
by Th2;
then
c in A
by A4, A5, A10, A18, AFF_1:25;
hence
contradiction
by A3, A8, A14, AFF_1:45;
verum
end;
a,
a9 // c,
c9
by A3, A4, A5, A8, A9, AFF_1:39;
then A21:
a1,
a19 '||' c1,
c19
by DIRAF:38;
a,
a9 // b,
b9
by A2, A4, A5, A6, A7, AFF_1:39;
then A22:
a1,
a19 '||' b1,
b19
by DIRAF:38;
set v99 =
(u9 + v) - u;
set w99 =
(u9 + w) - u;
reconsider b199 =
(u9 + v) - u,
c199 =
(u9 + w) - u as
Element of
OAS by A1, Th3;
((u9 + w) - u) - ((u9 + v) - u) =
(u9 + w) - (((u9 + v) - u) + u)
by RLVECT_1:27
.=
(u9 + w) - (u9 + v)
by RLSUB_2:61
.=
((w + u9) - u9) - v
by RLVECT_1:27
.=
w - v
by RLSUB_2:61
;
then
v,
w // (u9 + v) - u,
(u9 + w) - u
by ANALOAF:15;
then A23:
v,
w '||' (u9 + v) - u,
(u9 + w) - u
by GEOMTRAP:def 1;
u,
u9 // v,
(u9 + v) - u
by ANALOAF:16;
then
u,
u9 '||' v,
(u9 + v) - u
by GEOMTRAP:def 1;
then A24:
a1,
a19 '||' b1,
b199
by A1, Th4;
u,
w // u9,
(u9 + w) - u
by ANALOAF:16;
then
u,
w '||' u9,
(u9 + w) - u
by GEOMTRAP:def 1;
then A25:
a1,
c1 '||' a19,
c199
by A1, Th4;
u,
u9 // w,
(u9 + w) - u
by ANALOAF:16;
then
u,
u9 '||' w,
(u9 + w) - u
by GEOMTRAP:def 1;
then A26:
a1,
a19 '||' c1,
c199
by A1, Th4;
u,
v // u9,
(u9 + v) - u
by ANALOAF:16;
then
u,
v '||' u9,
(u9 + v) - u
by GEOMTRAP:def 1;
then A27:
a1,
b1 '||' a19,
b199
by A1, Th4;
a1,
c1 '||' a19,
c19
by A16, DIRAF:38;
then A28:
c199 = c19
by A20, A21, A26, A25, PASCH:5;
a1,
b1 '||' a19,
b19
by A15, DIRAF:38;
then
b199 = b19
by A19, A22, A24, A27, PASCH:5;
then
b1,
c1 '||' b19,
c19
by A1, A28, A23, Th4;
hence
b,
c // b9,
c9
by DIRAF:38;
verum end;
now ( a = a9 implies b,c // b9,c9 )assume A29:
a = a9
;
b,c // b9,c9A30:
c = c9
proof
LIN a,
c,
c9
by A16, A29, AFF_1:def 1;
then A31:
LIN c,
c9,
a
by AFF_1:6;
assume
c <> c9
;
contradiction
then
a in C
by A8, A9, A12, A31, AFF_1:25;
hence
contradiction
by A3, A4, A14, AFF_1:45;
verum
end;
b = b9
proof
LIN a,
b,
b9
by A15, A29, AFF_1:def 1;
then A32:
LIN b,
b9,
a
by AFF_1:6;
assume
b <> b9
;
contradiction
then
a in P
by A6, A7, A11, A32, AFF_1:25;
hence
contradiction
by A2, A4, A13, AFF_1:45;
verum
end; hence
b,
c // b9,
c9
by A30, AFF_1:2;
verum end;
hence
b,
c // b9,
c9
by A17;
verum
end;
hence
Lambda OAS is translational
by AFF_2:def 11; verum