Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

### Fundamental Types of Metric Affine Spaces

**by****Henryk Oryszczyszyn, and****Krzysztof Prazmowski**- Received April 17, 1991
- MML identifier: EUCLMETR

- [ Mizar article, MML identifier index ]

environ vocabulary ANALMETR, SYMSP_1, AFF_2, VECTSP_1, TRANSGEO, ANALOAF, DIRAF, AFF_1, INCSP_1, CONAFFM, CONMETR, PAPDESAF, RLVECT_1, ARYTM_1, FUNCT_3, RELAT_1, PARSP_1, EUCLMETR; notation SUBSET_1, STRUCT_0, REAL_1, RLVECT_1, ANALOAF, DIRAF, AFF_1, ANALMETR, GEOMTRAP, PAPDESAF, CONMETR, CONAFFM; constructors AFF_2, TRANSLAC, REAL_1, AFF_1, GEOMTRAP, CONMETR, CONAFFM, MEMBERED, XBOOLE_0; clusters ANALMETR, PAPDESAF, MEMBERED, ZFMISC_1, XBOOLE_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 the carrier 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 Af(IT) is Pappian; end; definition let IT be OrtAfSp; attr IT is Desarguesian means :: EUCLMETR:def 3 Af(IT) is Desarguesian; end; definition let IT be OrtAfSp; attr IT is Fanoian means :: EUCLMETR:def 4 Af(IT) is Fanoian; end; definition let IT be OrtAfSp; attr IT is Moufangian means :: EUCLMETR:def 5 Af(IT) is Moufangian; end; definition let IT be OrtAfSp; attr IT is translation means :: EUCLMETR:def 6 Af(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 or b,a _|_ 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 3H_holds_in MS; theorem :: EUCLMETR:9 MS is Homogeneous iff ODES_holds_in MS; theorem :: EUCLMETR:10 MS is Pappian iff PAP_holds_in MS; theorem :: EUCLMETR:11 MS is Desarguesian iff DES_holds_in MS; theorem :: EUCLMETR:12 MS is Moufangian iff TDES_holds_in MS; theorem :: EUCLMETR:13 MS is translation iff des_holds_in MS; 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 & o<>c1 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; canceled; theorem :: EUCLMETR:21 Gen w,y & MS = AMSpace(V,w,y) implies LIN_holds_in MS; theorem :: EUCLMETR:22 for o,a,a1,b,b1,c,c1 being Element of MS 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 & o=a1 holds b,c _|_ b1,c1; theorem :: EUCLMETR:23 Gen w,y & MS = AMSpace(V,w,y) implies MS is Homogeneous; definition cluster Euclidean Pappian Desarguesian Homogeneous translation Fanoian Moufangian OrtAfPl; end; definition cluster Euclidean Pappian Desarguesian Homogeneous translation Fanoian Moufangian OrtAfSp; end; theorem :: EUCLMETR:24 Gen w,y & MS=AMSpace(V,w,y) implies MS is Euclidean Pappian Desarguesian Homogeneous translation Fanoian Moufangian OrtAfPl; definition let MS be Pappian OrtAfPl; cluster Af(MS) -> Pappian; end; definition let MS be Desarguesian OrtAfPl; cluster Af(MS) -> Desarguesian; end; definition let MS be Moufangian OrtAfPl; cluster Af(MS) -> Moufangian; end; definition let MS be translation OrtAfPl; cluster Af(MS) -> translational; end; definition let MS be Fanoian OrtAfPl; cluster Af(MS) -> Fanoian; end; definition let MS be Homogeneous OrtAfPl; cluster Af(MS) -> Desarguesian; end; definition let MS be Euclidean Desarguesian OrtAfPl; cluster Af(MS) -> Pappian; end; definition let MS be Pappian OrtAfSp; cluster Af(MS) -> Pappian; end; definition let MS be Desarguesian OrtAfSp; cluster Af(MS) -> Desarguesian; end; definition let MS be Moufangian OrtAfSp; cluster Af(MS) -> Moufangian; end; definition let MS be translation OrtAfSp; cluster Af(MS) -> translational; end; definition let MS be Fanoian OrtAfSp; cluster Af(MS) -> Fanoian; end;

Back to top