:: Shear Theorems and Their Role in Affine Geometry :: by Jolanta \'Swierzy\'nska and Bogdan \'Swierzy\'nski :: :: Received April 19, 1991 :: Copyright (c) 1991-2018 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;