:: Shear Theorems and Their Role in Affine Geometry
:: by Jolanta \'Swierzy\'nska and Bogdan \'Swierzy\'nski
::
:: Received April 19, 1991
:: Copyright (c) 1991-2016 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 DIRAF, SUBSET_1, ANALOAF, AFF_1, AFF_2, ANALMETR, CONMETR,
CONAFFM, CONMETR1;
notations STRUCT_0, ANALOAF, DIRAF, AFF_1, ANALMETR, AFF_2, CONAFFM, CONMETR;
constructors AFF_1, AFF_2, CONAFFM, CONMETR;
registrations STRUCT_0, ANALMETR;
requirements SUBSET;
begin
reserve X for AffinPlane;
reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1,c2,d,d1,d2, d3,d4,d5,e1,e2,x,y,z
for Element of X;
reserve Y,Z,M,N,A,K,C for Subset of X;
definition
let X;
attr X is satisfying_minor_Scherungssatz means
:: CONMETR1:def 1
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;
end;
definition
let X;
attr X is satisfying_major_Scherungssatz means
:: CONMETR1:def 2
for o,a1,a2,a3,a4,b1,
b2,b3,b4,M,N st M is being_line & N is being_line & o in M & o in 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;
end;
definition
let X;
attr X is satisfying_Scherungssatz means
:: CONMETR1:def 3
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;
end;
definition
let X;
attr X is satisfying_indirect_Scherungssatz means
:: CONMETR1:def 4
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 & b2 in M
& b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a4 in M & not a2 in M &
not b1 in M & not b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in
N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4;
end;
definition
let X;
attr X is satisfying_minor_indirect_Scherungssatz means
:: CONMETR1:def 5
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 a4 in M & not a2 in M & not b1 in M & not
b3 in M & not a1 in N & not a3 in N & not b2 in N & not b4 in N & a3,a2 // b3,
b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds a3,a4 // b3,b4;
end;
definition
let X;
attr X is satisfying_major_indirect_Scherungssatz means
:: CONMETR1:def 6
for o,a1,a2,
a3,a4,b1,b2,b3,b4,M,N st M is being_line & N is being_line & o in M & o in 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 a4 in M & not a2 in M & not b1 in M & not b3 in M & not a1 in N & not a3 in
N & not b2 in N & not b4 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,
b4 holds a3,a4 // b3,b4;
end;
theorem :: CONMETR1:1
X is satisfying_indirect_Scherungssatz iff X is
satisfying_minor_indirect_Scherungssatz & X is
satisfying_major_indirect_Scherungssatz;
theorem :: CONMETR1:2
X is satisfying_Scherungssatz iff X is
satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz;
theorem :: CONMETR1:3
X is satisfying_minor_indirect_Scherungssatz implies X is
satisfying_minor_Scherungssatz;
theorem :: CONMETR1:4
X is satisfying_major_indirect_Scherungssatz implies X is
satisfying_major_Scherungssatz;
theorem :: CONMETR1:5
X is satisfying_indirect_Scherungssatz implies X is satisfying_Scherungssatz;
theorem :: CONMETR1:6
X is translational implies X is satisfying_minor_Scherungssatz;
theorem :: CONMETR1:7
X is Desarguesian implies X is satisfying_major_Scherungssatz;
theorem :: CONMETR1:8
X is Desarguesian iff X is satisfying_Scherungssatz;
theorem :: CONMETR1:9
X is satisfying_pap iff X is satisfying_minor_indirect_Scherungssatz;
theorem :: CONMETR1:10
X is Pappian iff X is satisfying_major_indirect_Scherungssatz;
theorem :: CONMETR1:11
X is satisfying_PPAP iff X is satisfying_indirect_Scherungssatz;
theorem :: CONMETR1:12
X is satisfying_major_indirect_Scherungssatz implies X is
satisfying_minor_indirect_Scherungssatz;
reserve X for OrtAfPl;
reserve o9,a9,a19,a29,a39,a49,b9,b19,b29,b39,b49,c9,c19 for Element of X;
reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1 for Element of the AffinStruct of X;
reserve M9,N9 for Subset of X;
reserve A,M,N for Subset of the AffinStruct of X;
theorem :: CONMETR1:13
the AffinStruct of X is satisfying_Scherungssatz iff X is satisfying_SCH;
theorem :: CONMETR1:14
X is satisfying_TDES iff the AffinStruct of X is Moufangian;
theorem :: CONMETR1:15
the AffinStruct of X is translational iff X is satisfying_des;
theorem :: CONMETR1:16
X is satisfying_PAP iff the AffinStruct of X is Pappian;
theorem :: CONMETR1:17
X is satisfying_DES iff the AffinStruct of X is Desarguesian;