Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### Shear Theorems and Their Role in Affine Geometry

by
Jolanta Swierzynska, and
Bogdan Swierzynski

MML identifier: CONMETR1
[ Mizar article, MML identifier index ]

```environ

vocabulary DIRAF, ANALOAF, AFF_1, AFF_2, ANALMETR, CONMETR, CONAFFM, CONMETR1;
notation SUBSET_1, STRUCT_0, ANALOAF, DIRAF, AFF_1, ANALMETR, AFF_2, CONAFFM,
CONMETR;
constructors AFF_1, AFF_2, CONAFFM, CONMETR, XBOOLE_0;
clusters ANALMETR, ZFMISC_1, XBOOLE_0;
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;
synonym X satisfies_minor_SCH;
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_line &
N is_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;
synonym X satisfies_major_SCH;
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_line &
N is_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;
synonym X satisfies_SCH;
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_line &
N is_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;
synonym X satisfies_SCH*;
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;
synonym X satisfies_minor_SCH*;
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_line & N is_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;
synonym X satisfies_major_SCH*;
end;

theorem :: CONMETR1:1
X satisfies_SCH* iff (X satisfies_minor_SCH* & X satisfies_major_SCH*);

theorem :: CONMETR1:2
X satisfies_SCH iff (X satisfies_minor_SCH & X satisfies_major_SCH);

theorem :: CONMETR1:3
X satisfies_minor_SCH* implies X satisfies_minor_SCH;

theorem :: CONMETR1:4
X satisfies_major_SCH* implies X satisfies_major_SCH;

theorem :: CONMETR1:5
X satisfies_SCH* implies X satisfies_SCH;

theorem :: CONMETR1:6
X satisfies_des implies X satisfies_minor_SCH;

theorem :: CONMETR1:7
X satisfies_DES implies X satisfies_major_SCH;

theorem :: CONMETR1:8
X satisfies_DES iff X satisfies_SCH;

theorem :: CONMETR1:9
X satisfies_pap iff X satisfies_minor_SCH*;

theorem :: CONMETR1:10
X satisfies_PAP iff X satisfies_major_SCH*;

theorem :: CONMETR1:11
X satisfies_PPAP iff X satisfies_SCH*;

theorem :: CONMETR1:12
X satisfies_major_SCH* implies X satisfies_minor_SCH*;

reserve X for OrtAfPl;
reserve o',a',a1',a2',a3',a4',b',b1',b2',b3',b4',c',c1'
for Element of X;
reserve o,a,a1,a2,a3,a4,b,b1,b2,b3,b4,c,c1
for Element of Af(X);
reserve M',N' for Subset of X;
reserve A,M,N for Subset of Af(X);

theorem :: CONMETR1:13
Af(X) satisfies_SCH iff SCH_holds_in X;

theorem :: CONMETR1:14
TDES_holds_in X iff Af(X) satisfies_TDES;

theorem :: CONMETR1:15
Af(X) satisfies_des iff des_holds_in X;

theorem :: CONMETR1:16
PAP_holds_in X iff Af(X) satisfies_PAP;

theorem :: CONMETR1:17
DES_holds_in X iff Af(X) satisfies_DES;
```