The Mizar article:

Transformations in Affine Spaces

by
Henryk Oryszczyszyn, and
Krzysztof Prazmowski

Received May 31, 1990

Copyright (c) 1990 Association of Mizar Users

MML identifier: TRANSGEO
[ MML identifier index ]


environ

 vocabulary FUNCT_2, FUNCT_1, BOOLE, RELAT_1, RELAT_2, ANALOAF, DIRAF, PARSP_1,
      INCSP_1, AFF_1, TRANSGEO;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_2, FUNCT_1, RELSET_1,
      STRUCT_0, ANALOAF, DIRAF, PARTFUN1, FUNCT_2, AFF_1;
 constructors DOMAIN_1, RELAT_2, AFF_1, MEMBERED, PARTFUN1, XBOOLE_0;
 clusters ANALOAF, DIRAF, RELSET_1, STRUCT_0, FUNCT_2, MEMBERED, ZFMISC_1,
      PARTFUN1, FUNCT_1, XBOOLE_0;
 requirements SUBSET, BOOLE;
 definitions RELAT_2;
 theorems DOMAIN_1, FUNCT_1, FUNCT_2, ANALOAF, DIRAF, AFF_1, PASCH, TARSKI,
      ZFMISC_1, RELAT_1, REALSET1, XBOOLE_0;
 schemes FUNCT_2;

begin

 reserve A for non empty set,
         a,b,x,y,z,t for Element of A,
         f,g,h for Permutation of A;

definition let A be set, f,g be Permutation of A;
 redefine func g*f -> Permutation of A;
 coherence proof thus g*f is Permutation of A; end;
end;

canceled;

theorem Th2:
   ex x st f.x=y
 proof
    y in A & rng f = A by FUNCT_2:def 3;
  then ex x being set st x in dom f & f.x = y by FUNCT_1:def 5;
  hence thesis;
 end;

canceled;

