:: Translations in Affine Planes
::  by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received June 12, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies DIRAF, SUBSET_1, VECTSP_1, ANALOAF, FUNCT_2, STRUCT_0, TRANSGEO,
      FUNCT_1, AFF_2, INCSP_1, AFF_1, RELAT_1;
 notations PARTFUN1, FUNCT_2, STRUCT_0, ANALOAF, DIRAF, AFF_1, AFF_2, TRANSGEO;
 constructors RELAT_2, PARTFUN1, AFF_1, AFF_2, TRANSGEO, RELSET_1;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_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;
end;

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

reserve AFP for AffinPlane,
  a,a9,b,b9,c,c9,d,p,p9,q,q9,r,x,x9,y,y9,z for Element of AFP,
  A,C,P for Subset of AFP,
  f,g,h,f1,f2 for Permutation of the carrier of AFP;

theorem :: TRANSLAC:2
  AFP is Fanoian & 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:3
  f is translation & not LIN a,f.a,x & a,f.a // x,y & a,x // f.a,y
  implies y=f.x;

theorem :: TRANSLAC:4
  AFP is translational iff for a,a9,b,c,b9,c9 st not LIN a,a9,b &
  not LIN a,a9,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9
  holds b,c // b9,c9;

theorem :: TRANSLAC:5
  ex f st f is translation & f.a=a;

theorem :: TRANSLAC:6
  (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:7
  AFP is translational implies ex f st f is translation & f.a=b;

theorem :: TRANSLAC:8
  (for a,b ex f st f is translation & f.a=b) implies AFP is translational;

theorem :: TRANSLAC:9
  f is translation & g is translation & not LIN a,f.a,g.a implies f*g=g*f;

theorem :: TRANSLAC:10
  AFP is translational & f is translation & g is translation implies f*g=g*f;

theorem :: TRANSLAC:11
  f is translation & g is translation & p,f.p // p,g.p implies p,f
  .p // p,(f*g).p;

theorem :: TRANSLAC:12
  AFP is Fanoian & AFP is translational & f is translation implies ex g
  st g is translation & g*g=f;

theorem :: TRANSLAC:13
  AFP is Fanoian & f is translation & f*f=id the carrier of AFP
  implies f=id the carrier of AFP;

theorem :: TRANSLAC:14
  AFP is translational & AFP is Fanoian & f1 is translation & f2 is
  translation & g=f1*f1 & g=f2*f2 implies f1=f2;