:: 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


definition
let X be AffinPlane;
attr X is satisfying_minor_Scherungssatz means :: 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 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;
attr X is satisfying_major_Scherungssatz means :: 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 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;
attr X is satisfying_Scherungssatz means :: 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 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;
attr X is satisfying_indirect_Scherungssatz means :: 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 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;
attr X is satisfying_minor_indirect_Scherungssatz means :: 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 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;
attr X is satisfying_major_indirect_Scherungssatz means :: 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 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 ) )
proof end;

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

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

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

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

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

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

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

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

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

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

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

theorem :: CONMETR1:13
for X being OrtAfPl holds
( AffinStruct(# the U1 of X, the CONGR of X #) is satisfying_Scherungssatz iff X is satisfying_SCH )
proof end;

theorem :: CONMETR1:14
for X being OrtAfPl holds
( X is satisfying_TDES iff AffinStruct(# the U1 of X, the CONGR of X #) is Moufangian )
proof end;

theorem :: CONMETR1:15
for X being OrtAfPl holds
( AffinStruct(# the U1 of X, the CONGR of X #) is translational iff X is satisfying_des )
proof end;

theorem :: CONMETR1:16
for X being OrtAfPl holds
( X is satisfying_PAP iff AffinStruct(# the U1 of X, the CONGR of X #) is Pappian )
proof end;

theorem :: CONMETR1:17
for X being OrtAfPl holds
( X is satisfying_DES iff AffinStruct(# the U1 of X, the CONGR of X #) is Desarguesian )
proof end;