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