:: Fanoian, Pappian and Desarguesian Affine Spaces
:: by Krzysztof Pra\.zmowski
::
:: Received November 16, 1990
:: Copyright (c) 1990-2016 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, BOOLE;
begin
registration
let OAS be OAffinSpace;
cluster Lambda(OAS) -> AffinSpace-like non trivial;
end;
registration
let OAS be OAffinPlane;
cluster Lambda(OAS) -> 2-dimensional;
end;
theorem :: PAPDESAF:1
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));
theorem :: PAPDESAF:2
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;
theorem :: PAPDESAF:3
for V being RealLinearSpace, x being set holds (x is Element of
OASpace(V) iff x is VECTOR of V);
theorem :: PAPDESAF:4
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);
theorem :: PAPDESAF:5
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;
definition
let AS be AffinSpace;
redefine attr AS is Fanoian means
:: PAPDESAF:def 1
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;
end;
definition
let IT be OAffinSpace;
attr IT is Pappian means
:: PAPDESAF:def 2
Lambda(IT) is Pappian;
attr IT is Desarguesian means
:: PAPDESAF:def 3
Lambda(IT) is Desarguesian;
attr IT is Moufangian means
:: PAPDESAF:def 4
Lambda(IT) is Moufangian;
attr IT is translation means
:: PAPDESAF:def 5
Lambda(IT) is translational;
end;
definition
let OAS be OAffinSpace;
attr OAS is satisfying_DES means
:: PAPDESAF:def 6
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
:: PAPDESAF:def 7
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 :: PAPDESAF:6
for OAS being OAffinSpace st OAS is satisfying_DES_1 holds OAS
is satisfying_DES;
theorem :: PAPDESAF:7
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;
theorem :: PAPDESAF:8
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;
theorem :: PAPDESAF:9
for OAP being OAffinSpace st OAP is satisfying_DES_1 holds
Lambda(OAP) is Desarguesian;
theorem :: PAPDESAF:10
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);
theorem :: PAPDESAF:11
for V being RealLinearSpace, OAS being OAffinSpace st OAS =
OASpace(V) holds OAS is satisfying_DES_1;
theorem :: PAPDESAF:12
for V being RealLinearSpace, OAS being OAffinSpace st OAS = OASpace(V)
holds OAS is satisfying_DES_1 & OAS is satisfying_DES;
theorem :: PAPDESAF:13
for V being RealLinearSpace, OAS being OAffinSpace st OAS =
OASpace(V) holds Lambda(OAS) is Pappian;
theorem :: PAPDESAF:14
for V being RealLinearSpace, OAS being OAffinSpace st OAS =
OASpace(V) holds Lambda(OAS) is Desarguesian;
theorem :: PAPDESAF:15
for AS being AffinSpace st AS is Desarguesian holds AS is Moufangian;
theorem :: PAPDESAF:16
for V being RealLinearSpace, OAS being OAffinSpace st OAS =
OASpace(V) holds Lambda(OAS) is Moufangian;
theorem :: PAPDESAF:17
for V being RealLinearSpace, OAS being OAffinSpace st OAS =
OASpace(V) holds Lambda(OAS) is translational;
theorem :: PAPDESAF:18
for OAS being OAffinSpace holds Lambda(OAS) is Fanoian;
registration
cluster Pappian Desarguesian Moufangian translation for OAffinSpace;
end;
registration
cluster strict Fanoian Pappian Desarguesian Moufangian translational
for AffinPlane;
end;
registration
cluster strict Fanoian Pappian Desarguesian Moufangian translational
for AffinSpace;
end;
registration
let OAS be OAffinSpace;
cluster Lambda(OAS) -> Fanoian;
end;
registration
let OAS be Pappian OAffinSpace;
cluster Lambda(OAS) -> Pappian;
end;
registration
let OAS be Desarguesian OAffinSpace;
cluster Lambda(OAS) -> Desarguesian;
end;
registration
let OAS be Moufangian OAffinSpace;
cluster Lambda(OAS) -> Moufangian;
end;
registration
let OAS be translation OAffinSpace;
cluster Lambda(OAS) -> translational;
end;