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