The abstract of the Mizar article:

Translations in Affine Planes

by

Henryk Oryszczyszyn, and

Krzysztof Prazmowski

Received June 12, 1990

MML identifier: TRANSLAC

[ Mizar article, MML identifier index ]

environ

 vocabulary DIRAF, VECTSP_1, ANALOAF, PASCH, FUNCT_2, TRANSGEO, FUNCT_1, AFF_2,
      INCSP_1, AFF_1, RELAT_1;
 notation PARTFUN1, FUNCT_2, STRUCT_0, ANALOAF, DIRAF, AFF_1, AFF_2, TRANSGEO;
 constructors AFF_1, AFF_2, TRANSGEO, MEMBERED, PARTFUN1, RELAT_2, XBOOLE_0;
 clusters STRUCT_0, RELSET_1, FUNCT_2, MEMBERED, ZFMISC_1, PARTFUN1, FUNCT_1,
      XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

 reserve AS for AffinSpace,
         a,b,c,d,p,q,r,s,x for Element of AS;

definition let AS;
 attr AS is Fanoian means
:: TRANSLAC:def 1
  for a,b,c,d st a,b // c,d & a,c // b,d & a,d // b,c
                                   holds LIN a,b,c;
  synonym AS satisfies_Fano;
end;

canceled;

theorem :: TRANSLAC:2
 (ex a,b,c st LIN a,b,c & a<>b & a<>c & b<>c) implies
   (for p,q st p<>q holds (ex r st LIN p,q,r & p<>r & q<>r));

 reserve AFP for AffinPlane,
         a,a',b,b',c,c',d,p,p',q,q',r,x,x',y,y',z
                        for Element of AFP,
         A,C,P for Subset of AFP,
         f,g,h,f1,f2 for Permutation of the carrier of AFP;

canceled;

theorem :: TRANSLAC:4
(AFP satisfies_Fano &
 a,b // c,d & a,c // b,d & not LIN a,b,c) implies ex p st LIN b,c,p & LIN a,d,p
;

theorem :: TRANSLAC:5
 f is_Tr & not LIN a,f.a,x & a,f.a // x,y & a,x // f.a,y
                                                implies y=f.x;

theorem :: TRANSLAC:6
  AFP satisfies_des iff
  (for a,a',b,c,b',c' st not LIN a,a',b & not LIN a,a',c & a,a' // b,b' &
    a,a' // c,c' & a,b // a',b' & a,c // a',c' holds b,c // b',c');

theorem :: TRANSLAC:7
 ex f st f is_Tr & f.a=a;

theorem :: TRANSLAC:8
 (for p,q,r st p<>q & LIN p,q,r holds r = p or r = q) & a,b // p,q &
     a,p // b,q & not LIN a,b,p implies a,q // b,p;

theorem :: TRANSLAC:9
 AFP satisfies_des implies ex f st f is_Tr & f.a=b;

theorem :: TRANSLAC:10
   (for a,b ex f st f is_Tr & f.a=b) implies AFP satisfies_des;

theorem :: TRANSLAC:11
 f is_Tr & g is_Tr & not LIN a,f.a,g.a implies f*g=g*f;

theorem :: TRANSLAC:12
 AFP satisfies_des & f is_Tr & g is_Tr implies f*g=g*f;

theorem :: TRANSLAC:13
 f is_Tr & g is_Tr & p,f.p // p,g.p implies p,f.p // p,(f*g).p;

theorem :: TRANSLAC:14
   AFP satisfies_Fano & AFP satisfies_des & f is_Tr
                                 implies ex g st g is_Tr & g*g=f;

theorem :: TRANSLAC:15
 AFP satisfies_Fano &
  f is_Tr & f*f=id the carrier of AFP implies f=id the carrier of AFP;

theorem :: TRANSLAC:16
   AFP satisfies_des & AFP satisfies_Fano &
  g is_Tr & f1 is_Tr & f2 is_Tr & g=f1*f1 & g=f2*f2 implies f1=f2;