:: Fundamental Types of Metric Affine Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received April 17, 1991
:: Copyright (c) 1991-2019 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, BOOLE;
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;