:: Shear Theorems and Their Role in Affine Geometry
:: by Jolanta \'Swierzy\'nska and Bogdan \'Swierzy\'nski
::
:: Received April 19, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

definition
let X be AffinPlane;
attrX is satisfying_minor_Scherungssatz  means :Def1: :: CONMETR1:def 1
 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X 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;

:: deftheorem Def1 defines satisfying_minor_Scherungssatz CONMETR1:def_1_:_
 for X being AffinPlane holds
( X is satisfying_minor_Scherungssatz iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X 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 );

definition
let X be AffinPlane;
attrX is satisfying_major_Scherungssatz  means :Def2: :: CONMETR1:def 2
 for o, a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X 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;

:: deftheorem Def2 defines satisfying_major_Scherungssatz CONMETR1:def_2_:_
 for X being AffinPlane holds
( X is satisfying_major_Scherungssatz iff for o, a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X 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 );

definition
let X be AffinPlane;
attrX is satisfying_Scherungssatz  means :Def3: :: CONMETR1:def 3
 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X 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;

:: deftheorem Def3 defines satisfying_Scherungssatz CONMETR1:def_3_:_
 for X being AffinPlane holds
( X is satisfying_Scherungssatz iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X 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 );

definition
let X be AffinPlane;
attrX is satisfying_indirect_Scherungssatz  means :Def4: :: CONMETR1:def 4
 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X 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;

:: deftheorem Def4 defines satisfying_indirect_Scherungssatz CONMETR1:def_4_:_
 for X being AffinPlane holds
( X is satisfying_indirect_Scherungssatz iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X 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 );

definition
let X be AffinPlane;
attrX is satisfying_minor_indirect_Scherungssatz  means :Def5: :: CONMETR1:def 5
 for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X 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;

:: deftheorem Def5 defines satisfying_minor_indirect_Scherungssatz CONMETR1:def_5_:_
 for X being AffinPlane holds
( X is satisfying_minor_indirect_Scherungssatz iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X 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 );

definition
let X be AffinPlane;
attrX is satisfying_major_indirect_Scherungssatz  means :Def6: :: CONMETR1:def 6
 for o, a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X 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;

:: deftheorem Def6 defines satisfying_major_indirect_Scherungssatz CONMETR1:def_6_:_
 for X being AffinPlane holds
( X is satisfying_major_indirect_Scherungssatz iff for o, a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X 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 );

theorem Th1: :: CONMETR1:1
for X being AffinPlane holds
( X is satisfying_indirect_Scherungssatz iff ( X is satisfying_minor_indirect_Scherungssatz & X is satisfying_major_indirect_Scherungssatz ) )
proofend;

theorem Th2: :: CONMETR1:2
for X being AffinPlane holds
( X is satisfying_Scherungssatz iff ( X is satisfying_minor_Scherungssatz & X is satisfying_major_Scherungssatz ) )
proofend;

theorem Th3: :: CONMETR1:3
for X being AffinPlane st X is satisfying_minor_indirect_Scherungssatz holds
X is satisfying_minor_Scherungssatz
proofend;

theorem Th4: :: CONMETR1:4
for X being AffinPlane st X is satisfying_major_indirect_Scherungssatz holds
X is satisfying_major_Scherungssatz
proofend;

theorem :: CONMETR1:5
for X being AffinPlane st X is satisfying_indirect_Scherungssatz holds
X is satisfying_Scherungssatz
proofend;

theorem Th6: :: CONMETR1:6
for X being AffinPlane st X is translational holds
X is satisfying_minor_Scherungssatz
proofend;

theorem Th7: :: CONMETR1:7
for X being AffinPlane st X is Desarguesian holds
X is satisfying_major_Scherungssatz
proofend;

theorem :: CONMETR1:8
for X being AffinPlane holds
( X is Desarguesian iff X is satisfying_Scherungssatz )
proofend;

theorem Th9: :: CONMETR1:9
for X being AffinPlane holds
( X is satisfying_pap iff X is satisfying_minor_indirect_Scherungssatz )
proofend;

theorem Th10: :: CONMETR1:10
for X being AffinPlane holds
( X is Pappian iff X is satisfying_major_indirect_Scherungssatz )
proofend;

theorem :: CONMETR1:11
for X being AffinPlane holds
( X is satisfying_PPAP iff X is satisfying_indirect_Scherungssatz )
proofend;

theorem :: CONMETR1:12
for X being AffinPlane st X is satisfying_major_indirect_Scherungssatz holds
X is satisfying_minor_indirect_Scherungssatz
proofend;

theorem :: CONMETR1:13
for X being OrtAfPl holds
( Af X is satisfying_Scherungssatz iff X is satisfying_SCH )
proofend;

theorem :: CONMETR1:14
for X being OrtAfPl holds
( X is satisfying_TDES iff Af X is Moufangian )
proofend;

theorem :: CONMETR1:15
for X being OrtAfPl holds
( Af X is translational iff X is satisfying_des )
proofend;

theorem :: CONMETR1:16
for X being OrtAfPl holds
( X is satisfying_PAP iff Af X is Pappian )
proofend;

theorem :: CONMETR1:17
for X being OrtAfPl holds
( X is satisfying_DES iff Af X is Desarguesian )
proofend;