:: Metric-Affine Configurations in Metric Affine Planes - Part II
:: by Jolanta \'Swierzy\'nska and Bogdan \'Swierzy\'nski
::
:: Received October 31, 1990
:: Copyright (c) 1990-2017 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, ANALOAF, AFF_1, DIRAF, INCSP_1,
AFF_2, CONAFFM, STRUCT_0, CONMETR;
notations SUBSET_1, STRUCT_0, ANALOAF, AFF_1, ANALMETR, AFF_2, CONAFFM;
constructors AFF_1, AFF_2, CONAFFM;
registrations ANALMETR;
requirements SUBSET;
begin
reserve X for OrtAfPl;
reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1,c2,c3,d,d1,d2,d3,d4,e1,e2 for
Element of X;
reserve a29,a39,b29,x9 for Element of the AffinStruct of X;
reserve A,K,M,N for Subset of X;
reserve A9,K9 for Subset of the AffinStruct of X;
definition
let X;
attr X is satisfying_OPAP means
:: CONMETR:def 1
for o,a1,a2,a3,b1,b2,b3,M,N st o in M
& a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2
in M & not a3 in N & M _|_ N & o<>a1 & o<>a2 & o<>a3 & o<>b1 & o<>b2 & o<>b3 &
a3,b2 // a2,b1 & a3,b3 // a1,b1 holds a1,b2 // a2,b3;
attr X is satisfying_PAP means
:: CONMETR:def 2
for o,a1,a2,a3,b1,b2,b3,M,N st M is
being_line & N is being_line & o in M & a1 in M & a2 in M & a3 in M & o in N &
b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o<>a1 & o<>a2 & o<>a3
& o<>b1 & o<>b2 & o<>b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds a1,b2 // a2,b3;
attr X is satisfying_MH1 means
:: CONMETR:def 3
for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M
_|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N &
b4 in N & not a2 in M & not a4 in M & a1,a2 _|_ b1,b2 & a2,a3 _|_ b2,b3 & a3,a4
_|_ b3,b4 holds a1,a4 _|_ b1,b4;
attr X is satisfying_MH2 means
:: CONMETR:def 4
for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M
_|_ N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N &
b3 in N & not a2 in M & not a4 in M & a1,a2 _|_ b1,b2 & a2,a3 _|_ b2,b3 & a3,a4
_|_ b3,b4 holds a1,a4 _|_ b1,b4;
attr X is satisfying_TDES means
:: CONMETR:def 5
for o,a,a1,b,b1,c,c1 st o<>a & o<>a1
& o<>b & o<>b1 & o<>c & o<>c1 & not LIN b,b1,a & not LIN b,b1,c & LIN o,a,a1 &
LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,b // o,c & b,c // b1,c1 holds a,c //
a1,c1;
attr X is satisfying_SCH means
:: CONMETR:def 6
for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M is
being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N
& a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not
b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,
b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4;
attr X is satisfying_OSCH means
:: CONMETR:def 7
for a1,a2,a3,a4,b1,b2,b3,b4,M,N st M
_|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N &
b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N &
not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,
a4 // b1,b4 holds a3,a4 // b3,b4;
attr X is satisfying_des means
:: CONMETR:def 8
for a,a1,b,b1,c,c1 st not LIN a,a1,b &
not LIN a,a1,c & a,a1 // b,b1 & a,a1 // c,c1 & a,b // a1,b1 & a,c // a1,c1
holds b,c // b1,c1;
end;
theorem :: CONMETR:1
ex a,b,c st LIN a,b,c & a<>b & b<>c & c <>a;
theorem :: CONMETR:2
for a,b ex c st LIN a,b,c & a<>c & b<>c;
theorem :: CONMETR:3
for A,a st A is being_line ex K st a in K & A _|_ K;
theorem :: CONMETR:4
A is being_line & a in A & b in A & c in A implies LIN a,b,c;
theorem :: CONMETR:5
A is being_line & M is being_line & a in A & b in A & a in M & b
in M implies a=b or A=M;
theorem :: CONMETR:6
for a,b,c,d,M holds for M9 being Subset of the AffinStruct of X, c9,d9 being
Element of the AffinStruct of X
st c =c9 & d=d9 & M=M9 & a in M & b in M & c9,d9 // M9 holds c,d // a,b;
theorem :: CONMETR:7
X is satisfying_TDES implies the AffinStruct of X is Moufangian;
theorem :: CONMETR:8
the AffinStruct of X is translational implies X is satisfying_des;
theorem :: CONMETR:9
X is satisfying_MH1 implies X is satisfying_OSCH;
theorem :: CONMETR:10
X is satisfying_MH2 implies X is satisfying_OSCH;
theorem :: CONMETR:11
X is satisfying_AH implies X is satisfying_TDES;
theorem :: CONMETR:12
X is satisfying_OSCH & X is satisfying_TDES implies X is satisfying_SCH;
theorem :: CONMETR:13
X is satisfying_OPAP & X is satisfying_DES implies X is satisfying_PAP;
theorem :: CONMETR:14
X is satisfying_MH1 & X is satisfying_MH2 implies X is satisfying_OPAP;
theorem :: CONMETR:15
X is satisfying_3H implies X is satisfying_OPAP;