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;