let V be RealLinearSpace; :: thesis: for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is translational
let OAS be OAffinSpace; :: thesis: ( OAS = OASpace V implies Lambda OAS is translational )
assume A1:
OAS = OASpace V
; :: thesis: Lambda OAS is translational
set AS = Lambda OAS;
for A, P, C being Subset of (Lambda OAS)
for a, b, c, a', b', c' being Element of the carrier of (Lambda OAS) 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
(Lambda OAS);
:: thesis: for a, b, c, a', b', c' being Element of the carrier of (Lambda OAS) 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 the
carrier of
(Lambda OAS);
:: thesis: ( 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 &
A // C )
and A3:
(
a in A &
a' in A &
b in P &
b' in P &
c in C &
c' in C )
and A4:
(
A is
being_line &
P is
being_line &
C is
being_line )
and A5:
(
A <> P &
A <> C )
and A6:
(
a,
b // a',
b' &
a,
c // a',
c' )
;
:: thesis: b,c // b',c'
reconsider a1 =
a,
b1 =
b,
c1 =
c,
a1' =
a',
b1' =
b',
c1' =
c' as
Element of
OAS by Th2;
reconsider u =
a1,
v =
b1,
w =
c1,
u' =
a1' as
VECTOR of
V by A1, Th4;
A7:
now assume A8:
a = a'
;
:: thesis: b,c // b',c'A9:
b = b'
proof
assume A10:
b <> b'
;
:: thesis: contradiction
LIN a,
b,
b'
by A6, A8, AFF_1:def 1;
then
LIN b,
b',
a
by AFF_1:15;
then
a in P
by A3, A4, A10, AFF_1:39;
hence
contradiction
by A2, A3, A5, AFF_1:59;
:: thesis: verum
end;
c = c'
proof
assume A11:
c <> c'
;
:: thesis: contradiction
LIN a,
c,
c'
by A6, A8, AFF_1:def 1;
then
LIN c,
c',
a
by AFF_1:15;
then
a in C
by A3, A4, A11, AFF_1:39;
hence
contradiction
by A2, A3, A5, AFF_1:59;
:: thesis: verum
end; hence
b,
c // b',
c'
by A9, AFF_1:11;
:: thesis: verum end;
now assume A12:
a <> a'
;
:: thesis: b,c // b',c'A13:
not
LIN a1,
a1',
b1
proof
assume
LIN a1,
a1',
b1
;
:: thesis: contradiction
then
LIN a,
a',
b
by Th3;
then
b in A
by A3, A4, A12, AFF_1:39;
hence
contradiction
by A2, A3, A5, AFF_1:59;
:: thesis: verum
end; A14:
not
LIN a1,
a1',
c1
proof
assume
LIN a1,
a1',
c1
;
:: thesis: contradiction
then
LIN a,
a',
c
by Th3;
then
c in A
by A3, A4, A12, AFF_1:39;
hence
contradiction
by A2, A3, A5, AFF_1:59;
:: thesis: verum
end; A15:
(
a1,
b1 '||' a1',
b1' &
a1,
c1 '||' a1',
c1' )
by A6, DIRAF:45;
A16:
(
a1,
a1' '||' b1,
b1' &
a1,
a1' '||' c1,
c1' )
proof
(
a,
a' // b,
b' &
a,
a' // c,
c' )
by A2, A3, AFF_1:53;
hence
(
a1,
a1' '||' b1,
b1' &
a1,
a1' '||' c1,
c1' )
by DIRAF:45;
:: thesis: verum
end; set v'' =
(u' + v) - u;
set w'' =
(u' + w) - u;
reconsider b1'' =
(u' + v) - u,
c1'' =
(u' + w) - u as
Element of the
carrier of
OAS by A1, Th4;
(
u,
u' // v,
(u' + v) - u &
u,
v // u',
(u' + v) - u &
u,
u' // w,
(u' + w) - u &
u,
w // u',
(u' + w) - u )
by ANALOAF:25;
then
(
u,
u' '||' v,
(u' + v) - u &
u,
v '||' u',
(u' + v) - u &
u,
u' '||' w,
(u' + w) - u &
u,
w '||' u',
(u' + w) - u )
by GEOMTRAP:def 1;
then
(
a1,
a1' '||' b1,
b1'' &
a1,
a1' '||' c1,
c1'' &
a1,
b1 '||' a1',
b1'' &
a1,
c1 '||' a1',
c1'' )
by A1, Th5;
then A17:
(
b1'' = b1' &
c1'' = c1' )
by A13, A14, A15, A16, PASCH:12;
((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
v,
w '||' (u' + v) - u,
(u' + w) - u
by GEOMTRAP:def 1;
then
b1,
c1 '||' b1',
c1'
by A1, A17, Th5;
hence
b,
c // b',
c'
by DIRAF:45;
:: thesis: verum end;
hence
b,
c // b',
c'
by A7;
:: thesis: verum
end;
hence
Lambda OAS is translational
by AFF_2:def 11; :: thesis: verum