theorem Th4:
   f.x=y iff (f").y=x
   proof A1: f is one-to-one & rng f = A &
    f is Function of A,A by FUNCT_2:def 3;
       now assume f.x=y;
     then f".(f.x)=f".y & x in A;
     then f".(f.x)=f".y & x in dom f by FUNCT_2:def 1;
     hence x=f".y by FUNCT_1:56; end;
    hence thesis by A1,FUNCT_1:57;
   end;

definition let A,f,g;
 func f\g -> Permutation of A equals
  :Def1: (g*f)*g";
  coherence;
 end;

scheme EXPermutation{A() -> non empty set,P[set,set]}:
  ex f being Permutation of A()
   st for x,y being Element of A() holds f.x=y iff P[x,y]
  provided
A1:  for x being Element of A()
      ex y being Element of A() st P[x,y] and
A2:  for y being Element of A()
      ex x being Element of A() st P[x,y] and
A3:  for x,y,x' being Element of A()
       st P[x,y] & P[x',y] holds x=x' and
A4:  for x,y,y' being Element of A()
       st P[x,y] & P[x,y'] holds y=y'
 proof
   defpred X[Element of A(),Element of A()] means P[$1,$2];
A5:  for x being Element of A()
      ex y being Element of A() st X[x,y] by A1;
  consider f being Function of A(), A() such that
A6: for x being Element of A() holds X[x,f.x] from FuncExD(A5);
    now
     now let x1,x2 be set;
    assume
A7:    x1 in A() & x2 in A();
    then P[x1,f.x1] & P[x2,f.x2] &
      f.x1 is Element of A() & f.x2 is Element of A() by A6,FUNCT_2:7;
    hence f.x1 = f.x2 implies x1 = x2 by A3,A7;
   end;
   hence f is one-to-one by FUNCT_2:25;
     now
     thus rng f c= A();
       now let y be set;
       assume A8: y in A();
       then consider x being Element of A() such that
A9:       P[x,y] by A2;
         P[x,f.x] & f.x is Element of A() by A6;
       then f.x = y & A() <> {} by A4,A8,A9;
       hence y in rng f by FUNCT_2:6;
     end;
     hence A() c= rng f by TARSKI:def 3;
   end;
   hence rng f = A() by XBOOLE_0:def 10;
  end;
  then reconsider f as Permutation of A() by FUNCT_2:83;
  take f;
  let x,y be Element of A();
  thus f.x=y implies P[x,y] by A6;
  assume
A10:   P[x,y];
    P[x,f.x] by A6;
  hence thesis by A4,A10;
 end;

canceled 4;

theorem
   f.(f".x) = x & f".(f.x) = x by Th4;

canceled;

theorem
   f*(id A) = (id A)*f
proof f*(id A)=f by FUNCT_2:23; hence thesis by FUNCT_2:23; end;

Lm1: f*g=f*h implies g=h
  proof assume f*g=f*h;
    then (f"*f)*g=f"*(f*h) by RELAT_1:55;
    then (f"*f)*g=(f"*f)*h by RELAT_1:55;
    then (id A)*g=(f"*f)*h by FUNCT_2:88;
    then (id A)*g=(id A)*h by FUNCT_2:88;
    then g=(id A)*h by FUNCT_2:23;
   hence thesis by FUNCT_2:23;
  end;

Lm2: g*f=h*f implies g=h
  proof assume g*f=h*f;
    then g*(f*f")=(h*f)*f" by RELAT_1:55;
    then g*(f*f")=h*(f*f") by RELAT_1:55;
    then g*(id A)=h*(f*f") by FUNCT_2:88;
    then g*(id A)=h*(id A) by FUNCT_2:88;
    then g=h*(id A) by FUNCT_2:23;
   hence thesis by FUNCT_2:23;
  end;

canceled;

theorem
   g*f=h*f or f*g=f*h implies g=h by Lm1,Lm2;

canceled 2;

theorem
   (f*g)\h = (f\h)*(g\h)
  proof thus
     (f*g)\h = (h*(f*g))*h" by Def1
          .= (h*(f*((id A)*g)))*h" by FUNCT_2:23
          .= (h*(f*((h"*h)*g)))*h" by FUNCT_2:88
          .= (h*(f*(h"*(h*g))))*h" by RELAT_1:55
          .= (h*((f*h")*(h*g)))*h" by RELAT_1:55
          .= ((h*(f*h"))*(h*g))*h" by RELAT_1:55
          .= (h*(f*h"))*((h*g)*h") by RELAT_1:55
          .= ((h*f)*h")*((h*g)*h") by RELAT_1:55
          .= (f\h)*((h*g)*h") by Def1
          .= (f\h)*(g\h) by Def1;
  end;

theorem
   (f")\g = (f\g)"
 proof thus (f\g)" = ((g*f)*g")" by Def1
        .= (g")"*(g*f)" by FUNCT_1:66
        .= (g")"*(f"*g") by FUNCT_1:66
        .= g*(f"*g") by FUNCT_1:65
        .= (g*f")*g" by RELAT_1:55
        .= f"\g by Def1;
 end;

theorem
   f\(g*h) = (f\h)\g
 proof
  thus f\(g*h) = ((g*h)*f)*(g*h)" by Def1
              .= ((g*h)*f)*(h"*g") by FUNCT_1:66
              .= (((g*h)*f)*h")*g" by RELAT_1:55
              .= ((g*(h*f))*h")*g" by RELAT_1:55
              .= (g*((h*f)*h"))*g" by RELAT_1:55
              .= (g*(f\h))*g" by Def1
              .= (f\h)\g by Def1;
 end;

theorem
   (id A)\f = id A
 proof
  thus (id A)\f = (f*(id A))*f" by Def1
                            .= f*f" by FUNCT_2:23
                            .= id A by FUNCT_2:88;
 end;

theorem
   f\(id A) = f
 proof thus f\(id A) = ((id A)*f)*(id A)" by Def1
                       .= f*(id A)" by FUNCT_2:23
                       .= f*(id A) by FUNCT_1:67
                       .= f by FUNCT_2:23;
 end;

theorem
   f.a=a implies (f\g).(g.a)=g.a
 proof assume A1: f.a=a; A2: g".(g.a) = (g"*g).a by FUNCT_2:70
                                   .= (id A).a by FUNCT_2:88
                                   .= a by FUNCT_1:35;
  thus (f\g).(g.a) = ((g*f)*g").(g.a) by Def1
              .= (g*f).a by A2,FUNCT_2:70
              .= g.a by A1,FUNCT_2:70;
  end;

reserve R for Relation of [:A,A:];

definition let A,f,R;
 pred f is_FormalIz_of R means
 :Def2: for x,y holds [[x,y],[f.x,f.y]] in R;
end;

canceled;

theorem
 Th23: R is_reflexive_in [:A,A:] implies id A is_FormalIz_of R
  proof assume A1: for x being set st x in [:A,A:] holds [x,x] in R;
   let x,y;
   A2: (id A).x = x & (id A).y = y by FUNCT_1:35;
     [x,y] in [:A,A:] by ZFMISC_1:def 2;
   hence thesis by A1,A2;
  end;

theorem
 Th24: R is_symmetric_in [:A,A:] & f is_FormalIz_of R
                                       implies f" is_FormalIz_of R
  proof assume A1: for x,y being set st x in [:A,A:] & y in [:A,A:] &
                                            [x,y] in R holds [y,x] in R;
   assume A2: for x,y holds [[x,y],[f.x,f.y]] in R;
   let x,y;
   A3: f.(f".x) = x & f.(f".y) =y by Th4;
     [[f".x,f".y],[f.(f".x),f.(f".y)]] in R & [f".x,f".y] in [:A,A:] &
    [f.(f".x),f.(f".y)] in [:A,A:] by A2,ZFMISC_1:def 2;
   hence thesis by A1,A3;
 end;

theorem
    R is_transitive_in [:A,A:] & f is_FormalIz_of R
                 & g is_FormalIz_of R implies (f*g) is_FormalIz_of R
   proof assume that A1: (for x,y,z being set st x in [:A,A:] &
    y in [:A,A:] & z in [:A,A:] & [x,y] in R & [y,z] in R holds [x,z] in R)
    and A2: (for x,y holds [[x,y],[f.x,f.y]] in R) &
    (for x,y holds [[x,y],[g.x,g.y]] in R);
    let x,y;
       f.(g.x) = (f*g).x & f.(g.y) = (f*g).y by FUNCT_2:70;
    then [[x,y],[g.x,g.y]] in R & [[g.x,g.y],[(f*g).x,(f*g).y]] in R &
    [x,y] in [:A,A:] & [g.x,g.y] in [:A,A:] &
            [(f*g).x,(f*g).y] in [:A,A:] by A2,ZFMISC_1:def 2;
    hence [[x,y],[(f*g).x,(f*g).y]] in R by A1;
   end;

theorem Th26:
   (for a,b,x,y,z,t st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a<>b
     holds [[x,y],[z,t]] in R) & (for x,y,z holds [[x,x],[y,z]] in R) &
   f is_FormalIz_of R & g is_FormalIz_of R implies f*g is_FormalIz_of R
   proof assume that A1: for a,b,x,y,z,t st
    [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a<>b holds [[x,y],[z,t]] in R
    and A2: for x,y,z holds [[x,x],[y,z]] in R
    and A3: (for x,y holds [[x,y],[f.x,f.y]] in R) &
    (for x,y holds [[x,y],[g.x,g.y]] in R);
    let x,y;
       f.(g.x) = (f*g).x & f.(g.y) = (f*g).y by FUNCT_2:70;
    then A4: [[x,y],[g.x,g.y]] in R & [[g.x,g.y],[(f*g).x,(f*g).y]] in R &
    [x,y] in [:A,A:] & [g.x,g.y] in [:A,A:] &
            [(f*g).x,(f*g).y] in [:A,A:] by A3,ZFMISC_1:def 2;
     now assume g.x = g.y; then x = y by FUNCT_2:85;
    hence [[x,y],[(f*g).x,(f*g).y]] in R by A2;
   end;
   hence [[x,y],[(f*g).x,(f*g).y]] in R by A1,A4;
   end;

definition
 let A; let f; let R;
 pred f is_automorphism_of R means :Def3:
  for x,y,z,t holds ([[x,y],[z,t]] in R iff [[f.x,f.y],[f.z,f.t]] in R);
end;

canceled;

theorem Th28:
 id A is_automorphism_of R
 proof let x,y,z,t;
  A1: (id A).x = x & (id A).y = y & (id A).z = z & (id A).t = t by FUNCT_1:35;
  hence [[x,y],[z,t]] in R implies
   [[(id A).x,(id A).y],[(id A).z,(id A).t]] in R;
  assume [[(id A).x,(id A).y],[(id A).z,(id A).t]] in R;
   hence [[x,y],[z,t]] in R by A1;
 end;

theorem Th29:
 f is_automorphism_of R implies f" is_automorphism_of R
 proof assume A1: for x,y,z,t holds
   ([[x,y],[z,t]] in R iff [[f.x,f.y],[f.z,f.t]] in R);
  let x,y,z,t;
     f.(f".x) = x & f.(f".y) = y & f.(f".z) = z & f.(f".t) = t by Th4;
   hence thesis by A1;
 end;

theorem Th30:
 f is_automorphism_of R & g is_automorphism_of R implies
                                    g*f is_automorphism_of R
 proof assume A1: (for x,y,z,t holds
   ([[x,y],[z,t]] in R iff [[f.x,f.y],[f.z,f.t]] in R)) &
 (for x,y,z,t holds ([[x,y],[z,t]] in R iff [[g.x,g.y],[g.z,g.t]] in R));
  let x,y,z,t;
  A2: g.(f.x) = (g*f).x & g.(f.y) = (g*f).y &
      g.(f.z) = (g*f).z & g.(f.t) = (g*f).t by FUNCT_2:70;
     ([[x,y],[z,t]] in R iff [[f.x,f.y],[f.z,f.t]] in R) &
   ([[f.x,f.y],[f.z,f.t]] in R iff
             [[g.(f.x),g.(f.y)],[g.(f.z),g.(f.t)]] in R) by A1;
   hence thesis by A2;
 end;

theorem
   R is_symmetric_in [:A,A:] & R is_transitive_in [:A,A:] &
            f is_FormalIz_of R implies f is_automorphism_of R
proof assume that
 A1: for x,y being set st x in [:A,A:] & y in [:A,A:] &
                            [x,y] in R holds [y,x] in R and
 A2: for x,y,z being set st x in [:A,A:] &
   y in [:A,A:] & z in [:A,A:] & [x,y] in R & [y,z] in R holds [x,z] in R and
 A3: for x,y holds [[x,y],[f.x,f.y]] in R;
 let x,y,z,t;
 A4: [x,y] in [:A,A:] & [z,t] in [:A,A:] & [f.x,f.y] in [:A,A:] &
     [f.z,f.t] in [:A,A:] by ZFMISC_1:def 2;
  A5: now assume A6: [[x,y],[z,t]] in R;
    [[x,y],[f.x,f.y]] in R & [[z,t],[f.z,f.t]] in R by A3;
  then [[f.x,f.y],[x,y]] in R & [[z,t],[f.z,f.t]] in R by A1,A4;
  then [[f.x,f.y],[z,t]] in R & [[z,t],[f.z,f.t]] in R by A2,A4,A6;
  hence [[f.x,f.y],[f.z,f.t]] in R by A2,A4; end;
    now assume A7: [[f.x,f.y],[f.z,f.t]] in R;
    [[x,y],[f.x,f.y]] in R & [[z,t],[f.z,f.t]] in R by A3;
  then [[x,y],[f.z,f.t]] in R & [[f.z,f.t],[z,t]] in R by A1,A2,A4,A7;
  hence [[x,y],[z,t]] in R by A2,A4; end;
  hence thesis by A5;
 end;

theorem
   (for a,b,x,y,z,t st [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a<>b
     holds [[x,y],[z,t]] in R) & (for x,y,z holds [[x,x],[y,z]] in R) &
    R is_symmetric_in [:A,A:] &
   f is_FormalIz_of R implies f is_automorphism_of R
   proof assume that A1: for a,b,x,y,z,t st
    [[x,y],[a,b]] in R & [[a,b],[z,t]] in R & a<>b holds [[x,y],[z,t]] in R
    and A2: for x,y,z holds [[x,x],[y,z]] in R and
    A3: for x,y being set st x in [:A,A:] & y in [:A,A:] &
                            [x,y] in R holds [y,x] in R and
    A4: for x,y holds [[x,y],[f.x,f.y]] in R;
    A5: for x,y,z holds [[y,z],[x,x]] in R proof let x,y,z;
     A6: [y,z] in [:A,A:] & [x,x] in [:A,A:] by ZFMISC_1:def 2;
       [[x,x],[y,z]] in R by A2; hence thesis by A3,A6; end;
 let x,y,z,t;
 A7: [x,y] in [:A,A:] & [z,t] in [:A,A:] & [f.x,f.y] in [:A,A:] &
     [f.z,f.t] in [:A,A:] by ZFMISC_1:def 2;
  A8: [[x,y],[f.x,f.y]] in R & [[z,t],[f.z,f.t]] in R by A4;
  then A9: [[f.x,f.y],[x,y]] in R & [[f.z,f.t],[z,t]] in R by A3,A7;
  A10: now assume A11: [[x,y],[z,t]] in R;
      now assume A12: x<>y & z<>t; then [[f.x,f.y],[z,t]] in R
    by A1,A9,A11; hence [[f.x,f.y],[f.z,f.t]] in R by A1,A8,A12; end;
   hence [[f.x,f.y],[f.z,f.t]] in R by A2,A5; end;
     now assume A13: [[f.x,f.y],[f.z,f.t]] in R;
   A14: now assume f.x = f.y; then x=y by FUNCT_2:85;
    hence [[x,y],[z,t]] in R by A2; end;
   A15: now assume f.z = f.t; then z=t by FUNCT_2:85;
    hence [[x,y],[z,t]] in R by A5; end;
      now assume A16: f.x<>f.y & f.z<>f.t; then [[x,y],[f.z,f.t]] in R
    by A1,A8,A13; hence [[x,y],[z,t]] in R by A1,A9,A16; end;
   hence [[x,y],[z,t]] in R by A14,A15; end;
 hence thesis by A10;
end;

theorem
     f is_FormalIz_of R & g is_automorphism_of R
          implies f\g is_FormalIz_of R
 proof assume that
  A1: for x,y holds [[x,y],[f.x,f.y]] in R and
  A2: for x,y,z,t holds ([[x,y],[z,t]] in R iff
                          [[g.x,g.y],[g.z,g.t]] in R);
  let x,y;
  A3: g.(g".x) = x & g.(g".y) = y by Th4;
    [[g".x,g".y],[f.(g".x),f.(g".y)]] in R by A1;
  then [[x,y],[g.(f.(g".x)),g.(f.(g".y))]] in R by A2,A3;
  then [[x,y],[(g*f).(g".x),g.(f.(g".y))]] in R by FUNCT_2:70;
  then [[x,y],[(g*f).(g".x),(g*f).(g".y)]] in R by FUNCT_2:70;
  then [[x,y],[((g*f)*g").x,(g*f).(g".y)]] in R by FUNCT_2:70;
  then [[x,y],[((g*f)*g").x,((g*f)*g").y]] in R by FUNCT_2:70;
  then [[x,y],[(f\g).x,((g*f)*g").y]] in R by Def1;
  hence [[x,y],[(f\g).x,(f\g).y]] in R by Def1;
 end;

reserve AS for non empty AffinStruct;

definition let AS; let f be Permutation of the carrier of AS;
  pred f is_DIL_of AS means
  :Def4: f is_FormalIz_of the CONGR of AS;
end;

reserve a,b,x,y for Element of AS;

canceled;

theorem Th35: for f being Permutation of the carrier of AS holds
      (f is_DIL_of AS iff (for a,b holds a,b // f.a,f.b))
  proof let f be Permutation of the carrier of AS;
   A1: now assume f is_DIL_of AS;
    then A2: f is_FormalIz_of the CONGR of AS by Def4;
    let a,b; [[a,b],[f.a,f.b]] in the CONGR of AS by A2,Def2;
    hence a,b // f.a,f.b by ANALOAF:def 2; end;
      now assume A3: for a,b holds a,b // f.a,f.b;
      for x,y holds [[x,y],[f.x,f.y]] in the CONGR of AS proof
      let x,y; x,y // f.x,f.y by A3; hence thesis by ANALOAF:def 2; end;
    then f is_FormalIz_of the CONGR of AS by Def2;
    hence f is_DIL_of AS by Def4; end;
   hence thesis by A1; end;

definition let IT be non empty AffinStruct;
 attr IT is CongrSpace-like means
  :Def5: (for x,y,z,t,a,b being Element of IT st
           x,y // a,b & a,b // z,t & a<>b holds x,y // z,t) &
           (for x,y,z being Element of IT holds
           x,x // y,z) &
           (for x,y,z,t being Element of IT st
           x,y // z,t holds z,t // x,y) &
           (for x,y being Element of IT holds
           x,y // x,y);
end;

definition
 cluster strict CongrSpace-like (non empty AffinStruct);
  existence
   proof consider OAS being strict OAffinSpace;
       (for x,y,z,t,a,b being Element of OAS st
           x,y // a,b & a,b // z,t & a<>b holds x,y // z,t) &
     (for x,y,z being Element of OAS holds
          x,x // y,z) &
     (for x,y,z,t being Element of OAS st
          x,y // z,t holds z,t // x,y) &
      for x,y being Element of OAS holds
          x,y // x,y by DIRAF:4,5,6,7;
      then OAS is CongrSpace-like by Def5;
     hence thesis;
   end;
end;

definition
  mode CongrSpace is CongrSpace-like (non empty AffinStruct);
end;

reserve CS for CongrSpace;

Lm3: the CONGR of CS is_reflexive_in [:the carrier of CS,the carrier of CS:]
 proof let x be set; assume
     x in [:the carrier of CS,the carrier of CS:];
  then consider x1,x2 being Element of CS such that
  A1: x=[x1,x2] by DOMAIN_1:9;
    x1,x2 // x1,x2 by Def5;
  hence [x,x] in the CONGR of CS by A1,ANALOAF:def 2;
 end;

Lm4: the CONGR of CS is_symmetric_in [:the carrier of CS,the carrier of CS:]
 proof let x,y be set; assume that
  A1: x in [:the carrier of CS,the carrier of CS:] &
  y in [:the carrier of CS,the carrier of CS:] and
  A2: [x,y] in the CONGR of CS;
  consider x1,x2 being Element of CS such that
  A3: x=[x1,x2] by A1,DOMAIN_1:9;
  consider y1,y2 being Element of CS such that
  A4: y=[y1,y2] by A1,DOMAIN_1:9;
    x1,x2 // y1,y2 by A2,A3,A4,ANALOAF:def 2; then y1,y2 // x1,x2 by Def5;
hence [y,x] in the CONGR of CS by A3,A4,ANALOAF:def 2; end;

canceled;

theorem Th37: id the carrier of CS is_DIL_of CS
 proof
    the CONGR of CS is_reflexive_in
   [:the carrier of CS,the carrier of CS:] by Lm3;
 then id the carrier of CS is_FormalIz_of the CONGR of CS by Th23;
 hence thesis by Def4; end;

theorem Th38: for f being Permutation of the carrier of CS st
           f is_DIL_of CS holds f" is_DIL_of CS
 proof let f be Permutation of the carrier of CS;
  assume f is_DIL_of CS; then f is_FormalIz_of the CONGR of CS &
   the CONGR of CS is_symmetric_in
        [:the carrier of CS,the carrier of CS:] by Def4,Lm4;
   then f" is_FormalIz_of the CONGR of CS by Th24;
   hence thesis by Def4;
 end;

theorem Th39: for f,g being Permutation of the carrier of CS st
    f is_DIL_of CS & g is_DIL_of CS holds f*g is_DIL_of CS
 proof let f,g be Permutation of the carrier of CS;
  assume f is_DIL_of CS & g is_DIL_of CS;
  then A1: f is_FormalIz_of the CONGR of CS &
                   g is_FormalIz_of the CONGR of CS by Def4;
   A2: now let a,b,x,y,z,t be Element of CS;
     assume [[x,y],[a,b]] in the CONGR of CS &
      [[a,b],[z,t]] in the CONGR of CS & a<>b;
      then x,y // a,b & a,b // z,t & a<>b by ANALOAF:def 2;
      then x,y // z,t by Def5;
      hence [[x,y],[z,t]] in the CONGR of CS by ANALOAF:def 2;
      end;
      now let x,y,z be Element of CS;
       x,x // y,z by Def5;
     hence [[x,x],[y,z]] in the CONGR of CS by ANALOAF:def 2;
    end;
   then f*g is_FormalIz_of the CONGR of CS by A1,A2,Th26;
   hence thesis by Def4;
 end;

reserve OAS for OAffinSpace;
reserve a,b,c,d,p,q,r,x,y,z,t,u for Element of OAS;

theorem Th40: OAS is CongrSpace-like proof
 thus for x,y,z,t,a,b being Element of OAS st
   x,y // a,b & a,b // z,t & a<>b holds x,y // z,t by DIRAF:6;
 thus for x,y,z being Element of OAS holds
        x,x // y,z by DIRAF:7;
 thus for x,y,z,t being Element of OAS st
        x,y // z,t holds z,t // x,y by DIRAF:5;
 thus for x,y being Element of OAS holds
        x,y // x,y by DIRAF:4;
end;

reserve f,g for Permutation of the carrier of OAS;

definition let OAS; let f be Permutation of the carrier of OAS;
  attr f is positive_dilatation means
  :Def6: f is_DIL_of OAS;
  synonym f is_CDil;
end;

canceled;

theorem Th42: for f being Permutation of the carrier of OAS holds
  (f is_CDil iff (for a,b holds a,b // f.a,f.b))
 proof let f be Permutation of the carrier of OAS;
 A1: now assume f is_CDil; then f is_DIL_of OAS by Def6;
   hence for a,b holds a,b // f.a,f.b by Th35; end;
    now assume for a,b holds a,b // f.a,f.b; then f is_DIL_of OAS by Th35;
   hence f is_CDil by Def6; end;
 hence thesis by A1; end;

definition let OAS; let f be Permutation of the carrier of OAS;
  attr f is negative_dilatation means
  :Def7: for a,b holds a,b // f.b,f.a;
  synonym f is_SDil;
end;

canceled;

theorem Th44: id the carrier of OAS is_CDil
  proof OAS is CongrSpace by Th40; then id the carrier of OAS is_DIL_of OAS
  by Th37; hence thesis by Def6; end;

theorem for f being Permutation of the carrier of OAS st
       f is_CDil holds f" is_CDil
  proof let f be Permutation of the carrier of OAS such that A1: f is_CDil;
  A2: OAS is CongrSpace by Th40;
    f is_DIL_of OAS by A1,Def6; then f" is_DIL_of OAS by A2,Th38;
  hence thesis by Def6; end;

theorem for f,g being Permutation of the carrier of OAS st
      f is_CDil & g is_CDil holds f*g is_CDil
  proof let f,g be Permutation of the carrier of OAS; assume
    f is_CDil & g is_CDil; then f is_DIL_of OAS & g is_DIL_of OAS &
  OAS is CongrSpace by Def6,Th40;
  then f*g is_DIL_of OAS by Th39; hence thesis by Def6; end;

theorem
   not ex f st f is_SDil & f is_CDil
  proof given f such that A1: f is_SDil & f is_CDil;
   consider a,b such that A2: a<>b by REALSET1:def 20;
     a,b // f.a,f.b & a,b // f.b,f.a by A1,Def7,Th42;
   then f.a,f.b // f.b,f.a by A2,ANALOAF:def 5; then f.a = f.b by ANALOAF:def 5
;
   hence contradiction by A2,FUNCT_2:85;
  end;

theorem
   f is_SDil implies f" is_SDil
  proof assume A1: f is_SDil; let x,y;
    set x'=f".x, y'=f".y;
      f.x'=x & f.y'=y by Th4; then y',x' // x,y by A1,Def7;
   hence x,y // f".y,f".x by DIRAF:5;
  end;

theorem f is_CDil & g is_SDil
                    implies f*g is_SDil & g*f is_SDil
  proof assume that A1: f is_CDil and A2: g is_SDil;
   thus x,y // (f*g).y,(f*g).x
     proof set x'=g.x; set y'=g.y;
       A3: (f*g).x= f.x' & (f*g).y=f.y' by FUNCT_2:70;
       A4: x,y // y',x' by A2,Def7;
A5:       y',x' // f.y',f.x' by A1,Th42;
         now assume x'=y'; then x=y by FUNCT_2:85;
        hence x,y // (f*g).y,(f*g).x by DIRAF:7;
       end;
      hence x,y // (f*g).y,(f*g).x by A3,A4,A5,DIRAF:6;
     end;
   thus x,y // (g*f).y,(g*f).x
     proof set x'=f.x; set y'=f.y;
     A6: (g*f).x= g.x' & (g*f).y=g.y' by FUNCT_2:70;
       A7: x,y // x',y' by A1,Th42;
A8:       x',y' // g.y',g.x' by A2,Def7;
         now assume x'=y'; then x=y by FUNCT_2:85;
        hence x,y // (g*f).y,(g*f).x by DIRAF:7;
       end;
      hence x,y // (g*f).y,(g*f).x by A6,A7,A8,DIRAF:6;
     end;
  end;

definition let OAS; let f be Permutation of the carrier of OAS;
  attr f is dilatation means
  :Def8: f is_FormalIz_of lambda(the CONGR of OAS);
  synonym f is_Dil;
end;

canceled;

theorem Th51:
 for f being Permutation of the carrier of OAS holds
       (f is_Dil iff (for a,b holds a,b '||' f.a,f.b))
 proof let f be Permutation of the carrier of OAS;
 A1: now assume f is_Dil;
  then A2: f is_FormalIz_of lambda(the CONGR of OAS) by Def8;
  let a,b; [[a,b],[f.a,f.b]] in lambda(the CONGR of OAS) by A2,Def2;
  hence a,b '||' f.a,f.b by DIRAF:23; end;
    now assume A3: for a,b holds a,b '||' f.a,f.b;
     now let a,b; a,b '||' f.a,f.b by A3; hence
      [[a,b],[f.a,f.b]] in lambda(the CONGR of OAS) by DIRAF:23; end;
   then f is_FormalIz_of lambda(the CONGR of OAS) by Def2;
   hence f is_Dil by Def8; end;
 hence thesis by A1; end;

theorem
   f is_CDil or f is_SDil implies f is_Dil
  proof assume A1: f is_CDil or f is_SDil;
      now let x,y; x,y // f.x,f.y or x,y // f.y,f.x by A1,Def7,Th42;
    hence x,y '||' f.x,f.y by DIRAF:def 4; end;
  hence thesis by Th51; end;

theorem
   for f being Permutation of the carrier of OAS st f is_Dil
 ex f' being Permutation of the carrier of Lambda(OAS) st
   f=f' & f' is_DIL_of Lambda(OAS)
 proof let f be Permutation of the carrier of OAS; assume f is_Dil;
 then A1: f is_FormalIz_of lambda(the CONGR of OAS) by Def8;
A2: Lambda(OAS) =
 AffinStruct(#the carrier of OAS, lambda(the CONGR of OAS)#) by DIRAF:def 2;
 then reconsider f'=f as Permutation of the carrier of Lambda(OAS);
 take f';
 thus thesis by A1,A2,Def4; end;

 theorem
    for f being Permutation of the carrier of Lambda(OAS)
    st f is_DIL_of Lambda(OAS) ex f' being Permutation of the carrier of OAS
    st f=f' & f' is_Dil
  proof let f be Permutation of the carrier of Lambda(OAS);
  assume f is_DIL_of Lambda(OAS);
  then A1: f is_FormalIz_of the CONGR of Lambda(OAS) by Def4;
A2:  Lambda(OAS) =
  AffinStruct(#the carrier of OAS, lambda(the CONGR of OAS)#) by DIRAF:def 2;
  then reconsider f'=f as Permutation of the carrier of OAS;
  take f';
  thus thesis by A1,A2,Def8; end;

theorem
   id the carrier of OAS is_Dil
  proof
     now let x,y; (id the carrier of OAS).x = x &
      (id the carrier of OAS).y = y by FUNCT_1:35;
    hence x,y '||' (id the carrier of OAS).x,(id the carrier of OAS).y
       by DIRAF:24; end;
   hence thesis by Th51;
  end;

theorem Th56:
 f is_Dil implies f" is_Dil
  proof assume A1: f is_Dil;
     now let x,y;
     set x'=f".x; set y'=f".y;
       f.x'=x & f.y'=y by Th4; then x',y' '||' x,y by A1,Th51;
     hence x,y '||' f".x,f".y by DIRAF:27; end;
   hence thesis by Th51;
  end;

theorem Th57:
 f is_Dil & g is_Dil implies f*g is_Dil
  proof assume that A1: f is_Dil and A2: g is_Dil;
     now let x,y; set x'=g.x; set y'=g.y;
    A3: (f*g).x= f.x' by FUNCT_2:70; A4: (f*g).y=f.y' by FUNCT_2:70;
A5:    x,y '||' x',y' & x',y' '||' f.x',f.y' by A1,A2,Th51;
      now assume x'=y'; then x=y by FUNCT_2:85;
     hence x,y '||' (f*g).x,(f*g).y by DIRAF:25;
    end;
   hence x,y '||' (f*g).x,(f*g).y by A3,A4,A5,DIRAF:28; end;
  hence thesis by Th51;
  end;

theorem Th58:
f is_Dil implies (for a,b,c,d holds a,b '||' c,d iff f.a,f.b '||' f.c,f.d)
  proof assume A1: f is_Dil; let a,b,c,d;
    A2: a,b '||' f.a,f.b by A1,Th51;
    A3: c,d '||' f.c,f.d by A1,Th51;
    A4: now assume a,b '||' c,d;
         then A5: f.a,f.b '||' c,d or a=b by A2,DIRAF:28;
            now assume A6: f.a,f.b '||' c,d;
               c = d implies f.a,f.b '||' f.c,f.d by DIRAF:25;
           hence f.a,f.b '||' f.c,f.d by A3,A6,DIRAF:28;
          end;
         hence f.a,f.b '||' f.c,f.d by A5,DIRAF:25;
        end;
      now assume A7: f.a,f.b '||' f.c,f.d;
      A8: now assume f.a=f.b; then a=b by FUNCT_2:85;
           hence a,b '||' c,d by DIRAF:25;
          end;
        now assume A9: a,b '||' f.c,f.d;
          now assume f.c = f.d; then c = d by FUNCT_2:85;
         hence a,b '||' c,d by DIRAF:25;
        end;
       hence a,b '||' c,d by A3,A9,DIRAF:28;
      end;
     hence a,b '||' c,d by A2,A7,A8,DIRAF:28;
    end;
   hence thesis by A4;
  end;

theorem Th59:
 f is_Dil implies (for a,b,c holds LIN a,b,c iff LIN f.a,f.b,f.c)
  proof assume A1: f is_Dil; let a,b,c;
      a,b '||' a,c iff f.a,f.b '||' f.a,f.c by A1,Th58;
   hence LIN a,b,c iff LIN f.a,f.b,f.c by DIRAF:def 5;
  end;

theorem Th60:
 f is_Dil & LIN x,f.x,y implies LIN x,f.x,f.y
  proof assume A1: f is_Dil; assume A2: LIN x,f.x,y;
      now assume A3: x<>y;
        x,f.x '||' x,y & x,y '||' f.x,f.y by A1,A2,Th51,DIRAF:def 5;
      then x,f.x '||' f.x,f.y by A3,DIRAF:28;
      then f.x,x '||' f.x,f.y by DIRAF:27;
      then LIN f.x,x,f.y by DIRAF:def 5; hence LIN x,f.x,f.y by DIRAF:36;
    end;
   hence thesis by DIRAF:37;
  end;

theorem Th61:
 a,b '||' c,d implies (a,c '||' b,d or (ex x st LIN a,c,x & LIN b,d,x))
 proof assume A1: a,b '||' c,d;
  assume A2: not a,c '||' b,d;
  A3: now assume a=b; then LIN a,c,a & LIN b,d,a by DIRAF:37;
   hence thesis; end;
     now assume A4: a<>b;
   consider z such that A5: a,b '||' c,z & a,c '||' b,z by DIRAF:31;
   A6: now assume b=z; then b,a '||' b,c by A5,DIRAF:27;
    then LIN b,a,c by DIRAF:def 5; then LIN a,c,b & LIN b,d,b by DIRAF:36,37;
    hence thesis; end;
      now assume A7: b<>z;
      c,d '||' c,z by A1,A4,A5,DIRAF:28; then LIN c,d,z by DIRAF:def 5;
   then LIN d,c,z by DIRAF:36; then d,c '||' d,z by DIRAF:def 5;
   then z,d '||' d,c by DIRAF:27; then consider t such that
   A8: b,d '||' d,t & b,z '||' c,t by A2,A5,DIRAF:32;
     a,c '||' c,t by A5,A7,A8,DIRAF:28;
   then c,a '||' c,t & d,b '||' d,t by A8,DIRAF:27;
   then LIN c,a,t & LIN d,b,t by DIRAF:def 5;
   then LIN a,c,t & LIN b,d,t by DIRAF:36;
   hence thesis; end;
   hence thesis by A6; end;
  hence thesis by A3;
 end;

theorem Th62:
f is_Dil implies ((f=id the carrier of OAS or for x holds f.x<>x) iff
             (for x,y holds x,f.x '||' y,f.y))
  proof assume A1: f is_Dil;
    A2: now assume A3: f=(id the carrier of OAS) or for z holds f.z<>z;
         let x,y; A4: x,y '||' f.x,f.y by A1,Th51;
          A5: now assume f=(id the carrier of OAS); then f.y=y by FUNCT_1:35;
                hence x,f.x '||' y,f.y by DIRAF:25; end;
            now assume A6: for z holds f.z<>z;
            assume A7: not x,f.x '||' y,f.y; then consider z
            such that A8: LIN x,f.x,z & LIN y,f.y,z by A4,Th61;
            set t=f.z; LIN x,f.x,t by A1,A8,Th60;
            then A9: x,f.x '||' z,t by A8,DIRAF:40;
              LIN y,f.y,z & LIN y,f.y,t & y<>f.y by A1,A6,A8,Th60;
            then y,f.y '||' z,t by DIRAF:40;
            then z<>t & z,t '||' y,f.y by A6,DIRAF:27;
           hence contradiction by A7,A9,DIRAF:28;
          end;
         hence x,f.x '||' y,f.y by A3,A5;
        end;
      now assume A10: for x,y holds x,f.x '||' y,f.y;
      assume A11: f<>(id the carrier of OAS);
      given x such that A12: f.x=x;
      consider y such that
      A13: f.y<>(id the carrier of OAS).y by A11,FUNCT_2:113;
      A14:f.y<>y by A13,FUNCT_1:35; x,y '||' f.x,f.y by A1,Th51;
      then A15: LIN x,y,f.y by A12,DIRAF:def 5;
      then A16: LIN y,f.y,x by DIRAF:36; LIN y,x,f.y by A15,DIRAF:36;
      then A17: y,x '||' y,f.y by DIRAF:def 5; x<>y by A12,A13,FUNCT_1:35;
      then consider z such that A18: not LIN x,y,z by DIRAF:43;
        x,z '||' f.x,f.z by A1,Th51; then LIN x,z,f.z by A12,DIRAF:def 5;
      then A19: LIN z,f.z,x by DIRAF:36;
A20:      now assume z=f.z; then z,y '||' z,f.y by A1,Th51;
        then LIN z,y,f.y by DIRAF:def 5;
        then LIN y,f.y,y & LIN y,f.y,z by DIRAF:36,37;
       hence contradiction by A14,A16,A18,DIRAF:38; end;
         LIN z,f.z,z by DIRAF:37;
      then A21: z,f.z '||' x,z by A19,DIRAF:40;
        y,f.y '||' z,f.z by A10; then y,f.y '||' x,z by A20,A21,DIRAF:28;
      then y,x '||' x,z by A14,A17,DIRAF:28;
      then x,y '||' x,z by DIRAF:27;
     hence contradiction by A18,DIRAF:def 5;
    end; hence thesis by A2;
  end;

theorem Th63:
  f is_Dil & f.a=a & f.b=b & not LIN a,b,x implies f.x=x
  proof assume that A1: f is_Dil and A2: f.a=a & f.b=b and A3: not LIN a,b,x;
    assume A4: f.x<>x; a,x '||' a,f.x by A1,A2,Th51;
    then LIN a,x,f.x by DIRAF:def 5; then A5: LIN x,f.x,a by DIRAF:36;
      b,x '||' b,f.x by A1,A2,Th51; then LIN b,x,f.x by DIRAF:def 5;
    then LIN x,f.x,x & LIN x,f.x,b by DIRAF:36,37;
   hence contradiction by A3,A4,A5,DIRAF:38;
  end;

theorem Th64:
f is_Dil & f.a=a & f.b=b & a<>b implies f=(id the carrier of OAS)
  proof assume that A1: f is_Dil and A2: f.a=a & f.b=b & a<>b;
      now let x;
     A3:  not LIN a,b,x implies f.x=x by A1,A2,Th63;
       now assume A4: LIN a,b,x;
        now assume A5: x<>a; consider z such that
       A6: not LIN a,b,z by A2,DIRAF:43;
       A7: f.z=z by A1,A2,A6,Th63;
         not LIN a,z,x
       proof assume LIN a,z,x;
         then LIN a,x,a & LIN a,x,z & LIN a,x,b by A4,DIRAF:36,37;
        hence contradiction by A5,A6,DIRAF:38;
       end;
      hence f.x=x by A1,A2,A7,Th63;
      end;
      hence f.x=x by A2;
     end;
     hence f.x=(id the carrier of OAS).x by A3,FUNCT_1:35;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
    f is_Dil & g is_Dil & f.a=g.a & f.b=g.b implies a=b or f=g
  proof assume that A1: f is_Dil & g is_Dil and
     A2: f.a=g.a & f.b=g.b;
    assume A3: a<>b; A4: (g"*f).a=g".(g.a) by A2,FUNCT_2:70 .=a by Th4;
    A5: (g"*f).b=g".(g.b) by A2,FUNCT_2:70
    .=b by Th4;
      g" is_Dil by A1,Th56; then g"*f is_Dil by A1,Th57;
    then A6: g"*f=(id the carrier of OAS) by A3,A4,A5,Th64;
      now let x; g".(f.x)=(g"*f).x by FUNCT_2:70;
      then g".(f.x)=x by A6,FUNCT_1:35;
     hence g.x=f.x by Th4;
    end;
   hence thesis by FUNCT_2:113;
  end;

definition let OAS; let f be Permutation of the carrier of OAS;
  attr f is translation means
  :Def9: f is_Dil & (f = id the carrier of OAS or for a holds a<>f.a);
  synonym f is_Tr;
end;

canceled;

theorem
Th67: f is_Dil implies (f is_Tr iff (for x,y holds x,f.x '||' y,f.y))
  proof assume A1: f is_Dil;
    then (f=id the carrier of OAS or for x holds f.x<>x) iff
             (for x,y holds x,f.x '||' y,f.y) by Th62;
   hence thesis by A1,Def9;
  end;

canceled;

theorem Th69:
  f is_Tr & g is_Tr & f.a=g.a & not LIN a,f.a,x implies f.x=g.x
  proof assume that A1: f is_Tr & g is_Tr and A2: f.a=g.a and
A3: not LIN a,f.a,x;
    A4: f is_Dil & g is_Dil by A1,Def9;
    set b=f.a, y=f.x, z=g.x;
    A5: a,x '||' b,y & a,b '||' x,y by A1,A4,Th51,Th67;
      a,x '||' b,z & a,b '||' x,z by A1,A2,A4,Th51,Th67;
   hence f.x=g.x by A3,A5,PASCH:12;
  end;

theorem Th70:
f is_Tr & g is_Tr & f.a=g.a implies f=g
  proof assume that
    A1: f is_Tr and A2: g is_Tr and A3: f.a=g.a;
    A4: f is_Dil by A1,Def9;
    set b=f.a;
    A5: now assume b=a;
          then f=id the carrier of OAS &
            g=id the carrier of OAS by A1,A2,A3,Def9;
         hence thesis;
        end;
      now assume A6: a<>b;
        for x holds f.x=g.x
        proof let x;
            now assume A7: LIN a,b,x;
              now assume x<>a; consider p such that
              A8: not LIN a,b,p by A6,DIRAF:43;
              A9: f.p=g.p by A1,A2,A3,A8,Th69;
                f<>(id the carrier of OAS) by A6,FUNCT_1:35;
              then A10: f.p<>p & f.x<>x by A1,Def9;
                not LIN p,f.p,x
                proof assume LIN p,f.p,x;
                  then LIN p,f.p,x & LIN p,f.p,f.x & LIN p,f.p,p
                                                  by A4,Th60,DIRAF:37;
                  then A11: LIN x,f.x,p by A10,DIRAF:38;
                  A12: LIN a,b,f.x by A4,A7,Th60;
                    LIN a,b,a by DIRAF:37;
                  then A13: LIN x,f.x,a by A6,A7,A12,DIRAF:38;
                    LIN a,b,b by DIRAF:37;
                  then LIN x,f.x,b by A6,A7,A12,DIRAF:38;
                 hence contradiction by A8,A10,A11,A13,DIRAF:38;
                end;
             hence f.x=g.x by A1,A2,A9,Th69;
            end;
           hence f.x=g.x by A3;
          end;
         hence f.x=g.x by A1,A2,A3,Th69;
        end;
       hence thesis by FUNCT_2:113;
      end;
     hence thesis by A5;
  end;

theorem Th71:
 f is_Tr implies f" is_Tr
  proof assume A1: f is_Tr; then f is_Dil by Def9;
    then A2: f" is_Dil by Th56;
A3: f=(id the carrier of OAS) implies f"=(id the carrier of OAS) by FUNCT_1:67;
      now assume A4: for x holds f.x<>x;
      given y such that A5: f".y=y;
        f.y=y by A5,Th4;
     hence contradiction by A4;
    end;
   hence thesis by A1,A2,A3,Def9;
  end;

theorem
   f is_Tr & g is_Tr implies (f*g) is_Tr
  proof assume that A1: f is_Tr and A2: g is_Tr;
    A3: f is_Dil by A1,Def9; g is_Dil by A2,Def9;
    then A4: (f*g) is_Dil by A3,Th57;
      now assume A5: (f*g)<>(id the carrier of OAS);
        for x holds (f*g).x<>x
        proof given x such that
          A6: (f*g).x=x; f.(g.x)=x by A6,FUNCT_2:70;
          then g.x=f".x & f" is_Tr by A1,Th4,Th71;
          then f*g=f*f" by A2,Th70;
         hence contradiction by A5,FUNCT_2:88;
        end;
     hence thesis by A4,Def9;
    end;
   hence thesis by A4,Def9;
  end;

Lm5:
 f is_Tr & not LIN a,f.a,b implies
         a,b // f.a,f.b & a,f.a // b,f.b
  proof assume that A1: f is_Tr and A2: not LIN a,f.a,b;
    A3: f is_Dil by A1,Def9; then A4: a,b '||' f.a,f.b by Th51;
      a,f.a '||' b,f.b by A1,A3,Th67;
   hence a,b // f.a,f.b & a,f.a // b,f.b by A2,A4,PASCH:21;
  end;

Lm6: f is_Tr & a<>f.a & LIN a,f.a,b implies a,f.a // b,f.b
  proof assume that A1: f is_Tr and A2: a<>f.a and
    A3: LIN a,f.a,b;
    A4: f is_Dil by A1,Def9; consider p such that
    A5: not LIN a,f.a,p by A2,DIRAF:43; f<>(id the carrier of OAS) by A2,
FUNCT_1:35;
    then A6: p<>f.p & b<>f.b by A1,Def9;
    A7: not LIN p,f.p,a
      proof assume LIN p,f.p,a;
        then LIN p,f.p,p & LIN p,f.p,a & LIN p,f.p,f.a by A4,Th60,DIRAF:37;
       hence contradiction by A5,A6,DIRAF:38;
      end;
   A8: not LIN p,f.p,b
      proof assume A9: LIN p,f.p,b;
          LIN a,f.a,b & LIN a,f.a,f.b & LIN a,f.a,a by A3,A4,Th60,DIRAF:37;
        then LIN b,f.b,a by A2,DIRAF:38;
        then A10: LIN b,f.b,f.a & LIN b,f.b,a by A4,Th60;
        A11: LIN p,f.p,f.b by A4,A9,Th60; LIN p,f.p,p by DIRAF:37;
        then LIN b,f.b,p by A6,A9,A11,DIRAF:38;
       hence contradiction by A5,A6,A10,DIRAF:38;
      end;
    A12: p,a // f.p,f.a & p,f.p // a,f.a by A1,A7,Lm5;
       p,b // f.p,f.b & p,f.p // b,f.b by A1,A8,Lm5;
   hence a,f.a // b,f.b by A6,A12,ANALOAF:def 5;
  end;

Lm7: f is_Tr & Mid a,f.a,b & a<>f.a implies a,b // f.a,f.b
 proof assume that A1: f is_Tr and A2: Mid a,f.a,b and A3: a<>f.a;
A4:   LIN a,f.a,b by A2,DIRAF:34; then A5: a,f.a // b,f.b by A1,A3,Lm6;
    now assume A6: b<>f.a; Mid b,f.a,a by A2,DIRAF:13;
   then b,f.a // f.a,a by DIRAF:def 3; then b,f.a // b,a by ANALOAF:def 5;
   then A7: a,b // f.a,b by DIRAF:5;
     a,f.a // f.a,b by A2,DIRAF:def 3; then f.a,b // b,f.b by A3,A5,ANALOAF:def
5
;
   then f.a,b // f.a,f.b by ANALOAF:def 5;
   hence a,b // f.a,f.b by A6,A7,DIRAF:6; end;
 hence thesis by A1,A3,A4,Lm6; end;

Lm8: f is_Tr & a<>f.a & b<>f.a & Mid a,b,f.a implies a,b // f.a,f.b
 proof assume A1: f is_Tr & a<>f.a & b<>f.a & Mid a,b,f.a;
  then A2: f<>(id the carrier of OAS) by FUNCT_1:35;
  A3: f is_Dil by A1,Def9; A4: LIN a,b,f.a by A1,DIRAF:34;
  then A5: LIN a,f.a,b by DIRAF:36;
  A6: a,b // b,f.a by A1,DIRAF:def 3;
     now assume A7: a<>b;
A8:   a,b '||' f.a,f.b by A3,Th51;
     now assume A9: a,b // f.b,f.a;
    A10: Mid f.a,f.b,b proof a,b // a,f.a & a,f.a // b,f.b by A1,A5,A6,Lm6,
ANALOAF:def 5; then a,b // b,f.b by A1,DIRAF:6;
      then b,f.b // f.b,f.a by A7,A9,ANALOAF:def 5
; then Mid b,f.b,f.a by DIRAF:def 3;
      hence thesis by DIRAF:13; end;
    consider q such that A11: not LIN a,f.a,q by A1,DIRAF:43;
    consider x such that A12: q,b // b,x & q,a // f.a,x by A6,A7,ANALOAF:def 5;
    A13: x<>f.a proof assume x=f.a;
     then Mid q,b,f.a by A12,DIRAF:def 3; then LIN q,b,f.a by DIRAF:34;
     then LIN f.a,b,q & LIN f.a,b,a & LIN f.a,b,b by A4,DIRAF:36,37;
     then LIN a,b,q & LIN a,b,f.a & LIN a,b,a by A1,DIRAF:36,38;
     hence contradiction by A7,A11,DIRAF:38; end;
    A14: not LIN x,f.a,b proof assume LIN x,f.a,b; then LIN
 f.a,x,b by DIRAF:36;
     then f.a,x '||' f.a,b & q,a '||' f.a,x by A12,DIRAF:def 4,def 5;
     then f.a,b '||' q,a & LIN f.a,b,a by A4,A13,DIRAF:28,36;
     then f.a,b '||' q,a & f.a,b '||' f.a,a by DIRAF:def 5;
     then f.a,a '||' q,a by A1,DIRAF:28; then a,f.a '||' a,q by DIRAF:27;
     hence contradiction by A11,DIRAF:def 5; end;
    A15: a,q // f.a,f.q & a,f.a // q,f.q & a<>q by A1,A11,Lm5,DIRAF:37;
      Mid q,b,x by A12,DIRAF:def 3;
    then A16: Mid x,b,q by DIRAF:13;
    A17: LIN x,f.a,f.q proof a,q // x,f.a by A12,DIRAF:5;
     then f.a,f.q // x,f.a by A15,ANALOAF:def 5
; then f.a,f.q '||' f.a,x by DIRAF:def 4;
     then LIN f.a,f.q,x by DIRAF:def 5; hence thesis by DIRAF:36; end;
       f.a,b '||' q,f.q proof LIN f.a,a,b by A4,DIRAF:36;
     then f.a,a '||' f.a,b by DIRAF:def 5;
     then a,f.a '||' b,f.a & a,f.a '||' q,f.q by A15,DIRAF:27,def 4;
     then b,f.a '||' q,f.q by A1,DIRAF:28; hence thesis by DIRAF:27; end;
    then Mid x,f.a,f.q by A14,A16,A17,PASCH:15; then consider y such that
    A18: Mid x,y,b & Mid y,f.b,f.q by A10,A14,PASCH:35;
    A19: LIN x,y,b & LIN y,f.b,f.q by A18,DIRAF:34;
    A20: LIN b,f.b,a & LIN b,f.b,f.a
     proof A21: LIN a,f.a,f.b & LIN a,f.a,a by A3,A5,Th60,DIRAF:37;
      hence LIN b,f.b,a by A1,A5,DIRAF:38; LIN a,f.a,f.a by DIRAF:37;
      hence LIN b,f.b,f.a by A1,A5,A21,DIRAF:38; end;
    A22: b<>f.b by A1,A2,Def9;
    then A23: not LIN b,f.b,q by A11,A20,DIRAF:38;
    A24: not LIN b,f.b,f.q proof assume LIN b,f.b,f.q;
     then LIN b,f.b,f.q & b,f.b '||' q,f.q by A1,A3,Th67;
     then LIN b,f.b,f.q & b,f.b '||' f.q,q by DIRAF:27;
     hence contradiction by A22,A23,DIRAF:39; end;
    A25: x<>b by A14,DIRAF:37;
A26:LIN x,b,q & LIN x,b,y & LIN x,b,b by A16,A19,DIRAF:34,36,37;
    then A27: LIN y,b,q by A25,DIRAF:38;
    A28: f.b<>f.q & b<>q by A24,DIRAF:37;
    A29: b,q '||' f.b,f.q by A3,Th51;
      LIN f.b,f.q,y & LIN b,q,y by A19,A25,A26,DIRAF:36,38;
    then f.b,f.q '||' f.b,y & b,q '||' b,y by DIRAF:def 5;
    then b,q '||' f.b,y & b,q '||' b,y by A28,A29,DIRAF:28;
    then f.b,y '||' b,y by A28,DIRAF:28; then y,b '||' y,f.b by DIRAF:27;
    then LIN y,b,f.b & LIN y,b,b by DIRAF:37,def 5;
    hence contradiction by A19,A23,A24,A27,DIRAF:38; end;
   hence thesis by A8,DIRAF:def 4; end;
  hence thesis by DIRAF:7;
 end;

Lm9: f is_Tr & a<>f.a & LIN a,f.a,b implies a,b // f.a,f.b
 proof assume A1: f is_Tr & a<>f.a & LIN a,f.a,b;
   then f<>(id the carrier of OAS) by FUNCT_1:35;
  then A2: b<>f.b by A1,Def9;
  A3: f is_Dil by A1,Def9;
     now assume A4: a<>b;
   A5:  Mid a,f.a,b implies thesis by A1,Lm7;
   A6: now assume A7: Mid f.a,a,b;
      LIN a,f.a,f.b & LIN a,f.a,a by A1,A3,Th60,DIRAF:37;
then A8:    LIN b,f.b,a by A1,DIRAF:38;
    A9: now assume Mid b,f.b,a; then b,a // f.b,f.a by A1,A2,Lm7;
     hence thesis by DIRAF:5; end;
    A10: now assume Mid b,a,f.b; then A11: b,a // f.b,f.a or a=f.b
    by A1,A2,Lm8;
       now assume a=f.b; then a=f.b & a,f.a // b,f.b by A1,Lm6;
      hence thesis by DIRAF:5; end;
     hence thesis by A11,DIRAF:5; end;
       now assume Mid f.b,b,a; then Mid a,b,f.b & Mid b,a,f.a by A7,DIRAF:13;
     then a,b // b,f.b & b,a // a,f.a by DIRAF:def 3;
     then A12: a,b // a,f.b & a,b // f.a,a by ANALOAF:def 5;
     then f.a,a // a,f.b by A4,ANALOAF:def 5;
     then f.a,a // f.a,f.b by ANALOAF:def 5;
     hence thesis by A12,DIRAF:6; end;
     hence thesis by A8,A9,A10,DIRAF:35; end;
      now assume A13: Mid a,b,f.a;
         b=f.a implies thesis by A1,Lm6;
    hence thesis by A1,A13,Lm8; end;
   hence thesis by A1,A5,A6,DIRAF:35; end;
  hence thesis by DIRAF:7;
 end;

theorem
Th73: f is_Tr implies f is_CDil
  proof assume A1: f is_Tr;
    A2:  f=id the carrier of OAS implies thesis by Th44;
      now assume A3: for x holds f.x<>x;
        for a,b holds a,b // f.a,f.b
        proof let a,b; A4: a<>f.a by A3;
            not LIN a,f.a,b implies a,b // f.a,f.b by A1,Lm5;
        hence a,b // f.a,f.b by A1,A4,Lm9; end;
     hence thesis by Th42; end;
   hence thesis by A1,A2,Def9; end;

theorem
Th74: f is_Dil & f.p=p & Mid q,p,f.q & not LIN p,q,x
                                         implies Mid x,p,f.x
  proof assume that A1: f is_Dil and
    A2: f.p=p and A3: Mid q,p,f.q and A4: not LIN p,q,x;
      p,x '||' p,f.x by A1,A2,Th51;
    then A5: LIN p,x,f.x by DIRAF:def 5; q,x '||' f.q,f.x by A1,Th51;
    then q,x '||' f.x,f.q by DIRAF:27;
   hence Mid x,p,f.x by A3,A4,A5,PASCH:13;
  end;

theorem
Th75: f is_Dil & f.p=p & Mid q,p,f.q & q<>p implies Mid x,p,f.x
  proof assume that A1: f is_Dil and
    A2: f.p=p and A3: Mid q,p,f.q and A4: q<>p;
      now assume A5: LIN p,q,x; consider r such that
      A6: not LIN p,q,r by A4,DIRAF:43;
      A7: Mid r,p,f.r by A1,A2,A3,A6,Th74;
         x=p or not LIN p,r,x
        proof assume A8: x<>p & LIN p,r,x;
          then LIN p,x,r & LIN p,x,q & LIN p,x,p by A5,DIRAF:36,37;
         hence contradiction by A6,A8,DIRAF:38;
        end;
     hence thesis by A1,A2,A7,Th74,DIRAF:14;
    end;
   hence thesis by A1,A2,A3,Th74;
  end;

theorem Th76:
 f is_Dil & f.p=p & q<>p & Mid q,p,f.q & not LIN p,x,y
                                     implies x,y // f.y,f.x
  proof assume A1: f is_Dil;
   then A2: x,y '||' f.x,f.y by Th51;
    assume f.p=p & q<>p & Mid q,p,f.q;
    then Mid x,p,f.x & Mid y,p,f.y by A1,Th75;
    then x,p // p,f.x & y,p // p,f.y by DIRAF:def 3;
   hence thesis by A2,PASCH:19;
  end;

theorem
Th77: f is_Dil & f.p=p & q<>p & Mid q,p,f.q & LIN p,x,y
                                    implies x,y // f.y,f.x
  proof assume that A1: f is_Dil and
    A2: f.p=p and A3: q<>p and A4: Mid q,p,f.q and A5: LIN p,x,y;
    A6: Mid x,p,f.x by A1,A2,A3,A4,Th75;
    A7: Mid y,p,f.y by A1,A2,A3,A4,Th75;
    A8: now assume A9: x=p; then y,x // x,f.y by A7,DIRAF:def 3;
          hence thesis by A2,A9,DIRAF:5; end;
      now assume A10: x<>p & y<>p & x<>y; then consider u such that
      A11: not LIN p,x,u by DIRAF:43; consider r such that
      A12: x,y '||' u,r and A13: x,u '||' y,r by DIRAF:31;
      A14: not LIN x,y,u
        proof assume LIN x,y,u;
          then LIN x,y,u & LIN x,y,p & LIN x,y,x by A5,DIRAF:36,37;
         hence contradiction by A10,A11,DIRAF:38;
        end;
      then A15: x,y // u,r by A12,A13,PASCH:21;
      A16: not LIN p,u,r
        proof
A17:      now assume u=r;
            then u,x '||' u,y by A13,DIRAF:27;
            then LIN u,x,y by DIRAF:def 5;
           hence contradiction by A14,DIRAF:36;
          end;
          assume LIN p,u,r; then A18: LIN u,r,p by DIRAF:36;
            LIN x,y,p by A5,DIRAF:36; then x,y '||' x,p by DIRAF:def 5;
          then x,y '||' p,x by DIRAF:27;
          then A19: u,r '||' p,x by A10,A12,DIRAF:28;
          then A20: LIN u,r,x by A17,A18,DIRAF:39;
            p,x '||' p,y by A5,DIRAF:def 5;
          then u,r '||' p,y by A10,A19,DIRAF:28;
          then LIN u,r,y & LIN u,r,u by A17,A18,DIRAF:37,39;
         hence contradiction by A14,A17,A20,DIRAF:38;
        end;
      then A21: u,r // f.r,f.u by A1,A2,A3,A4,Th76;
      set u'=f.u, r'=f.r, x'=f.x, y'=f.y;
        x',y' '||' u',r' & x',u' '||' y',r' & not LIN x',y',u'
                                             by A1,A12,A13,A14,Th58,Th59;
      then x',y' // u',r' by PASCH:21;
      then A22: r',u' // y',x' by DIRAF:5; A23: u<>r by A16,DIRAF:37;
      then A24: u<>r & u'<>r' by FUNCT_2:85;
        x,y // r',u' by A15,A21,A23,DIRAF:6;
     hence thesis by A22,A24,DIRAF:6;
    end;
   hence thesis by A2,A6,A8,DIRAF:7,def 3;
  end;

theorem
Th78: f is_Dil & f.p=p & q<>p & Mid q,p,f.q implies f is_SDil
  proof assume that A1: f is_Dil and
    A2: f.p=p and A3: q<>p and A4: Mid q,p,f.q;
      x,y // f.y,f.x
      proof not LIN p,x,y implies
                        x,y // f.y,f.x by A1,A2,A3,A4,Th76;
       hence x,y // f.y,f.x by A1,A2,A3,A4,Th77;
      end;
   hence thesis by Def7;
  end;

theorem
Th79: f is_Dil & f.p=p & (for x holds p,x // p,f.x) implies
                               (for y,z holds y,z // f.y,f.z)
  proof assume that A1: f is_Dil and A2: f.p=p and
    A3: p,x // p,f.x;
    A4: not LIN p,y,z implies y,z // f.y,f.z
      proof assume A5: not LIN p,y,z;
          p,y // p,f.y & p,z // p,f.z & y,z '||' f.y,f.z by A1,A3,Th51;
       hence y,z // f.y,f.z by A5,PASCH:20;
      end;
    let y,z;
      LIN p,y,z implies y,z // f.y,f.z
      proof assume A6: LIN p,y,z;
        A7: now assume p=z; then z,y // f.z,f.y by A2,A3;
             hence y,z // f.y,f.z by DIRAF:5;
            end;
          now assume A8: p<>y & y<>z & z<>p;
          then consider q such that
          A9: not LIN p,y,q by DIRAF:43; consider r such that
          A10: y,z '||' q,r and A11: y,q '||' z,r by DIRAF:31;
          A12: not LIN y,z,q
            proof assume LIN y,z,q;
              then LIN y,z,q & LIN y,z,p & LIN y,z,y by A6,DIRAF:36,37;
             hence contradiction by A8,A9,DIRAF:38;
            end;
          then A13: y,z // q,r by A10,A11,PASCH:21;
          A14: q<>r
            proof assume q=r;
              then q,y '||' q,z by A11,DIRAF:27; then LIN q,y,z by DIRAF:def 5;
             hence contradiction by A12,DIRAF:36;
            end;
          then A15: f.q<>f.r by FUNCT_2:85;
             not LIN p,q,r
            proof assume LIN p,q,r; then A16: LIN q,r,p by DIRAF:36;
                LIN y,p,z by A6,DIRAF:36; then y,p '||' y,z by DIRAF:def 5;
              then y,z '||' p,y by DIRAF:27;
              then q,r '||' p,y by A8,A10,DIRAF:28;
              then LIN q,r,y & LIN q,r,q by A14,A16,DIRAF:37,39;
             hence contradiction by A9,A14,A16,DIRAF:38;
            end;
          then A17: q,r // f.q,f.r by A4;
          A18: f.y,f.z '||' f.q,f.r by A1,A10,Th58;
          A19: f.y,f.q '||' f.z,f.r by A1,A11,Th58;
             not LIN f.y,f.z,f.q by A1,A12,Th59;
          then f.y,f.z // f.q,f.r by A18,A19,PASCH:21;
          then A20: f.q,f.r // f.y,f.z by DIRAF:5;
            y,z // f.q,f.r by A13,A14,A17,DIRAF:6;
         hence y,z // f.y,f.z by A15,A20,DIRAF:6;
        end;
      hence thesis by A2,A3,A7,DIRAF:7;
     end;
   hence thesis by A4;
  end;

theorem
   f is_Dil implies f is_CDil or f is_SDil
  proof assume A1: f is_Dil;
    A2: now assume for x holds f.x<>x; then f is_Tr by A1,Def9;
        hence f is_CDil by Th73;
       end;
      now given p such that A3: f.p=p;
      A4: now assume for x holds p,x // p,f.x;
            then for x,y holds x,y // f.x,f.y by A1,A3,Th79;
           hence f is_CDil by Th42;
          end;
        now given q such that
        A5: not p,q // p,f.q;
          p,q '||' p,f.q by A1,A3,Th51; then p,q // f.q,p by A5,DIRAF:def 4;
        then q,p // p,f.q by DIRAF:5;
        then Mid q,p,f.q & p<>q by A5,DIRAF:def 3;
       hence f is_SDil by A1,A3,Th78;
      end;
     hence thesis by A4;
    end;
   hence thesis by A2;
  end;

reserve AFS for AffinSpace;
reserve a,b,c,d,d1,d2,p,x,y,z,t for Element of AFS;

canceled;

theorem Th82: AFS is CongrSpace-like
 proof
  thus for x,y,z,t,a,b st x,y // a,b & a,b // z,t & a<>b
                                           holds x,y // z,t by AFF_1:14;
  thus for x,y,z holds x,x // y,z by AFF_1:12;
  thus for x,y,z,t st x,y // z,t holds z,t // x,y by AFF_1:13;
  thus for x,y holds x,y // x,y by AFF_1:11;
 end;

theorem Lambda(OAS) is CongrSpace proof Lambda(OAS) is AffinSpace
 by DIRAF:48; hence thesis by Th82; end;

reserve f,g for Permutation of the carrier of AFS;

definition let AFS; let f;
  attr f is dilatation means
  :Def10: f is_DIL_of AFS;
  synonym f is_Dil;
end;

canceled;

theorem Th85:
  f is_Dil iff (for a,b holds a,b // f.a,f.b)
  proof thus f is_Dil implies (for a,b holds a,b // f.a,f.b)
   proof assume f is_Dil; then A1: f is_DIL_of AFS by Def10;
    let a,b;
    thus a,b // f.a,f.b by A1,Th35;
   end;
   assume for a,b holds a,b // f.a,f.b;
    then f is_DIL_of AFS by Th35;
    hence thesis by Def10;
   end;

theorem Th86:
 id the carrier of AFS is_Dil
  proof
     now let x,y; (id the carrier of AFS).x = x &
      (id the carrier of AFS).y = y by FUNCT_1:35;
    hence x,y // (id the carrier of AFS).x,(id the carrier of AFS).y
       by AFF_1:11; end;
   hence thesis by Th85;
  end;

theorem Th87:
 f is_Dil implies f" is_Dil
  proof assume A1: f is_Dil;
     now let x,y;
     set x'=f".x; set y'=f".y;
       f.x'=x & f.y'=y by Th4; then x',y' // x,y by A1,Th85;
     hence x,y // f".x,f".y by AFF_1:13; end;
   hence thesis by Th85;
  end;

theorem Th88:
 f is_Dil & g is_Dil implies (f*g) is_Dil
  proof assume that A1: f is_Dil and A2: g is_Dil;
     now let x,y; set x'=g.x; set y'=g.y;
    A3: (f*g).x= f.x' by FUNCT_2:70; A4: (f*g).y=f.y' by FUNCT_2:70;
A5:    x,y // x',y' & x',y' // f.x',f.y' by A1,A2,Th85;
      now assume x'=y'; then x=y by FUNCT_2:85;
     hence x,y // (f*g).x,(f*g).y by AFF_1:12;
    end;
   hence x,y // (f*g).x,(f*g).y by A3,A4,A5,AFF_1:14; end;
  hence thesis by Th85;
  end;

theorem Th89:
f is_Dil implies (for a,b,c,d holds a,b // c,d iff f.a,f.b // f.c,f.d)
  proof assume A1: f is_Dil; let a,b,c,d;
    A2: a,b // f.a,f.b by A1,Th85;
    A3: c,d // f.c,f.d by A1,Th85;
    A4: now assume a,b // c,d;
         then A5: f.a,f.b // c,d or a=b by A2,AFF_1:14;
            now assume A6: f.a,f.b // c,d;
               c = d implies f.a,f.b // f.c,f.d by AFF_1:12;
           hence f.a,f.b // f.c,f.d by A3,A6,AFF_1:14;
          end;
         hence f.a,f.b // f.c,f.d by A5,AFF_1:12;
        end;
      now assume A7: f.a,f.b // f.c,f.d;
      A8: now assume f.a=f.b; then a=b by FUNCT_2:85;
           hence a,b // c,d by AFF_1:12;
          end;
        now assume A9: a,b // f.c,f.d;
          now assume f.c = f.d; then c = d by FUNCT_2:85;
         hence a,b // c,d by AFF_1:12;
        end;
       hence a,b // c,d by A3,A9,AFF_1:14;
      end;
     hence a,b // c,d by A2,A7,A8,AFF_1:14;
    end;
   hence thesis by A4;
  end;

theorem
   f is_Dil implies (for a,b,c holds LIN a,b,c iff LIN f.a,f.b,f.c)
  proof assume A1: f is_Dil; let a,b,c;
      a,b // a,c iff f.a,f.b // f.a,f.c by A1,Th89;
   hence LIN a,b,c iff LIN f.a,f.b,f.c by AFF_1:def 1;
  end;

theorem Th91:
 f is_Dil & LIN x,f.x,y implies LIN x,f.x,f.y
  proof assume A1: f is_Dil; assume A2: LIN x,f.x,y;
      now assume A3: x<>y;
        x,f.x // x,y & x,y // f.x,f.y by A1,A2,Th85,AFF_1:def 1;
      then x,f.x // f.x,f.y by A3,AFF_1:14;
      then f.x,x // f.x,f.y by AFF_1:13;
      then LIN f.x,x,f.y by AFF_1:def 1; hence LIN x,f.x,f.y by AFF_1:15;
    end;
   hence thesis by AFF_1:16;
  end;

theorem Th92:
 a,b // c,d implies (a,c // b,d or (ex x st LIN a,c,x & LIN b,d,x))
 proof assume A1: a,b // c,d;
  assume A2: not a,c // b,d;
  A3: now assume a=b; then LIN a,c,a & LIN b,d,a by AFF_1:16;
   hence thesis; end;
     now assume A4: a<>b;
   consider z such that A5: a,b // c,z & a,c // b,z by DIRAF:47;
   A6: now assume b=z; then b,a // b,c by A5,AFF_1:13;
    then LIN b,a,c by AFF_1:def 1; then LIN a,c,b & LIN b,d,b by AFF_1:15,16;
    hence thesis; end;
      now assume A7: b<>z;
      c,d // c,z by A1,A4,A5,AFF_1:14; then LIN c,d,z by AFF_1:def 1;
   then LIN d,c,z by AFF_1:15; then d,c // d,z by AFF_1:def 1;
   then z,d // d,c by AFF_1:13; then consider t such that
   A8: b,d // d,t & b,z // c,t by A2,A5,DIRAF:47;
     a,c // c,t by A5,A7,A8,AFF_1:14;
   then c,a // c,t & d,b // d,t by A8,AFF_1:13;
   then LIN c,a,t & LIN d,b,t by AFF_1:def 1;
   then LIN a,c,t & LIN b,d,t by AFF_1:15;
   hence thesis; end;
   hence thesis by A6; end;
  hence thesis by A3;
 end;

theorem Th93:
f is_Dil implies ((f=id the carrier of AFS or for x holds f.x<>x) iff
             (for x,y holds x,f.x // y,f.y))
  proof assume A1: f is_Dil;
    A2: now assume A3: f=id the carrier of AFS or for z holds f.z<>z;
         let x,y; A4: x,y // f.x,f.y by A1,Th85;
          A5: now assume f=(id the carrier of AFS); then f.y=y by FUNCT_1:35;
                hence x,f.x // y,f.y by AFF_1:12; end;
            now assume A6: for z holds f.z<>z;
            assume A7: not x,f.x // y,f.y; then consider z
            such that A8: LIN x,f.x,z & LIN y,f.y,z by A4,Th92;
            set t=f.z; LIN x,f.x,t by A1,A8,Th91;
            then A9: x,f.x // z,t by A8,AFF_1:19;
              LIN y,f.y,z & LIN y,f.y,t & y<>f.y by A1,A6,A8,Th91;
            then y,f.y // z,t by AFF_1:19;
            then z<>t & z,t // y,f.y by A6,AFF_1:13;
           hence contradiction by A7,A9,AFF_1:14;
          end;
         hence x,f.x // y,f.y by A3,A5;
        end;
      now assume A10: for x,y holds x,f.x // y,f.y;
      assume A11: f<>(id the carrier of AFS);
      given x such that A12: f.x=x;
      consider y such that
      A13: f.y<>(id the carrier of AFS).y by A11,FUNCT_2:113;
      A14:f.y<>y by A13,FUNCT_1:35; x,y // f.x,f.y by A1,Th85;
      then A15: LIN x,y,f.y by A12,AFF_1:def 1;
      then A16: LIN y,f.y,x by AFF_1:15; LIN y,x,f.y by A15,AFF_1:15;
      then A17: y,x // y,f.y by AFF_1:def 1; x<>y by A12,A13,FUNCT_1:35;
      then consider z such that A18: not LIN x,y,z by AFF_1:22;
        x,z // f.x,f.z by A1,Th85; then LIN x,z,f.z by A12,AFF_1:def 1;
      then A19: LIN z,f.z,x by AFF_1:15;
A20:      now assume z=f.z; then z,y //z,f.y by A1,Th85;
        then LIN z,y,f.y by AFF_1:def 1;
        then LIN y,f.y,y & LIN y,f.y,z by AFF_1:15,16;
       hence contradiction by A14,A16,A18,AFF_1:17; end;
         LIN z,f.z,z by AFF_1:16;
      then A21: z,f.z // x,z by A19,AFF_1:19;
        y,f.y // z,f.z by A10; then y,f.y // x,z by A20,A21,AFF_1:14;
      then y,x // x,z by A14,A17,AFF_1:14;
      then x,y // x,z by AFF_1:13;
     hence contradiction by A18,AFF_1:def 1;
    end; hence thesis by A2;
  end;

theorem Th94:
  f is_Dil & f.a=a & f.b=b & not LIN a,b,x implies f.x=x
  proof assume that A1: f is_Dil and
    A2: f.a=a & f.b=b and A3: not LIN a,b,x;
    assume A4: f.x<>x; a,x // a,f.x by A1,A2,Th85;
    then LIN a,x,f.x by AFF_1:def 1; then A5: LIN x,f.x,a by AFF_1:15;
      b,x // b,f.x by A1,A2,Th85; then LIN b,x,f.x by AFF_1:def 1;
    then LIN x,f.x,x & LIN x,f.x,b by AFF_1:15,16;
   hence contradiction by A3,A4,A5,AFF_1:17;
  end;

theorem Th95:
  f is_Dil & f.a=a & f.b=b & a<>b implies f=id the carrier of AFS
  proof assume that A1: f is_Dil and A2: f.a=a & f.b=b & a<>b;
      now let x;
     A3:  not LIN a,b,x implies f.x=x by A1,A2,Th94;
       now assume A4: LIN a,b,x;
        now assume A5: x<>a; consider z such that
       A6: not LIN a,b,z by A2,AFF_1:22;
       A7: f.z=z by A1,A2,A6,Th94;
         not LIN a,z,x
       proof assume LIN a,z,x;
         then LIN a,x,a & LIN a,x,z & LIN a,x,b by A4,AFF_1:15,16;
        hence contradiction by A5,A6,AFF_1:17;
       end;
      hence f.x=x by A1,A2,A7,Th94;
      end;
      hence f.x=x by A2;
     end;
     hence f.x=(id the carrier of AFS).x by A3,FUNCT_1:35;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
  f is_Dil & g is_Dil & f.a=g.a & f.b=g.b implies a=b or f=g
  proof assume that A1: f is_Dil & g is_Dil and
     A2: f.a=g.a & f.b=g.b;
    assume A3: a<>b; A4: (g"*f).a=g".(g.a) by A2,FUNCT_2:70 .=a by Th4;
    A5: (g"*f).b=g".(g.b) by A2,FUNCT_2:70 .=b by Th4;
      g" is_Dil by A1,Th87; then g"*f is_Dil by A1,Th88;
    then A6: g"*f=(id the carrier of AFS) by A3,A4,A5,Th95;
      now let x; g".(f.x)=(g"*f).x by FUNCT_2:70;
      then g".(f.x)=x by A6,FUNCT_1:35;
     hence g.x=f.x by Th4;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem Th97:
 not LIN a,b,c & a,b // c,d1 & a,b // c,d2 & a,c // b,d1 &
       a,c // b,d2 implies d1=d2
  proof assume that A1: not LIN a,b,c and A2: a,b // c,d1 and
     A3: a,b // c,d2 and A4: a,c // b,d1 and A5: a,c // b,d2;
   assume A6: d1<>d2; A7: a<>b & a<>c by A1,AFF_1:16;
   then A8: c,d1 // c,d2 by A2,A3,AFF_1:14;
      b,d1 // b,d2 by A4,A5,A7,AFF_1:14;
   then A9: LIN c,d1,d2 & LIN b,d1,d2 by A8,AFF_1:def 1;
   then A10: LIN d1,d2,c & LIN d1,d2,b by AFF_1:15;
     LIN d1,d2,c & LIN d1,d2,d1 by A9,AFF_1:15,16;
   then d1,d2 // c,d1 by AFF_1:19;
   then A11: d1,d2 // a,b or c = d1 by A2,AFF_1:14;
     now assume c = d1;
     then c,a // c,b by A4,AFF_1:13;
     then LIN c,a,b by AFF_1:def 1;
    hence contradiction by A1,AFF_1:15; end;
   then d1,d2 // b,a by A11,AFF_1:13;
   then LIN d1,d2,a by A6,A10,AFF_1:18;
  hence contradiction by A1,A6,A10,AFF_1:17;
 end;

definition let AFS; let f;
  attr f is translation means
  :Def11: f is_Dil & (f = id the carrier of AFS or
  (for a holds a<>f.a));
  synonym f is_Tr;
 end;

canceled;

theorem
   id the carrier of AFS is_Tr
  proof id the carrier of AFS is_Dil by Th86;
   hence thesis by Def11;
  end;

theorem Th100: f is_Dil implies
                 (f is_Tr iff (for x,y holds x,f.x // y,f.y))
  proof assume A1: f is_Dil;
    then (f=(id the carrier of AFS) or for x holds f.x<>x) iff
             (for x,y holds x,f.x // y,f.y) by Th93;
   hence thesis by A1,Def11;
  end;

canceled;

theorem Th102:
  f is_Tr & g is_Tr & f.a=g.a & not LIN a,f.a,x implies f.x=g.x
  proof assume that A1: f is_Tr & g is_Tr and A2: f.a=g.a and
  A3: not LIN a,f.a,x;
    A4: f is_Dil & g is_Dil by A1,Def11;
    set b=f.a, y=f.x, z=g.x;
    A5: a,x // b,y & a,b // x,y by A1,A4,Th85,Th100;
      a,x // b,z & a,b // x,z by A1,A2,A4,Th85,Th100;
   hence f.x=g.x by A3,A5,Th97;
  end;

theorem Th103:
 f is_Tr & g is_Tr & f.a=g.a implies f=g
  proof assume that
    A1: f is_Tr and A2: g is_Tr and A3: f.a=g.a;
    A4: f is_Dil by A1,Def11;
    set b=f.a;
    A5: now assume b=a;
          then f=id the carrier of AFS &
                         g=id the carrier of AFS by A1,A2,A3,Def11;
         hence thesis;
        end;
      now assume A6: a<>b;
        for x holds f.x=g.x
        proof let x;
            now assume A7: LIN a,b,x;
              now assume x<>a; consider p such that
              A8: not LIN a,b,p by A6,AFF_1:22;
              A9: f.p=g.p by A1,A2,A3,A8,Th102;
                f<>(id the carrier of AFS) by A6,FUNCT_1:35;
              then A10: f.p<>p & f.x<>x by A1,Def11;
                not LIN p,f.p,x
                proof assume LIN p,f.p,x;
                  then LIN p,f.p,x & LIN p,f.p,f.x & LIN p,f.p,p
                                                  by A4,Th91,AFF_1:16;
                  then A11: LIN x,f.x,p by A10,AFF_1:17;
                  A12: LIN a,b,f.x by A4,A7,Th91;
                    LIN a,b,a by AFF_1:16;
                  then A13: LIN x,f.x,a by A6,A7,A12,AFF_1:17;
                    LIN a,b,b by AFF_1:16;
                  then LIN x,f.x,b by A6,A7,A12,AFF_1:17;
                 hence contradiction by A8,A10,A11,A13,AFF_1:17;
                end;
             hence f.x=g.x by A1,A2,A9,Th102;
            end;
           hence f.x=g.x by A3;
          end;
         hence f.x=g.x by A1,A2,A3,Th102;
        end;
       hence thesis by FUNCT_2:113;
      end;
     hence thesis by A5;
  end;

theorem Th104:
 f is_Tr implies f" is_Tr
  proof assume A1: f is_Tr; then f is_Dil by Def11;
    then A2: f" is_Dil by Th87;
A3:  f=(id the carrier of AFS) implies f"=(id the carrier of AFS) by FUNCT_1:67
;
      now assume A4: for x holds f.x<>x;
      given y such that A5: f".y=y;
        f.y=y by A5,Th4;
     hence contradiction by A4;
    end;
   hence thesis by A1,A2,A3,Def11;
  end;

theorem
   f is_Tr & g is_Tr implies (f*g) is_Tr
  proof assume that A1: f is_Tr and A2: g is_Tr;
    A3: f is_Dil by A1,Def11; g is_Dil by A2,Def11;
    then A4: (f*g) is_Dil by A3,Th88;
      now assume A5: (f*g)<>(id the carrier of AFS);
        for x holds (f*g).x<>x
        proof given x such that
          A6: (f*g).x=x; f.(g.x)=x by A6,FUNCT_2:70;
          then g.x=f".x & f" is_Tr by A1,Th4,Th104;
          then (f*g) = f*f" by A2,Th103;
         hence contradiction by A5,FUNCT_2:88;
        end;
     hence thesis by A4,Def11;
    end;
   hence thesis by A4,Def11;
  end;

definition let AFS; let f;
 attr f is collineation means
     f is_automorphism_of the CONGR of AFS;
  synonym f is_Col;
end;

canceled;

theorem Th107:
 f is_Col iff (for x,y,z,t holds (x,y // z,t iff f.x,f.y // f.z,f.t))
  proof thus f is_Col implies
     (for x,y,z,t holds x,y // z,t iff f.x,f.y // f.z,f.t)
   proof assume A1: f is_automorphism_of the CONGR of AFS;
    let x,y,z,t;
     thus x,y // z,t implies f.x,f.y // f.z,f.t
      proof assume x,y // z,t;
       then [[x,y],[z,t]] in the CONGR of AFS by ANALOAF:def 2;
       then [[f.x,f.y],[f.z,f.t]] in the CONGR of AFS by A1,Def3;
       hence thesis by ANALOAF:def 2; end;
     assume f.x,f.y // f.z,f.t;
      then [[f.x,f.y],[f.z,f.t]] in the CONGR of AFS by ANALOAF:def 2;
      then [[x,y],[z,t]] in the CONGR of AFS by A1,Def3;
     hence thesis by ANALOAF:def 2;
   end;
  assume A2: for x,y,z,t holds (x,y // z,t iff f.x,f.y // f.z,f.t);
   let x,y,z,t; x,y // z,t iff f.x,f.y // f.z,f.t by A2;
    hence thesis by ANALOAF:def 2;
 end;

theorem Th108:
 f is_Col implies (LIN x,y,z iff LIN f.x,f.y,f.z)
 proof assume f is_Col;
  then x,y // x,z iff f.x,f.y // f.x,f.z by Th107;
  hence thesis by AFF_1:def 1;
 end;

theorem
   f is_Col & g is_Col implies f" is_Col & f*g is_Col &
  id the carrier of AFS is_Col
 proof assume f is_automorphism_of the CONGR of AFS &
    g is_automorphism_of the CONGR of AFS;
  hence f" is_automorphism_of the CONGR of AFS &
   f*g is_automorphism_of the CONGR of AFS by Th29,Th30;
  thus id the carrier of AFS is_automorphism_of the CONGR of AFS by Th28;
 end;

reserve A,C,K for Subset of AFS;

theorem
Th110: a in A implies f.a in f.:A
 proof assume A1: a in A;
     dom f = the carrier of AFS by FUNCT_2:67;hence thesis by A1,FUNCT_1:def 12
;
 end;

theorem Th111: x in f.:A iff ex y st y in A & f.y=x
 proof thus x in f.:A implies ex y st y in A & f.y=x
  proof assume x in f.:A; then consider y being set such that
   A1: y in dom f & y in A & x=f.y by FUNCT_1:def 12;
   thus thesis by A1; end;
  given y such that A2: y in A & f.y=x;
    dom f = the carrier of AFS by FUNCT_2:67;
  hence thesis by A2,FUNCT_1:def 12;
 end;

theorem Th112:
 f.:A=f.:C implies A=C proof assume A1: f.:A=f.:C;
  A2: A c= C proof now let a be set; assume A3: a in A;
    then reconsider a'=a as Element of AFS;
    set x=f.a'; x in f.:A by A3,Th110;
    then ex b st b in C & f.b=x by A1,Th111;
    hence a in C by FUNCT_2:85; end; hence thesis by TARSKI:def 3; end;
     C c= A proof now let b be set; assume A4: b in C;
    then reconsider b'=b as Element of AFS;
    set y=f.b'; y in f.:C by A4,Th110;
    then ex a st a in A & f.a=y by A1,Th111;
    hence b in A by FUNCT_2:85; end; hence thesis by TARSKI:def 3; end;
 hence thesis by A2,XBOOLE_0:def 10; end;

theorem Th113:
 f is_Col implies f.:(Line(a,b))=Line(f.a,f.b)
 proof assume A1: f is_Col;
  A2: f.:(Line(a,b)) c= Line(f.a,f.b)
   proof now let x be set; assume A3: x in f.:(Line(a,b));
    then reconsider x'=x as Element of AFS;
   consider y such that
     A4: y in Line(a,b) & f.y=x' by A3,Th111;
       LIN a,b,y by A4,AFF_1:def 2; then LIN f.a,f.b,x' by A1,A4,Th108;
     hence x in Line(f.a,f.b) by AFF_1:def 2; end;
    hence thesis by TARSKI:def 3; end;
     Line(f.a,f.b) c= f.:(Line(a,b))
    proof now let x be set; assume A5: x in Line(f.a,f.b);
    then reconsider x'=x as Element of AFS;
     consider y such that A6: f.y=x' by Th2;
       LIN f.a,f.b,f.y by A5,A6,AFF_1:def 2; then LIN a,b,y by A1,Th108;
     then y in Line(a,b) by AFF_1:def 2;
     hence x in f.:(Line(a,b)) by A6,Th111; end;
    hence thesis by TARSKI:def 3; end;
 hence thesis by A2,XBOOLE_0:def 10; end;

theorem
   f is_Col & K is_line implies f.:K is_line
 proof assume that A1: f is_Col and A2: K is_line;
      consider a,b such that A3: a<>b & K=Line(a,b) by A2,AFF_1:def 3;
      set p=f.a; set q=f.b; A4: f.:K=Line(p,q) by A1,A3,Th113;
        p<>q by A3,FUNCT_2:85; hence thesis by A4,AFF_1:def 3; end;

theorem Th115:
  f is_Col & A // C implies f.:A // f.:C
 proof assume that A1: f is_Col and A2: A // C;
      consider a,b,c,d such that
A3: a<>b & c <>d & a,b // c,d & A=Line(a,b) & C=Line(c,d) by A2,AFF_1:51;
    A4: f.:A=Line(f.a,f.b) & f.:C=Line(f.c,f.d) by A1,A3,Th113;
    A5: f.a<>f.b & f.c <>f.d by A3,FUNCT_2:85;
      f.a,f.b // f.c,f.d by A1,A3,Th107;
 hence thesis by A4,A5,AFF_1:51; end;

reserve AFP for AffinPlane,
        A,C,D,K for Subset of AFP,
        a,b,c,d,p,x,y for Element of AFP,
        f for Permutation of the carrier of AFP;

theorem
   (for A st A is_line holds f.:A is_line) implies f is_Col
 proof assume A1: for A st A is_line holds f.:A is_line;
 A2: a<>b implies f.:(Line(a,b))=Line(f.a,f.b) proof assume A3: a<>b;
  set A=Line(a,b); set x=f.a; set y=f.b;
   A4: x<>y by A3,FUNCT_2:85;
  set K=Line(x,y); set M=f.:A;
   A5: A is_line & K is_line by A4,AFF_1:def 3;
   then A6: M is_line by A1;
     a in A & b in A by AFF_1:26;
   then x in K & y in K & x in M & y in M by Th110,AFF_1:26;
 hence thesis by A4,A5,A6,AFF_1:30; end;
 A7: A // C implies f.:A // f.:C proof assume A8: A // C;
     then A is_line & C is_line by AFF_1:50;
    then A9: f.:A is_line & f.:C is_line by A1;
       A<>C implies thesis proof assume A10: A<>C; assume not f.:A // f.:C;
    then consider x such that
     A11: x in f.:A & x in f.:C by A9,AFF_1:72; consider a such that
     A12: a in A & x=f.a by A11,Th111; consider b such that
     A13: b in C & x=f.b by A11,Th111; a=b by A12,A13,FUNCT_2:85
;hence contradiction by A8,A10,A12,A13,AFF_1:59; end;
 hence thesis by A9,AFF_1:55; end;
 A14: f.:A is_line implies A is_line
  proof assume A15: f.:A is_line; set K=f.:A;
  consider x,y such that A16: x<>y & K=Line(x,y) by A15,AFF_1:def 3;
    A17: x in K & y in K by A16,AFF_1:26;
  then consider a such that A18: a in A & f.a=x by Th111;
  consider b such that A19: b in A & f.b=y by A17,Th111;
  set C=Line(a,b); A20: C is_line by A16,A18,A19,AFF_1:def 3;
    f.:C=K by A2,A16,A18,A19;
  hence thesis by A20,Th112; end;
 A21: f.:A // f.:C implies A // C proof assume A22: f.:A // f.:C;
 set K=f.:A; set M=f.:C;
      K is_line & M is_line by A22,AFF_1:50;
   then A23: A is_line & C is_line by A14;
       now assume A<>C;
      then A24: K<>M by Th112;
    assume not A // C; then consider p such that
      A25: p in A & p in C by A23,AFF_1:72; set x=f.p;
        x in K & x in M by A25,Th110;
      hence contradiction by A22,A24,AFF_1:59; end;
 hence thesis by A23,AFF_1:55; end;
 A26: a,b // c,d implies f.a,f.b // f.c,f.d
  proof assume A27: a,b // c,d;
       now assume A28: a<>b & c <>d; set A=Line(a,b); set C=Line(c,d);
    set K=f.:A; set M=f.:C;
      A29: A // C by A27,A28,AFF_1:51;
         a in A & b in A & c in C & d in C by AFF_1:26;
      then A30: f.a in K & f.b in K & f.c in M & f.d in M by Th110;
        K // M by A7,A29; hence thesis by A30,AFF_1:53; end;
 hence thesis by AFF_1:12; end;
    f.a,f.b // f.c,f.d implies a,b // c,d
  proof assume A31: f.a,f.b // f.c,f.d;
  set x=f.a; set y=f.b; set z=f.c; set t=f.d;
       now assume A32: a<>b & c <>d; set A=Line(a,b); set C=Line(c,d);
    set K=f.:A; set M=f.:C;
      A33: a in A & b in A & c in C & d in C by AFF_1:26;
      A34: x<>y & z<>t by A32,FUNCT_2:85;
        K=Line(x,y) & M=Line(z,t) by A2,A32; then K // M by A31,A34,AFF_1:51;
      then A // C by A21; hence thesis by A33,AFF_1:53; end;
 hence thesis by AFF_1:12; end;
    hence thesis by A26,Th107;
 end;

theorem
  f is_Col & K is_line & (for x st x in K holds f.x=x) &
        not p in K & f.p=p implies f=id the carrier of AFP
 proof assume that A1: f is_Col and A2: K is_line and
        A3: for x st x in K holds f.x=x and
        A4: not p in K & f.p=p;
 A5: for x holds f.x=x proof let x;
       now assume not x in K; consider a,b such that
       A6: a in K & b in K & a<>b by A2,AFF_1:31;
       set A=Line(p,a); set M=Line(p,b);
       A7: A is_line & M is_line by A4,A6,AFF_1:def 3;
       then consider C such that A8: x in C & A // C by AFF_1:63;
       consider D such that A9: x in D & M // D by A7,AFF_1:63;
       A10: C is_line & D is_line & A is_line by A8,A9,AFF_1:50;
       A11: p in A & p in M by AFF_1:26;
       A12: a in A & b in M by AFF_1:26;
       A13: not C // K proof assume C // K;
           then A // K by A8,AFF_1:58;
           hence contradiction by A4,A6,A11,A12,AFF_1:59; end;
       A14: not D // K proof assume D // K;
           then M // K by A9,AFF_1:58;
           hence contradiction by A4,A6,A11,A12,AFF_1:59; end;
       consider c such that
                      A15: c in C & c in K by A2,A10,A13,AFF_1:72;
       consider d such that
                      A16: d in D & d in K by A2,A10,A14,AFF_1:72;
       A17: f.:A=A proof f.:A=Line(f.p,f.a) by A1,Th113;
            hence thesis by A3,A4,A6; end;
       A18: f.:M=M proof f.:M=Line(f.p,f.b) by A1,Th113;
            hence thesis by A3,A4,A6; end;
       A19: f.:C=C proof f.:A // f.:C by A1,A8,Th115;
            then A20: f.:C // C by A8,A17,AFF_1:58;
              f.c = c by A3,A15; then c in f.:C by A15,Th110;
            hence thesis by A15,A20,AFF_1:59; end;
       A21: f.:D=D proof f.:M // f.:D by A1,A9,Th115;
            then A22: f.:D // D by A9,A18,AFF_1:58;
              f.d=d by A3,A16; then d in f.:D by A16,Th110;
            hence thesis by A16,A22,AFF_1:59; end;
         x=f.x proof assume A23: x<>f.x;
              f.x in C & f.x in D by A8,A9,A19,A21,Th110;
            then C=D by A8,A9,A10,A23,AFF_1:30; then A // M by A8,A9,AFF_1:58
; then A=M by A11,AFF_1:59;
            hence contradiction by A2,A4,A6,A10,A11,A12,AFF_1:30; end;
      hence thesis; end;
   hence thesis by A3; end;
    for x holds f.x=(id the carrier of AFP).x proof let x;
         f.x=x by A5;
       hence thesis by FUNCT_1:35; end;
hence thesis by FUNCT_2:113; end;

Back to top