:: Homotheties and Shears in Affine Planes
::  by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received September 21, 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, FUNCT_2, STRUCT_0, AFF_2, ANALOAF, INCSP_1,
      AFF_1, TRANSGEO, FUNCT_1, RELAT_1, TARSKI, HOMOTHET;
 notations TARSKI, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0, ANALOAF, DIRAF,
      AFF_1, AFF_2, TRANSGEO;
 constructors PARTFUN1, AFF_1, AFF_2, TRANSGEO, RELSET_1;
 registrations STRUCT_0;
 requirements SUBSET, BOOLE;


begin

reserve AFP for AffinPlane;
reserve a,a9,b,b9,c,c9,d,d9,o,p,p9,q,q9,r,s,t,x,y,z for Element of AFP;
reserve A,A9,C,D,P,B9,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,p9 &
  LIN o,p,q & LIN o,p,q9 & p<>q & o<>q & o<>x & a,p // b,p9 & a,q // b,q9 & x,p
  // y,p9 & AFP is Desarguesian implies x,q // y,q9;

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

theorem :: HOMOTHET:3
  AFP is Desarguesian implies for o,a,b st o<>a & o<>b & LIN o,a,b
  ex f st f is dilatation & f.o=o & f.a=b;

theorem :: HOMOTHET:4
  AFP is Desarguesian iff for o,a,b st o<>a & o<>b & LIN o,a,b ex f st f
  is dilatation & f.o=o & f.a=b;

definition
  let AFP,f,K;
  pred f is_Sc K means
:: HOMOTHET:def 1

  f is collineation & K is being_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 is Moufangian;

theorem :: HOMOTHET:7
  K // M & p in K & q in K & p9 in K & q9 in K & AFP is Moufangian
& a in M & b in M & x in M & y in M & a<>b & q<>p & p,a // p9,x & p,b // p9,y &
  q,a // q9,x implies q,b // q9,y;

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

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