:: Fanoian, Pappian and Desarguesian Affine Spaces :: by Krzysztof Pra\.zmowski :: :: Received November 16, 1990 :: Copyright (c) 1990-2021 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; 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;