:: Fanoian, Pappian and Desarguesian Affine Spaces
:: by Krzysztof Pra\.zmowski
::
:: Received November 16, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ANALOAF, DIRAF, ZFMISC_1, SUBSET_1, STRUCT_0, PARSP_1,
RLVECT_1, REAL_1, RELAT_1, ARYTM_3, SUPINF_2, CARD_1, ARYTM_1, VECTSP_1,
AFF_2, TRANSGEO, CONAFFM, AFF_1, INCSP_1, PENCIL_1;
notations ORDINAL1, NUMBERS, STRUCT_0, RLVECT_1, XXREAL_0, XCMPLX_0, XREAL_0,
REAL_1, ANALOAF, DIRAF, AFF_1, AFF_2, GEOMTRAP, TRANSLAC;
constructors XXREAL_0, REAL_1, MEMBERED, AFF_1, AFF_2, TRANSLAC, GEOMTRAP;
registrations MEMBERED, STRUCT_0, DIRAF, XREAL_0;
requirements NUMERALS, REAL, SUBSET, ARITHM;
definitions TRANSLAC;
equalities RLVECT_1;
theorems RLVECT_1, FUNCSDOM, ANALOAF, DIRAF, AFF_1, AFF_2, PASCH, ANALMETR,
GEOMTRAP, RLSUB_2, XCMPLX_0, XCMPLX_1, XREAL_1;
begin
registration
let OAS be OAffinSpace;
cluster Lambda(OAS) -> AffinSpace-like non trivial;
correctness by DIRAF:41;
end;
registration
let OAS be OAffinPlane;
cluster Lambda(OAS) -> 2-dimensional;
correctness by DIRAF:45;
end;
theorem Th1:
for OAS being OAffinSpace, x being set holds (x is Element of OAS
iff x is Element of Lambda(OAS)) & (x is Subset of OAS iff x is Subset of
Lambda(OAS))
proof
let OAS be OAffinSpace;
Lambda(OAS) = AffinStruct (#the carrier of OAS, lambda(the CONGR of OAS)
#) by DIRAF:def 2;
hence thesis;
end;
theorem Th2:
for OAS being OAffinSpace holds for a,b,c being (Element of OAS),
a9,b9,c9 being (Element of Lambda(OAS)) st a=a9 & b=b9 & c =c9
holds a,b,c are_collinear
iff LIN a9,b9,c9
proof
let OAS be OAffinSpace;
let a,b,c be (Element of OAS), a9,b9,c9 be (Element of Lambda(OAS)) such
that
A1: a=a9 & b=b9 & c =c9;
A2: now
assume a,b,c are_collinear;
then a,b '||' a,c by DIRAF:def 5;
then a9,b9 // a9, c9 by A1,DIRAF:38;
hence LIN a9,b9,c9 by AFF_1:def 1;
end;
now
assume LIN a9,b9,c9;
then a9,b9 // a9,c9 by AFF_1:def 1;
then a,b '||' a,c by A1,DIRAF:38;
hence a,b,c are_collinear by DIRAF:def 5;
end;
hence thesis by A2;
end;
theorem Th3:
for V being RealLinearSpace, x being set holds (x is Element of
OASpace(V) iff x is VECTOR of V)
proof
let V be RealLinearSpace, x be set;
(OASpace(V)) = AffinStruct (#the carrier of V, DirPar(V)#) by ANALOAF:def 4;
hence thesis;
end;
theorem Th4:
for V being RealLinearSpace, OAS being OAffinSpace st OAS=OASpace
(V) holds for a,b,c,d being Element of OAS,u,v,w,y being VECTOR of V st a=u & b
=v & c =w & d=y holds (a,b '||' c,d iff u,v '||' w,y)
proof
let V be RealLinearSpace, OAS be OAffinSpace such that
A1: OAS=OASpace(V);
let a,b,c,d be Element of OAS,u,v,w,y be VECTOR of V;
assume
A2: a=u & b=v & c =w & d=y;
A3: now
assume u,v '||' w,y;
then u,v // w,y or u,v // y,w by GEOMTRAP:def 1;
then a,b // c,d or a,b // d,c by A1,A2,GEOMTRAP:2;
hence a,b '||' c,d by DIRAF:def 4;
end;
now
assume a,b '||' c,d;
then a,b // c,d or a,b // d,c by DIRAF:def 4;
then u,v // w,y or u,v // y,w by A1,A2,GEOMTRAP:2;
hence u,v '||' w,y by GEOMTRAP:def 1;
end;
hence thesis by A3;
end;
theorem
for V being RealLinearSpace, OAS being OAffinSpace st OAS=OASpace(V)
holds ex u,v being VECTOR of V st for a,b being Real st a*u + b*v = 0.V holds a
=0 & b=0
proof
let V be RealLinearSpace, OAS be OAffinSpace such that
A1: OAS = OASpace(V);
consider a,b,c,d being Element of OAS such that
A2: ( not a,b // c,d)& not a,b // d,c by ANALOAF:def 5;
reconsider u=a,v=b,w=c,y=d as VECTOR of V by A1,Th3;
take z1=v-u,z2=y-w;
now
let r1,r2 be Real;
assume r1*z1+r2*z2 = 0.V;
then
A3: r1*z1 = -(r2*z2) by RLVECT_1:6
.= r2*(-z2) by RLVECT_1:25
.= (-r2)*z2 by RLVECT_1:24;
assume r1<>0 or r2<>0;
then r1<>0 or -r2<>0;
then u,v // w,y or u,v // y,w by A3,ANALMETR:14;
hence r1=0 & r2=0 by A1,A2,GEOMTRAP:2;
end;
hence thesis;
end;
definition
let AS be AffinSpace;
redefine attr AS is Fanoian means :: redefines Fanoian (TRANSLAC, definition)
for a,b,c,d being Element of AS st a,b // c,
d & a,c // b,d & a,d // b,c holds a,b // a,c;
compatibility
proof
thus AS is Fanoian implies for a,b,c,d being Element of AS st a,b // c,d &
a,c // b,d & a,d // b,c holds a,b // a,c
proof
assume
A1: for a,b,c,d being Element of AS st a,b // c,d & a,c // b,d & a,d
// b,c holds LIN a,b,c;
let a,b,c,d be Element of AS;
assume a,b // c,d & a,c // b,d & a,d // b,c;
then LIN a,b,c by A1;
hence thesis by AFF_1:def 1;
end;
assume
A2: for a,b,c,d being Element of AS st a,b // c,d & a,c // b,d & a,d
// b,c holds a,b // a,c;
let a,b,c,d be Element of AS;
assume a,b // c,d & a,c // b,d & a,d // b,c;
then a,b // a,c by A2;
hence thesis by AFF_1:def 1;
end;
end;
definition
let IT be OAffinSpace;
attr IT is Pappian means
:Def2:
Lambda(IT) is Pappian;
attr IT is Desarguesian means
:Def3:
Lambda(IT) is Desarguesian;
attr IT is Moufangian means
:Def4:
Lambda(IT) is Moufangian;
attr IT is translation means
:Def5:
Lambda(IT) is translational;
end;
definition
let OAS be OAffinSpace;
attr OAS is satisfying_DES means
for o,a,b,c,a1,b1,c1 being Element
of OAS st o,a // o,a1 & o,b // o,b1 & o,c // o,c1 &
not o,a,b are_collinear & not o,a,c are_collinear &
a,b // a1,b1 & a,c // a1,c1 holds b,c // b1,c1;
end;
definition
let OAS be OAffinSpace;
attr OAS is satisfying_DES_1 means
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;
end;
theorem Th6:
for OAS being OAffinSpace st OAS is satisfying_DES_1 holds OAS
is satisfying_DES
proof
let OAS be OAffinSpace such that
A1: OAS is satisfying_DES_1;
for o,a,b,c,a1,b1,c1 being Element of OAS st o,a // o,a1 & o,b // o,b1 &
o,c // o,c1 & not o,a,b are_collinear & not o,a,c are_collinear & a,b // a1,b1
& a,c // a1,c1 holds
b,c // b1,c1
proof
let o,a,b,c,a1,b1,c1 be Element of OAS such that
A2: o,a // o,a1 and
A3: o,b // o,b1 and
A4: o,c // o,c1 and
A5: not o,a,b are_collinear and
A6: not o,a,c are_collinear and
A7: a,b // a1,b1 and
A8: a,c // a1,c1;
consider a2 being Element of OAS such that
A9: Mid a,o,a2 and
A10: o<>a2 by DIRAF:13;
A11: a,o // o,a2 by A9,DIRAF:def 3;
A12: o<>a by A5,DIRAF:31;
then consider c2 being Element of OAS such that
A13: c,o // o,c2 and
A14: c,a // a2,c2 by A11,ANALOAF:def 5;
A15: c2,a2 // a,c by A14,DIRAF:2;
A16: c2,o // o,c by A13,DIRAF:2;
then Mid c2,o,c by DIRAF:def 3;
then
A17: c2,o,c are_collinear by DIRAF:28;
a,o,a2 are_collinear by A9,DIRAF:28;
then
A18: o,a2,a are_collinear by DIRAF:30;
A19: o<>c2
proof
assume o=c2;
then o,a2 // a,c by A14,DIRAF:2;
then o,a2 '||' a,c by DIRAF:def 4;
then o,a2,o are_collinear & o,a2,c are_collinear by A10,A18,DIRAF:31,33;
hence contradiction by A6,A10,A18,DIRAF:32;
end;
A20: not o,a2,c2 are_collinear
proof
A21: c2,o,o are_collinear by DIRAF:31;
A22: o,a2,o are_collinear by DIRAF:31;
assume o,a2,c2 are_collinear;
then c2,o,a are_collinear by A10,A18,A22,DIRAF:32;
hence contradiction by A6,A17,A19,A21,DIRAF:32;
end;
consider b2 being Element of OAS such that
A23: b,o // o,b2 and
A24: b,a // a2,b2 by A12,A11,ANALOAF:def 5;
A25: b2,a2 // a,b by A24,DIRAF:2;
a<>b by A5,DIRAF:31;
then b2,a2 // a1,b1 by A7,A25,DIRAF:3;
then
A26: a2,b2 // b1,a1 by DIRAF:2;
o<>c by A6,DIRAF:31;
then
A27: c2,o // o,c1 by A4,A16,DIRAF:3;
A28: a,c // c2,a2 by A14,ANALOAF:def 5;
A29: b2,o // o,b by A23,DIRAF:2;
then Mid b2,o,b by DIRAF:def 3;
then
A30: b2,o,b are_collinear by DIRAF:28;
A31: o<>b2
proof
assume o=b2;
then o,a2 // a,b by A24,DIRAF:2;
then o,a2 '||' a,b by DIRAF:def 4;
then o,a2,o are_collinear & o,a2,b are_collinear by A10,A18,DIRAF:31,33;
hence contradiction by A5,A10,A18,DIRAF:32;
end;
A32: not o,a2,b2 are_collinear
proof
A33: b2,o,o are_collinear by DIRAF:31;
A34: o,a2,o are_collinear by DIRAF:31;
assume o,a2,b2 are_collinear;
then b2,o,a are_collinear by A10,A18,A34,DIRAF:32;
hence contradiction by A5,A30,A31,A33,DIRAF:32;
end;
A35: now
b2,a2 // a,b by A24,DIRAF:2;
then
A36: b2,a2 '||' a,b by DIRAF:def 4;
assume
A37: c2=b2;
then
A38: o,b2,c are_collinear by A17,DIRAF:30;
c2,a2 // a,c by A14,DIRAF:2;
then
A39: b2,a2 '||' a,c by A37,DIRAF:def 4;
( not o,b2,a2 are_collinear)& o,b2,b are_collinear by A30,A32,DIRAF:30;
then b=c by A18,A38,A36,A39,PASCH:4;
hence thesis by DIRAF:4;
end;
a2,o // o,a by A11,DIRAF:2;
then
A40: a2,o // o,a1 by A2,A12,DIRAF:3;
a<>c by A6,DIRAF:31;
then c2,a2 // a1,c1 by A8,A15,DIRAF:3;
then
A41: a2,c2 // c1,a1 by DIRAF:2;
o<>b by A5,DIRAF:31;
then b2,o // o,b1 by A3,A29,DIRAF:3;
then
A42: c2,b2 // b1,c1 by A1,A40,A27,A41,A26,A32,A20;
a,b // b2,a2 by A24,ANALOAF:def 5;
then b,c // c2,b2 by A1,A5,A6,A11,A23,A13,A28;
hence thesis by A42,A35,DIRAF:3;
end;
hence thesis;
end;
theorem Th7:
for OAS being OAffinSpace holds for o,a,b,a9,b9 being Element
of OAS st not o,a,b are_collinear & a,o // o,a9 &
o,b,b9 are_collinear & a,b '||' a9,b9
holds b,o // o,b9 & a,b // b9,a9
proof
let OAS be OAffinSpace;
let o,a,b,a9,b9 be Element of OAS such that
A1: not o,a,b are_collinear and
A2: a,o // o,a9 and
A3: o,b,b9 are_collinear and
A4: a,b '||' a9,b9;
Mid a,o,a9 & a,b '||' b9,a9 by A2,A4,DIRAF:22,def 3;
then Mid b,o,b9 by A1,A3,PASCH:6;
hence b,o // o,b9 by DIRAF:def 3;
hence thesis by A1,A2,A4,PASCH:12;
end;
theorem Th8:
for OAS being OAffinSpace holds for o,a,b,a9,b9 being Element
of OAS st not o,a,b are_collinear & o,a // o,a9 & o,b,b9 are_collinear &
a,b '||' a9,b9
holds o,b // o,b9 & a,b // a9,b9
proof
let OAS be OAffinSpace;
let o,a,b,a9,b9 be Element of OAS such that
A1: not o,a,b are_collinear and
A2: o,a // o,a9 and
A3: o,b,b9 are_collinear and
A4: a,b '||' a9,b9;
A5: o<>a by A1,DIRAF:31;
consider a2 being Element of OAS such that
A6: Mid a,o,a2 and
A7: o<>a2 by DIRAF:13;
a,o // o,a2 by A6,DIRAF:def 3;
then consider b2 being Element of OAS such that
A8: b,o // o,b2 and
A9: b,a // a2,b2 by A5,ANALOAF:def 5;
A10: o,b // b2,o by A8,DIRAF:2;
a,o // o,a2 by A6,DIRAF:def 3;
then a2,o // o,a by DIRAF:2;
then
A11: a2,o // o,a9 by A2,A5,DIRAF:3;
a,o,a2 are_collinear by A6,DIRAF:28;
then
A12: o,a2,a are_collinear by DIRAF:30;
A13: o<>b2
proof
assume o=b2;
then o,a2 // a,b by A9,DIRAF:2;
then o,a2 '||' a,b by DIRAF:def 4;
then o,a2,o are_collinear & o,a2,b are_collinear by A7,A12,DIRAF:31,33;
hence contradiction by A1,A7,A12,DIRAF:32;
end;
Mid b,o,b2 by A8,DIRAF:def 3;
then b,o,b2 are_collinear by DIRAF:28;
then
A14: b2,o,b are_collinear by DIRAF:30;
A15: not o,a2,b2 are_collinear
proof
A16: b2,o,o are_collinear by DIRAF:31;
A17: o,a2,o are_collinear by DIRAF:31;
assume o,a2,b2 are_collinear;
then b2,o,a are_collinear by A7,A12,A17,DIRAF:32;
hence contradiction by A1,A14,A13,A16,DIRAF:32;
end;
a2,b2 // b,a by A9,DIRAF:2;
then
A18: a2,b2 '||' a,b by DIRAF:def 4;
b<>a by A1,DIRAF:31;
then
A19: a2,b2 '||' a9,b9 by A4,A18,DIRAF:23;
A20: a,b // b2,a2 by A9,DIRAF:2;
Mid b,o,b2 by A8,DIRAF:def 3;
then b,o,b2 are_collinear by DIRAF:28;
then
A21: o,b,b2 are_collinear by DIRAF:30;
A22: o,b,o are_collinear by DIRAF:31;
o<>b by A1,DIRAF:31;
then
A23: o,b2,b9 are_collinear by A3,A21,A22,DIRAF:32;
then a2,b2 // b9,a9 by A15,A11,A19,Th7;
then
A24: b2,a2 // a9,b9 by DIRAF:2;
b2,o // o,b9 by A15,A11,A19,A23,Th7;
hence o,b // o,b9 by A13,A10,DIRAF:3;
a2<>b2 by A15,DIRAF:31;
hence thesis by A20,A24,DIRAF:3;
end;
theorem Th9:
for OAP being OAffinSpace st OAP is satisfying_DES_1 holds
Lambda(OAP) is Desarguesian
proof
let OAP be OAffinSpace;
set AP = Lambda(OAP);
assume
A1: OAP is satisfying_DES_1;
then
A2: OAP is satisfying_DES by Th6;
for A,P,C being Subset of AP, o,a,b,c,a9,b9,c9 being Element of AP st o
in A & o in P & o in C & o<>a & o<>b & o<>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 AP;
let o,a,b,c,a9,b9,c9 be Element of AP;
reconsider o1=o,a1=a,b1=b,c1=c,a19=a9,b19=b9,c19=c9 as Element of OAP by
Th1;
assume that
A3: o in A and
A4: o in P and
A5: o in C and
A6: o<>a and
A7: o<>b and
A8: o<>c and
A9: a in A and
A10: a9 in A and
A11: b in P and
A12: b9 in P and
A13: c in C and
A14: c9 in C and
A15: A is being_line and
A16: P is being_line and
A17: C is being_line and
A18: A<>P and
A19: A<>C and
A20: a,b // a9,b9 & a,c // a9,c9;
LIN o,b,b9 by A4,A11,A12,A16,AFF_1:21;
then
A21: o1,b1,b19 are_collinear by Th2;
A22: not o1,a1,b1 are_collinear & not o1,a1,c1 are_collinear
proof
A23: now
assume LIN o,a,c;
then consider X being Subset of Lambda(OAP) such that
A24: X is being_line & o in X and
A25: a in X and
A26: c in X by AFF_1:21;
X = C by A5,A8,A13,A17,A24,A26,AFF_1:18;
hence contradiction by A3,A6,A9,A15,A19,A24,A25,AFF_1:18;
end;
A27: now
assume LIN o,a,b;
then consider X being Subset of Lambda(OAP) such that
A28: X is being_line & o in X and
A29: a in X and
A30: b in X by AFF_1:21;
X = P by A4,A7,A11,A16,A28,A30,AFF_1:18;
hence contradiction by A3,A6,A9,A15,A18,A28,A29,AFF_1:18;
end;
assume not thesis;
hence contradiction by A27,A23,Th2;
end;
LIN o,c,c9 by A5,A13,A14,A17,AFF_1:21;
then
A31: o1,c1,c19 are_collinear by Th2;
A32: a1,b1 '||' a19,b19 & a1,c1 '||' a19,c19 by A20,DIRAF:38;
A33: now
assume
A34: a1,o1 // o1,a19;
then
A35: a1,b1 // b19,a19 & a1,c1 // c19,a19 by A21,A31,A22,A32,Th7;
b1,o1 // o1,b19 & c1,o1 // o1,c19 by A21,A31,A22,A32,A34,Th7;
then b1,c1 // c19,b19 by A1,A22,A34,A35;
then b1,c1 '||' b19,c19 by DIRAF:def 4;
hence thesis by DIRAF:38;
end;
A36: now
assume
A37: o1,a1 // o1,a19;
then
A38: a1,b1 // a19,b19 & a1,c1 // a19,c19 by A21,A31,A22,A32,Th8;
o1,b1 // o1,b19 & o1,c1 // o1,c19 by A21,A31,A22,A32,A37,Th8;
then b1,c1 // b19,c19 by A2,A22,A37,A38;
then b1,c1 '||' b19,c19 by DIRAF:def 4;
hence thesis by DIRAF:38;
end;
LIN o,a,a9 by A3,A9,A10,A15,AFF_1:21;
then o1,a1,a19 are_collinear by Th2;
then Mid o1,a1,a19 or Mid a1,o1,a19 or Mid o1,a19,a1 by DIRAF:29;
hence thesis by A33,A36,DIRAF:7,def 3;
end;
hence thesis by AFF_2:def 4;
end;
theorem Th10:
for V being RealLinearSpace holds for o,u,v,u1,v1 being VECTOR
of V, r being Real
st o-u=r*(u1-o) & r<>0 & o,v '||' o,v1 & not o,u '||' o,v &
u,v '||' u1,v1 holds v1 = u1 + (-r)"*(v-u) & v1 = o + (-r)"*(v-o) & v-u = (-r)*
(v1-u1)
proof
let V be RealLinearSpace;
let o,u,v,u1,v1 be VECTOR of V, r be Real such that
A1: o-u=r*(u1-o) and
A2: r<>0 and
A3: o,v '||' o,v1 and
A4: not o,u '||' o,v and
A5: u,v '||' u1,v1;
A6: -r <> 0 by A2;
for r1,r2 being Real st r1*(u-o)+r2*(v-o) = 0.V holds r1=0 & r2=0
proof
let r1,r2 be Real;
assume r1*(u-o)+r2*(v-o) = 0.V;
then
A7: r1*(u-o) = -(r2*(v-o)) by RLVECT_1:6
.= r2*(-(v-o)) by RLVECT_1:25
.= (-r2)*(v-o) by RLVECT_1:24;
assume r1<>0 or r2<>0;
then r1<>0 or -r2<>0;
then o,u // o,v or o,u // v,o by A7,ANALMETR:14;
hence contradiction by A4,GEOMTRAP:def 1;
end;
then reconsider X = OASpace(V) as OAffinSpace by ANALOAF:26;
set w = u1 + (-r)"*(v-u);
reconsider p=o,a=u,a1=u1,b=v,b1=v1,q=w as Element of X by Th3;
a,b '||' a1,b1 by A5,Th4;
then
A8: b,a '||' a1,b1 by DIRAF:22;
p,b '||' p,b1 by A3,Th4;
then
A9: p,b,b1 are_collinear by DIRAF:def 5;
A10: (-r)*(w-u1) = (-r)*((-r)"*(v-u)) by RLSUB_2:61
.= ((-r)*(-r)")*(v-u) by RLVECT_1:def 7
.= 1*(v-u) by A6,XCMPLX_0:def 7;
then
A11: v-u = (-r)*(w-u1) by RLVECT_1:def 8;
u,v // u1,w or u,v // w,u1 by A10,ANALMETR:14;
then u,v '||' u1,w by GEOMTRAP:def 1;
then a,b '||' a1,q by Th4;
then
A12: b,a '||' a1,q by DIRAF:22;
A13: (-r)*(o-w) = (-r)*o - (-r)*w by RLVECT_1:34
.= (-r)*o - ((-r)*u1 + (-r)*((-r)"*(v-u))) by RLVECT_1:def 5
.= (-r)*o - ((-r)*u1 + ((-r)*(-r)")*(v-u)) by RLVECT_1:def 7
.= (-r)*o - ((-r)*u1 + 1*(v-u)) by A6,XCMPLX_0:def 7
.= (-r)*o - ((-r)*u1 + (v-u)) by RLVECT_1:def 8
.= ((-r)*o - (-r)*u1) - (v-u) by RLVECT_1:27
.= (-r)*(o-u1) - (v-u) by RLVECT_1:34
.= r*(-(o-u1)) - (v-u) by RLVECT_1:24
.= (o-u) - (v-u) by A1,RLVECT_1:33
.= o - ((v-u)+u) by RLVECT_1:27
.= o - v by RLSUB_2:61
.= 1*(o-v) by RLVECT_1:def 8;
then v,o // w,o or v,o // o,w by ANALMETR:14;
then o,v // w,o or o,v // o,w by ANALOAF:12;
then o,v '||' o,w by GEOMTRAP:def 1;
then p,b '||' p,q by Th4;
then
A14: p,b,q are_collinear by DIRAF:def 5;
1*(u-o) = (-1)*(-(u-o)) by RLVECT_1:26
.= (-1)*(r*(u1-o)) by A1,RLVECT_1:33
.= ((-1)*r)*(u1-o) by RLVECT_1:def 7
.= (-r)*(u1-o);
then o,u // o,u1 or o,u // u1,o by ANALMETR:14;
then o,u '||' o,u1 by GEOMTRAP:def 1;
then p,a '||' p,a1 by Th4;
then
A15: p,a,a1 are_collinear by DIRAF:def 5;
A16: not p,b,a are_collinear
proof
assume p,b,a are_collinear;
then p,b '||' p,a by DIRAF:def 5;
then p,a '||' p,b by DIRAF:22;
hence contradiction by A4,Th4;
end;
A17: (-r)*(w-o) = r*(-(w-o)) by RLVECT_1:24
.= r*(o-w) by RLVECT_1:33
.= -(-(r*(o-w))) by RLVECT_1:17
.= -(r*(-(o-w))) by RLVECT_1:25
.= -(1*(o-v)) by A13,RLVECT_1:24
.= -(o-v) by RLVECT_1:def 8
.= v-o by RLVECT_1:33;
w = o + (w-o) by RLSUB_2:61
.= o + (-r)"*(v-o) by A6,A17,ANALOAF:6;
hence thesis by A11,A16,A9,A14,A15,A12,A8,PASCH:4;
end;
Lm1: for V being RealLinearSpace holds for u,v,w being VECTOR of V st u<>v & w
<>v & u,v // v,w ex r being Real st v-u = r*(w-v) & 0<r
proof
let V be RealLinearSpace;
let u,v,w be VECTOR of V;
assume u<>v & w<>v & u,v // v,w;
then consider a,b being Real such that
A1: a*(v-u)=b*(w-v) and
A2: 0<a and
A3: 0<b by ANALOAF:7;
take r = a"*b;
0<a" by A2,XREAL_1:122;
then
A4: 0*b < r by A3,XREAL_1:68;
v-u = 1*(v-u) by RLVECT_1:def 8
.= (a"*a)*(v-u) by A2,XCMPLX_0:def 7
.= a"*(b*(w-v)) by A1,RLVECT_1:def 7
.= r*(w-v) by RLVECT_1:def 7;
hence thesis by A4;
end;
theorem Th11:
for V being RealLinearSpace, OAS being OAffinSpace st OAS =
OASpace(V) holds OAS is satisfying_DES_1
proof
let V be RealLinearSpace,OAS be OAffinSpace such that
A1: OAS = OASpace(V);
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 such 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;
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
A11: not y,u '||' y,v & not y,u '||' y,w
proof
assume not thesis;
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;
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;
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 thesis by DIRAF:2;
end;
now
assume
A19: o=a1;
A20: 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;
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;
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;
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;
end;
hence thesis by A20,DIRAF:4;
end;
hence thesis by A10;
end;
hence thesis;
end;
theorem
for V being RealLinearSpace, OAS being OAffinSpace st OAS = OASpace(V)
holds OAS is satisfying_DES_1 & OAS is satisfying_DES by Th6,Th11;
Lm2: for V being RealLinearSpace holds for y,u,v being VECTOR of V st y,u '||'
y,v & y<>u & y<>v ex r being Real st u-y = r*(v-y) & r<>0
proof
let V be RealLinearSpace;
let y,u,v be VECTOR of V such that
A1: y,u '||' y,v and
A2: y<>u and
A3: y<>v;
y,u // y,v or y,u // v,y by A1,GEOMTRAP:def 1;
then consider a,b being Real such that
A4: a*(u-y) = b*(v-y) and
A5: a<>0 or b<>0 by ANALMETR:14;
A6: now
assume
A7: b=0;
then 0.V = a*(u-y) by A4,RLVECT_1:10;
then u-y = 0.V by A5,A7,RLVECT_1:11;
hence contradiction by A2,RLVECT_1:21;
end;
A8: now
assume
A9: a=0;
then 0.V = b*(v-y) by A4,RLVECT_1:10;
then v-y = 0.V by A5,A9,RLVECT_1:11;
hence contradiction by A3,RLVECT_1:21;
end;
then
A10: a"<>0 by XCMPLX_1:202;
take r=a"*b;
r*(v-y) = a"*(a*(u-y)) by A4,RLVECT_1:def 7
.= (a"*a)*(u-y) by RLVECT_1:def 7
.= 1*(u-y) by A8,XCMPLX_0:def 7
.= u-y by RLVECT_1:def 8;
hence thesis by A6,A10,XCMPLX_1:6;
end;
Lm3: for V being RealLinearSpace holds for u,v,y being VECTOR of V holds (u-y)
-(v-y) = u-v
proof
let V be RealLinearSpace;
let u,v,y be VECTOR of V;
thus (u-y)-(v-y) = u-((v-y)+y) by RLVECT_1:27
.= u-v by RLSUB_2:61;
end;
theorem Th13:
for V being RealLinearSpace, OAS being OAffinSpace st OAS =
OASpace(V) holds Lambda(OAS) is Pappian
proof
let V be RealLinearSpace, OAS be OAffinSpace such that
A1: OAS = OASpace(V);
set AS = Lambda(OAS);
for M,N being Subset of AS, o,a,b,c,a9,b9,c9 being Element
of AS st M is being_line & N is being_line & M<>N & o in M & o in N & o
<>a & o<>a9 & o<>b & o<>b9 & o<>c & o<>c9 & a in M & b in M & c in M & a9 in N
& b9 in N & c9 in N & a,b9 // b,a9 & b,c9 // c,b9 holds a,c9 // c,a9
proof
let M,N be Subset of AS, o,a,b,c,a9,b9,c9 be Element of AS
such that
A2: M is being_line and
A3: N is being_line and
A4: M<>N and
A5: o in M and
A6: o in N and
A7: o<>a and
A8: o<>a9 and
A9: o<>b and
o<>b9 and
A10: o<>c and
A11: o<>c9 and
A12: a in M and
A13: b in M and
A14: c in M and
A15: a9 in N and
A16: b9 in N and
A17: c9 in N and
A18: a,b9 // b,a9 and
A19: b,c9 // c,b9;
reconsider o1=o,a1=a,b1=b,c1=c,a19=a9,b19=b9,c19=c9 as Element of OAS by
Th1;
reconsider q=o1,u=a1,v=b1,w=c1,u9=a19,v9=b19,w9=c19 as VECTOR of V by A1
,Th3;
b1,c19 '||' c1,b19 by A19,DIRAF:38;
then
A20: v,w9 '||' w,v9 by A1,Th4;
A21: not q,v '||' q,w9 & not q,v '||' q,u9
proof
assume not thesis;
then o1,b1 '||' o1,c19 or o1,b1 '||' o1,a19 by A1,Th4;
then o,b // o,c9 or o,b // o,a9 by DIRAF:38;
then LIN o,b,c9 or LIN o,b,a9 by AFF_1:def 1;
then c9 in M or a9 in M by A2,A5,A9,A13,AFF_1:25;
hence contradiction by A2,A3,A4,A5,A6,A8,A11,A15,A17,AFF_1:18;
end;
LIN o,c,b by A2,A5,A13,A14,AFF_1:21;
then o,c // o,b by AFF_1:def 1;
then o1,c1 '||' o1,b1 by DIRAF:38;
then q,w '||' q,v by A1,Th4;
then consider r2 being Real such that
A22: w-q = r2*(v-q) and
A23: r2<>0 by A9,A10,Lm2;
A24: -r2<>0 by A23;
LIN o,a,b by A2,A5,A12,A13,AFF_1:21;
then o,a // o,b by AFF_1:def 1;
then o1,a1 '||' o1,b1 by DIRAF:38;
then q,u '||' q,v by A1,Th4;
then consider r1 being Real such that
A25: u-q = r1*(v-q) and
A26: r1<>0 by A7,A9,Lm2;
A27: (-r1)*(q-v) = r1*(-(q-v)) by RLVECT_1:24
.= u-q by A25,RLVECT_1:33;
LIN o,c9,b9 by A3,A6,A16,A17,AFF_1:21;
then o,c9 // o,b9 by AFF_1:def 1;
then o1,c19 '||' o1,b19 by DIRAF:38;
then
A28: q,w9 '||' q,v9 by A1,Th4;
(-r2)*(q-v) = r2*(-(q-v)) by RLVECT_1:24
.= w-q by A22,RLVECT_1:33;
then
A29: q-v = (-r2)"*(w-q) by A24,ANALOAF:5;
(-r2)" <>0 by A24,XCMPLX_1:202;
then v9 = q + (-((-r2)"))"*(w9-q) by A20,A29,A28,A21,Th10
.= q + (-(-(r2")))"*(w9-q) by XCMPLX_1:222
.= q+ r2*(w9-q);
then
A30: v9-q = r2*(w9-q) by RLSUB_2:61;
LIN o,a9,b9 by A3,A6,A15,A16,AFF_1:21;
then o,a9 // o,b9 by AFF_1:def 1;
then o1,a19 '||' o1,b19 by DIRAF:38;
then
A31: q,u9 '||' q,v9 by A1,Th4;
a1,b19 '||' b1,a19 by A18,DIRAF:38;
then b1,a19 '||' a1,b19 by DIRAF:22;
then
A32: v,u9 '||' u,v9 by A1,Th4;
r1"<>0 by A26,XCMPLX_1:202;
then
A33: r1"*r2<>0 by A23,XCMPLX_1:6;
set s=r1*(r2");
A34: u-q = r1*(r2"*(w-q)) by A25,A22,A23,ANALOAF:6
.= s*(w-q) by RLVECT_1:def 7;
-r1<>0 by A26;
then
A35: (-r1)" <>0 by XCMPLX_1:202;
-r1<>0 by A26;
then q-v = (-r1)"*(u-q) by A27,ANALOAF:6;
then v9 = q + (-((-r1)"))"*(u9-q) by A32,A35,A31,A21,Th10
.= q + (-(-(r1")))"*(u9-q) by XCMPLX_1:222
.= q+ r1*(u9-q);
then v9-q = r1*(u9-q) by RLSUB_2:61;
then u9-q = r1"*(r2*(w9-q)) by A26,A30,ANALOAF:6
.= (r1"*r2)*(w9-q) by RLVECT_1:def 7;
then
A36: w9-q = (r1"*r2)"*(u9-q) by A33,ANALOAF:6
.= ((r1")"*(r2"))*(u9-q) by XCMPLX_1:204
.= s*(u9-q);
1*(w9-u) = w9-u by RLVECT_1:def 8
.= s*(u9-q) - s*(w-q) by A36,A34,Lm3
.= s*((u9-q)-(w-q)) by RLVECT_1:34
.= s*(u9-w) by Lm3;
then u,w9 // w,u9 or u,w9 // u9,w by ANALMETR:14;
then u,w9 '||' w,u9 by GEOMTRAP:def 1;
then a1,c19 '||' c1,a19 by A1,Th4;
hence thesis by DIRAF:38;
end;
hence thesis by AFF_2:def 2;
end;
theorem Th14:
for V being RealLinearSpace, OAS being OAffinSpace st OAS =
OASpace(V) holds Lambda(OAS) is Desarguesian by Th9,Th11;
theorem Th15:
for AS being AffinSpace st AS is Desarguesian holds AS is Moufangian
proof
let AS be AffinSpace such that
A1: AS is Desarguesian;
now
let K be Subset of AS, o,a,b,c,a9,b9,c9 be Element of AS
such that
A2: K is being_line and
A3: o in K and
A4: c in K & c9 in K and
A5: not a in K and
A6: o<>c and
A7: a<>b and
A8: LIN o,a,a9 and
A9: LIN o,b,b9 and
A10: a,b // a9,b9 & a,c // a9,c9 and
A11: a,b // K;
set A=Line(o,a), P=Line(o,b);
A12: o in A by A3,A5,AFF_1:24;
A13: now
assume
A14: o=b;
b,a // K by A11,AFF_1:34;
hence contradiction by A2,A3,A5,A14,AFF_1:23;
end;
then
A15: b in P by AFF_1:24;
A16: a in A by A3,A5,AFF_1:24;
A17: A is being_line by A3,A5,AFF_1:24;
A18: A<>P
proof
assume A=P;
then a,b // A by A17,A16,A15,AFF_1:40,41;
hence contradiction by A3,A5,A7,A11,A12,A16,AFF_1:45,53;
end;
A19: P is being_line & o in P by A13,AFF_1:24;
then
A20: b9 in P by A9,A13,A15,AFF_1:25;
a9 in A by A3,A5,A8,A17,A12,A16,AFF_1:25;
hence b,c // b9,c9 by A1,A2,A3,A4,A5,A6,A10,A13,A17,A12,A16,A19,A15,A20,A18
,AFF_2:def 4;
end;
hence thesis by AFF_2:def 7;
end;
theorem Th16:
for V being RealLinearSpace, OAS being OAffinSpace st OAS =
OASpace(V) holds Lambda(OAS) is Moufangian
proof
let V be RealLinearSpace, OAS be OAffinSpace;
assume OAS = OASpace(V);
then (Lambda(OAS)) is Desarguesian by Th9,Th11;
hence thesis by Th15;
end;
theorem Th17:
for V being RealLinearSpace, OAS being OAffinSpace st OAS =
OASpace(V) holds Lambda(OAS) is translational
proof
let V be RealLinearSpace, OAS be OAffinSpace such that
A1: OAS = OASpace(V);
set AS = Lambda(OAS);
for A,P,C being Subset of AS, a,b,c,a9,b9,c9 being Element
of AS 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 AS, a,b,c,a9,b9,c9 be Element of AS
such 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;
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
assume
A18: a<>a9;
A19: not a1,a19,b1 are_collinear
proof
assume a1,a19,b1 are_collinear;
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;
end;
A20: not a1,a19,c1 are_collinear
proof
assume a1,a19,c1 are_collinear;
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;
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,w99=(u9+w)-u;
reconsider b199=v99,c199=w99 as Element of OAS by A1,Th3;
w99-v99 = (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 // v99,w99 by ANALOAF:15;
then
A23: v,w '||' v99,w99 by GEOMTRAP:def 1;
u,u9 // v,v99 by ANALOAF:16;
then u,u9 '||' v,v99 by GEOMTRAP:def 1;
then
A24: a1,a19 '||' b1,b199 by A1,Th4;
u,w // u9,w99 by ANALOAF:16;
then u,w '||' u9,w99 by GEOMTRAP:def 1;
then
A25: a1,c1 '||' a19,c199 by A1,Th4;
u,u9 // w,w99 by ANALOAF:16;
then u,u9 '||' w,w99 by GEOMTRAP:def 1;
then
A26: a1,a19 '||' c1,c199 by A1,Th4;
u,v // u9,v99 by ANALOAF:16;
then u,v '||' u9,v99 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 thesis by DIRAF:38;
end;
now
assume
A29: a=a9;
A30: 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;
then a in C by A8,A9,A12,A31,AFF_1:25;
hence contradiction by A3,A4,A14,AFF_1:45;
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;
then a in P by A6,A7,A11,A32,AFF_1:25;
hence contradiction by A2,A4,A13,AFF_1:45;
end;
hence thesis by A30,AFF_1:2;
end;
hence thesis by A17;
end;
hence thesis by AFF_2:def 11;
end;
theorem Th18:
for OAS being OAffinSpace holds Lambda(OAS) is Fanoian
proof
let OAS be OAffinSpace;
set AS = Lambda(OAS);
for a,b,c,d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c
holds a,b // a,c
proof
let a,b,c,d be Element of AS such that
A1: a,b // c,d and
A2: a,c // b,d and
A3: a,d // b,c;
reconsider a1=a,b1=b,c1=c,d1=d as Element of OAS by Th1;
set P = Line(a,d),Q = Line(b,c);
assume
A4: not a,b // a,c;
then
A5: a<>d by A1,AFF_1:4;
then
A6: P is being_line by AFF_1:def 3;
A7: not a1,b1,c1 are_collinear
proof
assume not thesis;
then a1,b1 '||' a1,c1 by DIRAF:def 5;
hence contradiction by A4,DIRAF:38;
end;
a1,b1 '||' c1,d1 & a1,c1 '||' b1,d1 by A1,A2,DIRAF:38;
then consider x1 being Element of OAS such that
A8: x1,a1,d1 are_collinear and
A9: x1,b1,c1 are_collinear by A7,PASCH:25;
reconsider x=x1 as Element of AS by Th1;
A10: d in P by AFF_1:15;
x1,a1 '||' x1,d1 by A8,DIRAF:def 5;
then x,a // x,d by DIRAF:38;
then LIN x,a,d by AFF_1:def 1;
then LIN a,d,x by AFF_1:6;
then
A11: x in P by AFF_1:def 2;
A12: a in P & b in Q by AFF_1:15;
x1,b1 '||' x1,c1 by A9,DIRAF:def 5;
then x,b // x,c by DIRAF:38;
then LIN x,b,c by AFF_1:def 1;
then LIN b,c,x by AFF_1:6;
then
A13: x in Q by AFF_1:def 2;
A14: c in Q by AFF_1:15;
A15: not LIN a,b,c by A4,AFF_1:def 1;
then
A16: b<>c by AFF_1:7;
then Q is being_line by AFF_1:def 3;
then P // Q by A3,A16,A5,A6,A10,A12,A14,AFF_1:38;
then P = Q by A11,A13,AFF_1:45;
hence contradiction by A15,A6,A12,A14,AFF_1:21;
end;
hence thesis;
end;
registration
cluster Pappian Desarguesian Moufangian translation for OAffinSpace;
existence
proof
consider V being RealLinearSpace such that
A1: ex u,v being VECTOR of V st
for a,b being Real st a*u + b*v = 0.V
holds a=0 & b=0 by FUNCSDOM:23;
reconsider X = OASpace(V) as OAffinSpace by A1,ANALOAF:26;
take X;
set AS = Lambda(X);
A2: AS is Moufangian & AS is translational by Th16,Th17;
AS is Pappian & AS is Desarguesian by Th9,Th11,Th13;
hence thesis by A2;
end;
end;
registration
cluster strict Fanoian Pappian Desarguesian Moufangian translational
for AffinPlane;
existence
proof
consider V being RealLinearSpace such that
A1: ex u,v being VECTOR of V st
(for a,b being Real st a*u + b*v = 0.V
holds a=0 & b=0) & for w being VECTOR of V
ex a,b being Real st w = a*u + b*v
by FUNCSDOM:23;
reconsider OAS = OASpace(V) as OAffinPlane by A1,ANALOAF:28;
take X = Lambda(OAS);
A2: X is Pappian by Th13;
then X is Moufangian by AFF_2:11,12;
hence thesis by A2,Th18,AFF_2:11,14;
end;
end;
registration
cluster strict Fanoian Pappian Desarguesian Moufangian translational
for AffinSpace;
existence
proof
consider V being RealLinearSpace such that
A1: ex u,v being VECTOR of V st for a,b being Real st a*u + b*v = 0.V
holds a=0 & b=0 by FUNCSDOM:23;
reconsider X = OASpace(V) as OAffinSpace by A1,ANALOAF:26;
take Lambda(X);
thus thesis by Th13,Th14,Th16,Th17,Th18;
end;
end;
registration
let OAS be OAffinSpace;
cluster Lambda(OAS) -> Fanoian;
correctness by Th18;
end;
registration
let OAS be Pappian OAffinSpace;
cluster Lambda(OAS) -> Pappian;
correctness by Def2;
end;
registration
let OAS be Desarguesian OAffinSpace;
cluster Lambda(OAS) -> Desarguesian;
correctness by Def3;
end;
registration
let OAS be Moufangian OAffinSpace;
cluster Lambda(OAS) -> Moufangian;
correctness by Def4;
end;
registration
let OAS be translation OAffinSpace;
cluster Lambda(OAS) -> translational;
correctness by Def5;
end;