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
for a, b, c, a', b', c' being Element of st A // P & A // C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
proof
let A,
P,
C be
Subset of ;
for a, b, c, a', b', c' being Element of st A // P & A // C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'let a,
b,
c,
a',
b',
c' be
Element of ;
( A // P & A // C & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' implies b,c // b',c' )
assume that A2:
A // P
and A3:
A // C
and A4:
a in A
and A5:
a' in A
and A6:
b in P
and A7:
b' in P
and A8:
c in C
and A9:
c' 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 // a',
b'
and A16:
a,
c // a',
c'
;
b,c // b',c'
reconsider a1 =
a,
b1 =
b,
c1 =
c,
a1' =
a',
b1' =
b',
c1' =
c' as
Element of
by Th2;
reconsider u =
a1,
v =
b1,
w =
c1,
u' =
a1' as
VECTOR of
by A1, Th4;
A17:
now assume A18:
a <> a'
;
b,c // b',c'A19:
not
LIN a1,
a1',
b1
proof
assume
LIN a1,
a1',
b1
;
contradiction
then
LIN a,
a',
b
by Th3;
then
b in A
by A4, A5, A10, A18, AFF_1:39;
hence
contradiction
by A2, A6, A13, AFF_1:59;
verum
end; A20:
not
LIN a1,
a1',
c1
proof
assume
LIN a1,
a1',
c1
;
contradiction
then
LIN a,
a',
c
by Th3;
then
c in A
by A4, A5, A10, A18, AFF_1:39;
hence
contradiction
by A3, A8, A14, AFF_1:59;
verum
end;
a,
a' // c,
c'
by A3, A4, A5, A8, A9, AFF_1:53;
then A21:
a1,
a1' '||' c1,
c1'
by DIRAF:45;
a,
a' // b,
b'
by A2, A4, A5, A6, A7, AFF_1:53;
then A22:
a1,
a1' '||' b1,
b1'
by DIRAF:45;
set v'' =
(u' + v) - u;
set w'' =
(u' + w) - u;
reconsider b1'' =
(u' + v) - u,
c1'' =
(u' + w) - u as
Element of
by A1, Th4;
((u' + w) - u) - ((u' + v) - u) =
(u' + w) - (((u' + v) - u) + u)
by RLVECT_1:41
.=
(u' + w) - (u' + v)
by RLSUB_2:78
.=
((w + u') - u') - v
by RLVECT_1:41
.=
w - v
by RLSUB_2:78
;
then
v,
w // (u' + v) - u,
(u' + w) - u
by ANALOAF:24;
then A23:
v,
w '||' (u' + v) - u,
(u' + w) - u
by GEOMTRAP:def 1;
u,
u' // v,
(u' + v) - u
by ANALOAF:25;
then
u,
u' '||' v,
(u' + v) - u
by GEOMTRAP:def 1;
then A24:
a1,
a1' '||' b1,
b1''
by A1, Th5;
u,
w // u',
(u' + w) - u
by ANALOAF:25;
then
u,
w '||' u',
(u' + w) - u
by GEOMTRAP:def 1;
then A25:
a1,
c1 '||' a1',
c1''
by A1, Th5;
u,
u' // w,
(u' + w) - u
by ANALOAF:25;
then
u,
u' '||' w,
(u' + w) - u
by GEOMTRAP:def 1;
then A26:
a1,
a1' '||' c1,
c1''
by A1, Th5;
u,
v // u',
(u' + v) - u
by ANALOAF:25;
then
u,
v '||' u',
(u' + v) - u
by GEOMTRAP:def 1;
then A27:
a1,
b1 '||' a1',
b1''
by A1, Th5;
a1,
c1 '||' a1',
c1'
by A16, DIRAF:45;
then A28:
c1'' = c1'
by A20, A21, A26, A25, PASCH:12;
a1,
b1 '||' a1',
b1'
by A15, DIRAF:45;
then
b1'' = b1'
by A19, A22, A24, A27, PASCH:12;
then
b1,
c1 '||' b1',
c1'
by A1, A28, A23, Th5;
hence
b,
c // b',
c'
by DIRAF:45;
verum end;
now assume A29:
a = a'
;
b,c // b',c'A30:
c = c'
proof
LIN a,
c,
c'
by A16, A29, AFF_1:def 1;
then A31:
LIN c,
c',
a
by AFF_1:15;
assume
c <> c'
;
contradiction
then
a in C
by A8, A9, A12, A31, AFF_1:39;
hence
contradiction
by A3, A4, A14, AFF_1:59;
verum
end;
b = b'
proof
LIN a,
b,
b'
by A15, A29, AFF_1:def 1;
then A32:
LIN b,
b',
a
by AFF_1:15;
assume
b <> b'
;
contradiction
then
a in P
by A6, A7, A11, A32, AFF_1:39;
hence
contradiction
by A2, A4, A13, AFF_1:59;
verum
end; hence
b,
c // b',
c'
by A30, AFF_1:11;
verum end;
hence
b,
c // b',
c'
by A17;
verum
end;
hence
Lambda OAS is translational
by AFF_2:def 11; verum