The abstract of the Mizar article:

Homotheties and Shears in Affine Planes

by

Henryk Oryszczyszyn, and

Krzysztof Prazmowski

Received September 21, 1990

MML identifier: HOMOTHET

[ Mizar article, MML identifier index ]

environ

 vocabulary DIRAF, FUNCT_2, AFF_2, ANALOAF, INCSP_1, AFF_1, TRANSGEO, FUNCT_1,
      RELAT_1, HOMOTHET;
 notation TARSKI, PARTFUN1, FUNCT_2, STRUCT_0, ANALOAF, DIRAF, AFF_1, AFF_2,
      TRANSGEO;
 constructors AFF_1, AFF_2, TRANSGEO, PARTFUN1, XBOOLE_0;
 clusters STRUCT_0, ZFMISC_1, PARTFUN1, FUNCT_2, FUNCT_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

reserve AFP for AffinPlane;

reserve a,a',b,b',c,c',d,d',o,p,p',q,q',r,s,t,x,y,z
                        for Element of AFP;

reserve A,A',C,D,P,B',M,N,K for Subset of AFP;

reserve f for Permutation of the carrier of AFP;

theorem :: HOMOTHET:1
 not LIN o,a,p & LIN o,a,b & LIN o,a,x & LIN o,a,y & LIN o,p,p' &
        LIN o,p,q & LIN o,p,q' & p<>q & a<>x & o<>q & o<>x &
        a,p // b,p' & a,q // b,q' & x,p // y,p' & AFP satisfies_DES
                                            implies x,q // y,q';

theorem :: HOMOTHET:2
 (for o,a,b st o<>a & o<>b & LIN o,a,b
                  ex f st f is_Dil & f.o=o & f.a=b) implies
                                             AFP satisfies_DES;

theorem :: HOMOTHET:3
 AFP satisfies_DES implies (for o,a,b st o<>a & o<>b & LIN o,a,b ex f st
                                      f is_Dil & f.o=o & f.a=b);

theorem :: HOMOTHET:4
   AFP satisfies_DES iff (for o,a,b st o<>a & o<>b & LIN o,a,b ex f st
                                      f is_Dil & f.o=o & f.a=b);

definition let AFP,f,K;
 pred f is_Sc K means
:: HOMOTHET:def 1
   f is_Col & K is_line & (for x st x in K holds f.x = x) &
    (for x holds x,f.x // K);
 end;

theorem :: HOMOTHET:5
 f is_Sc K & f.p=p & not p in K implies f=id the carrier of AFP;

theorem :: HOMOTHET:6
 (for a,b,K st a,b // K & not a in K ex f st
                               f is_Sc K & f.a=b) implies AFP satisfies_TDES;

theorem :: HOMOTHET:7
 K // M & p in K & q in K & p' in K & q' in K & AFP satisfies_TDES &
         a in M & b in M & x in M & y in M & a<>b & q<>p &
      p,a // p',x & p,b // p',y & q,a // q',x
                                          implies q,b // q',y;

theorem :: HOMOTHET:8
 a,b // K & not a in K & AFP satisfies_TDES implies ex f st f is_Sc K &
                                                           f.a=b;

theorem :: HOMOTHET:9
   AFP satisfies_TDES iff (for a,b,K st a,b // K & not a in K ex f
                                           st f is_Sc K & f.a=b);