:: Fundamental Types of Metric Affine Spaces :: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski :: :: Received April 17, 1991 :: Copyright (c) 1991-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 ANALMETR, SUBSET_1, SYMSP_1, AFF_2, VECTSP_1, TRANSGEO, ANALOAF, DIRAF, STRUCT_0, AFF_1, INCSP_1, CONAFFM, CONMETR, RLVECT_1, ARYTM_1, ARYTM_3, REAL_1, RELAT_1, CARD_1, MCART_1, SUPINF_2, PARSP_1, EUCLMETR; notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, STRUCT_0, REAL_1, RLVECT_1, ANALOAF, DIRAF, AFF_1, AFF_2, ANALMETR, GEOMTRAP, PAPDESAF, CONMETR, CONAFFM; constructors REAL_1, AFF_1, AFF_2, TRANSLAC, GEOMTRAP, CONAFFM, CONMETR; registrations ANALMETR, PAPDESAF, ORDINAL1, XREAL_0, STRUCT_0; requirements NUMERALS, SUBSET, ARITHM; begin definition let IT be OrtAfSp; attr IT is Euclidean means :: EUCLMETR:def 1 for a,b,c,d being Element of IT st a,b _|_ c,d & b,c _|_ a,d holds b,d _|_ a,c; end; definition let IT be OrtAfSp; attr IT is Pappian means :: EUCLMETR:def 2 the AffinStruct of IT is Pappian; end; definition let IT be OrtAfSp; attr IT is Desarguesian means :: EUCLMETR:def 3 the AffinStruct of IT is Desarguesian; end; definition let IT be OrtAfSp; attr IT is Fanoian means :: EUCLMETR:def 4 the AffinStruct of IT is Fanoian; end; definition let IT be OrtAfSp; attr IT is Moufangian means :: EUCLMETR:def 5 the AffinStruct of IT is Moufangian; end; definition let IT be OrtAfSp; attr IT is translation means :: EUCLMETR:def 6 the AffinStruct of IT is translational; end; definition let IT be OrtAfSp; attr IT is Homogeneous means :: EUCLMETR:def 7 for o,a,a1,b,b1,c,c1 being Element of IT st o,a _|_ o,a1 & o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b holds b,c _|_ b1,c1; end; reserve MS for OrtAfPl; reserve MP for OrtAfSp; theorem :: EUCLMETR:1 for a,b,c being Element of MP st not LIN a,b,c holds a<>b & b<>c & a<>c; theorem :: EUCLMETR:2 for a,b,c,d being Element of MS, K being Subset of the carrier of MS st a,b _|_ K & c,d _|_ K holds a,b // c,d & a,b // d,c; theorem :: EUCLMETR:3 for a,b being Element of MS, A,K being Subset of the carrier of MS st a<>b & (a,b _|_ K or b,a _|_ K) & a,b _|_ A holds K // A; theorem :: EUCLMETR:4 for x,y,z being Element of MP st LIN x,y,z holds LIN x,z,y & LIN y,x,z & LIN y,z,x & LIN z,x,y & LIN z,y,x; theorem :: EUCLMETR:5 for a,b,c being Element of MS st not LIN a,b,c ex d being Element of MS st d,a _|_ b,c & d,b _|_ a,c; theorem :: EUCLMETR:6 for a,b,c,d1,d2 being Element of MS st not LIN a,b,c & d1,a _|_ b ,c & d1,b _|_ a,c & d2,a _|_ b,c & d2,b _|_ a,c holds d1=d2; theorem :: EUCLMETR:7 for a,b,c,d being Element of MS st a,b _|_ c,d & b,c _|_ a,d & LIN a,b,c holds (a=c or a=b or b=c); theorem :: EUCLMETR:8 MS is Euclidean iff MS is satisfying_3H; theorem :: EUCLMETR:9 MS is Homogeneous iff MS is satisfying_ODES; theorem :: EUCLMETR:10 MS is Pappian iff MS is satisfying_PAP; theorem :: EUCLMETR:11 MS is Desarguesian iff MS is satisfying_DES; theorem :: EUCLMETR:12 MS is Moufangian iff MS is satisfying_TDES; theorem :: EUCLMETR:13 MS is translation iff MS is satisfying_des; theorem :: EUCLMETR:14 MS is Homogeneous implies MS is Desarguesian; theorem :: EUCLMETR:15 MS is Euclidean Desarguesian implies MS is Pappian; reserve V for RealLinearSpace; reserve w,y,u,v for VECTOR of V; theorem :: EUCLMETR:16 for o,c,c1,a,a1,a2 being Element of MS st not LIN o,c,a & o<>c1 & o,c _|_ o,c1 & o,a _|_ o,a1 & o,a _|_ o,a2 & c,a _|_ c1,a1 & c,a _|_ c1,a2 holds a1=a2; theorem :: EUCLMETR:17 for o,c,c1,a being Element of MS st not LIN o,c,a ex a1 being Element of MS st o,a _|_ o,a1 & c,a _|_ c1,a1; theorem :: EUCLMETR:18 for a,b being Real st Gen w,y & 0.V<>u & 0.V<>v & u,v are_Ort_wrt w,y & u=a*w+b*y ex c being Real st c <>0 & v=(c*b)*w+(-c*a)*y; theorem :: EUCLMETR:19 Gen w,y & 0.V<>u & 0.V<>v & u,v are_Ort_wrt w,y implies ex c being Real st for a,b being Real holds a*w+b*y,(c*b)*w+(-c*a)*y are_Ort_wrt w,y & (a*w+b*y)-u,((c*b)*w+(-c*a)*y)-v are_Ort_wrt w,y; theorem :: EUCLMETR:20 Gen w,y & MS = AMSpace(V,w,y) implies MS is satisfying_LIN; theorem :: EUCLMETR:21 for o,a,a1,b,b1,c,c1 being Element of MS st o,b _|_ o,b1 & o,c _|_ o,c1 & a,b _|_ a1,b1 & a,c _|_ a1,c1 & not o,c // o,a & not o,a // o,b & o= a1 holds b,c _|_ b1,c1; theorem :: EUCLMETR:22 Gen w,y & MS = AMSpace(V,w,y) implies MS is Homogeneous; registration cluster Euclidean Pappian Desarguesian Homogeneous translation Fanoian Moufangian for OrtAfPl; end; registration cluster Euclidean Pappian Desarguesian Homogeneous translation Fanoian Moufangian for OrtAfSp; end; theorem :: EUCLMETR:23 Gen w,y & MS=AMSpace(V,w,y) implies MS is Euclidean Pappian Desarguesian Homogeneous translation Fanoian Moufangian OrtAfPl; registration let MS be Pappian OrtAfPl; cluster the AffinStruct of MS -> Pappian; end; registration let MS be Desarguesian OrtAfPl; cluster the AffinStruct of MS -> Desarguesian; end; registration let MS be Moufangian OrtAfPl; cluster the AffinStruct of MS -> Moufangian; end; registration let MS be translation OrtAfPl; cluster the AffinStruct of MS -> translational; end; registration let MS be Fanoian OrtAfPl; cluster the AffinStruct of MS -> Fanoian; end; registration let MS be Homogeneous OrtAfPl; cluster the AffinStruct of MS -> Desarguesian; end; registration let MS be Euclidean Desarguesian OrtAfPl; cluster the AffinStruct of MS -> Pappian; end; registration let MS be Pappian OrtAfSp; cluster the AffinStruct of MS -> Pappian; end; registration let MS be Desarguesian OrtAfSp; cluster the AffinStruct of MS -> Desarguesian; end; registration let MS be Moufangian OrtAfSp; cluster the AffinStruct of MS -> Moufangian; end; registration let MS be translation OrtAfSp; cluster the AffinStruct of MS -> translational; end; registration let MS be Fanoian OrtAfSp; cluster the AffinStruct of MS -> Fanoian; end;