The Mizar abstract of TRANSGEO

Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users
The abstract of the Mizar article:: Transformations in Affine Spaces
by
Henryk Oryszczyszyn, and
Krzysztof Prazmowski
Received May 31, 1990
MML identifier: TRANSGEO
[ Mizar article, 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;


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;
end;

canceled;

theorem :: TRANSGEO:2
   ex x st f.x=y;

canceled;

theorem :: TRANSGEO:4
   f.x=y iff (f").y=x;

definition let A,f,g;
 func f\g -> Permutation of A equals
:: TRANSGEO:def 1
   (g*f)*g";
 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
  for x being Element of A()
      ex y being Element of A() st P[x,y] and
  for y being Element of A()
      ex x being Element of A() st P[x,y] and
  for x,y,x' being Element of A()
       st P[x,y] & P[x',y] holds x=x' and
  for x,y,y' being Element of A()
       st P[x,y] & P[x,y'] holds y=y';

canceled 4;

theorem :: TRANSGEO:9
   f.(f".x) = x & f".(f.x) = x;

canceled;

theorem :: TRANSGEO:11
   f*(id A) = (id A)*f;

canceled;

theorem :: TRANSGEO:13
   g*f=h*f or f*g=f*h implies g=h;

canceled 2;

theorem :: TRANSGEO:16
   (f*g)\h = (f\h)*(g\h);

theorem :: TRANSGEO:17
   (f")\g = (f\g)";

theorem :: TRANSGEO:18
   f\(g*h) = (f\h)\g;

theorem :: TRANSGEO:19
   (id A)\f = id A;

theorem :: TRANSGEO:20
   f\(id A) = f;

theorem :: TRANSGEO:21
   f.a=a implies (f\g).(g.a)=g.a;

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

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

canceled;

theorem :: TRANSGEO:23
  R is_reflexive_in [:A,A:] implies id A is_FormalIz_of R;

theorem :: TRANSGEO:24
  R is_symmetric_in [:A,A:] & f is_FormalIz_of R
                                       implies f" is_FormalIz_of R;

theorem :: TRANSGEO:25
    R is_transitive_in [:A,A:] & f is_FormalIz_of R
                 & g is_FormalIz_of R implies (f*g) is_FormalIz_of R;

theorem :: TRANSGEO:26
   (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;

definition
 let A; let f; let R;
 pred f is_automorphism_of R means
:: TRANSGEO:def 3
  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 :: TRANSGEO:28
 id A is_automorphism_of R;

theorem :: TRANSGEO:29
 f is_automorphism_of R implies f" is_automorphism_of R;

theorem :: TRANSGEO:30
 f is_automorphism_of R & g is_automorphism_of R implies
                                    g*f is_automorphism_of R;

theorem :: TRANSGEO:31
   R is_symmetric_in [:A,A:] & R is_transitive_in [:A,A:] &
            f is_FormalIz_of R implies f is_automorphism_of R;

theorem :: TRANSGEO:32
   (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;

theorem :: TRANSGEO:33
     f is_FormalIz_of R & g is_automorphism_of R
          implies f\g is_FormalIz_of R;

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
:: TRANSGEO:def 4
   f is_FormalIz_of the CONGR of AS;
end;

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

canceled;

theorem :: TRANSGEO:35
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));

definition let IT be non empty AffinStruct;
 attr IT is CongrSpace-like means
:: TRANSGEO:def 5
   (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);
end;

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

reserve CS for CongrSpace;

canceled;

theorem :: TRANSGEO:37
id the carrier of CS is_DIL_of CS;

theorem :: TRANSGEO:38
for f being Permutation of the carrier of CS st
           f is_DIL_of CS holds f" is_DIL_of CS;

theorem :: TRANSGEO:39
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;

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

theorem :: TRANSGEO:40
OAS is CongrSpace-like;

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
:: TRANSGEO:def 6
   f is_DIL_of OAS;
  synonym f is_CDil;
end;

canceled;

theorem :: TRANSGEO:42
for f being Permutation of the carrier of OAS holds
  (f is_CDil iff (for a,b holds a,b // f.a,f.b));

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

canceled;

theorem :: TRANSGEO:44
id the carrier of OAS is_CDil;

theorem :: TRANSGEO:45
for f being Permutation of the carrier of OAS st
       f is_CDil holds f" is_CDil;

theorem :: TRANSGEO:46
for f,g being Permutation of the carrier of OAS st
      f is_CDil & g is_CDil holds f*g is_CDil;

theorem :: TRANSGEO:47
   not ex f st f is_SDil & f is_CDil;

theorem :: TRANSGEO:48
   f is_SDil implies f" is_SDil;

theorem :: TRANSGEO:49
f is_CDil & g is_SDil
                    implies f*g is_SDil & g*f is_SDil;

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

canceled;

theorem :: TRANSGEO:51
 for f being Permutation of the carrier of OAS holds
       (f is_Dil iff (for a,b holds a,b '||' f.a,f.b));

theorem :: TRANSGEO:52
   f is_CDil or f is_SDil implies f is_Dil;

theorem :: TRANSGEO:53
   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);

 theorem :: TRANSGEO:54
    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;

theorem :: TRANSGEO:55
   id the carrier of OAS is_Dil;

theorem :: TRANSGEO:56
 f is_Dil implies f" is_Dil;

theorem :: TRANSGEO:57
 f is_Dil & g is_Dil implies f*g is_Dil;

theorem :: TRANSGEO:58
f is_Dil implies (for a,b,c,d holds a,b '||' c,d iff f.a,f.b '||' f.c,f.d);

theorem :: TRANSGEO:59
 f is_Dil implies (for a,b,c holds LIN a,b,c iff LIN f.a,f.b,f.c);

theorem :: TRANSGEO:60
 f is_Dil & LIN x,f.x,y implies LIN x,f.x,f.y;

theorem :: TRANSGEO:61
 a,b '||' c,d implies (a,c '||' b,d or (ex x st LIN a,c,x & LIN b,d,x));

theorem :: TRANSGEO:62
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));

theorem :: TRANSGEO:63
  f is_Dil & f.a=a & f.b=b & not LIN a,b,x implies f.x=x;

theorem :: TRANSGEO:64
f is_Dil & f.a=a & f.b=b & a<>b implies f=(id the carrier of OAS);

theorem :: TRANSGEO:65
    f is_Dil & g is_Dil & f.a=g.a & f.b=g.b implies a=b or f=g;

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

canceled;

theorem :: TRANSGEO:67
 f is_Dil implies (f is_Tr iff (for x,y holds x,f.x '||' y,f.y));

canceled;

theorem :: TRANSGEO:69
  f is_Tr & g is_Tr & f.a=g.a & not LIN a,f.a,x implies f.x=g.x;

theorem :: TRANSGEO:70
f is_Tr & g is_Tr & f.a=g.a implies f=g;

theorem :: TRANSGEO:71
 f is_Tr implies f" is_Tr;

theorem :: TRANSGEO:72
   f is_Tr & g is_Tr implies (f*g) is_Tr;

theorem :: TRANSGEO:73
 f is_Tr implies f is_CDil;

theorem :: TRANSGEO:74
 f is_Dil & f.p=p & Mid q,p,f.q & not LIN p,q,x
                                         implies Mid x,p,f.x;

theorem :: TRANSGEO:75
 f is_Dil & f.p=p & Mid q,p,f.q & q<>p implies Mid x,p,f.x;

theorem :: TRANSGEO:76
 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;

theorem :: TRANSGEO:77
 f is_Dil & f.p=p & q<>p & Mid q,p,f.q & LIN p,x,y
                                    implies x,y // f.y,f.x;

theorem :: TRANSGEO:78
 f is_Dil & f.p=p & q<>p & Mid q,p,f.q implies f is_SDil;

theorem :: TRANSGEO:79
 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);

theorem :: TRANSGEO:80
   f is_Dil implies f is_CDil or f is_SDil;

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

canceled;

theorem :: TRANSGEO:82
AFS is CongrSpace-like;

theorem :: TRANSGEO:83
Lambda(OAS) is CongrSpace;

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

definition let AFS; let f;
  attr f is dilatation means
:: TRANSGEO:def 10
   f is_DIL_of AFS;
  synonym f is_Dil;
end;

canceled;

theorem :: TRANSGEO:85
  f is_Dil iff (for a,b holds a,b // f.a,f.b);

theorem :: TRANSGEO:86
 id the carrier of AFS is_Dil;

theorem :: TRANSGEO:87
 f is_Dil implies f" is_Dil;

theorem :: TRANSGEO:88
 f is_Dil & g is_Dil implies (f*g) is_Dil;

theorem :: TRANSGEO:89
f is_Dil implies (for a,b,c,d holds a,b // c,d iff f.a,f.b // f.c,f.d);

theorem :: TRANSGEO:90
   f is_Dil implies (for a,b,c holds LIN a,b,c iff LIN f.a,f.b,f.c);

theorem :: TRANSGEO:91
 f is_Dil & LIN x,f.x,y implies LIN x,f.x,f.y;

theorem :: TRANSGEO:92
 a,b // c,d implies (a,c // b,d or (ex x st LIN a,c,x & LIN b,d,x));

theorem :: TRANSGEO:93
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));

theorem :: TRANSGEO:94
  f is_Dil & f.a=a & f.b=b & not LIN a,b,x implies f.x=x;

theorem :: TRANSGEO:95
  f is_Dil & f.a=a & f.b=b & a<>b implies f=id the carrier of AFS;

theorem :: TRANSGEO:96
  f is_Dil & g is_Dil & f.a=g.a & f.b=g.b implies a=b or f=g;

theorem :: TRANSGEO:97
 not LIN a,b,c & a,b // c,d1 & a,b // c,d2 & a,c // b,d1 &
       a,c // b,d2 implies d1=d2;

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

canceled;

theorem :: TRANSGEO:99
   id the carrier of AFS is_Tr;

theorem :: TRANSGEO:100
f is_Dil implies
                 (f is_Tr iff (for x,y holds x,f.x // y,f.y));

canceled;

theorem :: TRANSGEO:102
  f is_Tr & g is_Tr & f.a=g.a & not LIN a,f.a,x implies f.x=g.x;

theorem :: TRANSGEO:103
 f is_Tr & g is_Tr & f.a=g.a implies f=g;

theorem :: TRANSGEO:104
 f is_Tr implies f" is_Tr;

theorem :: TRANSGEO:105
   f is_Tr & g is_Tr implies (f*g) is_Tr;

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

canceled;

theorem :: TRANSGEO:107
 f is_Col iff (for x,y,z,t holds (x,y // z,t iff f.x,f.y // f.z,f.t));

theorem :: TRANSGEO:108
 f is_Col implies (LIN x,y,z iff LIN f.x,f.y,f.z);

theorem :: TRANSGEO:109
   f is_Col & g is_Col implies f" is_Col & f*g is_Col &
  id the carrier of AFS is_Col;

reserve A,C,K for Subset of AFS;

theorem :: TRANSGEO:110
 a in A implies f.a in f.:A;

theorem :: TRANSGEO:111
x in f.:A iff ex y st y in A & f.y=x;

theorem :: TRANSGEO:112
 f.:A=f.:C implies A=C;

theorem :: TRANSGEO:113
 f is_Col implies f.:(Line(a,b))=Line(f.a,f.b);

theorem :: TRANSGEO:114
   f is_Col & K is_line implies f.:K is_line;

theorem :: TRANSGEO:115
  f is_Col & A // C implies f.:A // f.:C;

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 :: TRANSGEO:116
   (for A st A is_line holds f.:A is_line) implies f is_Col;

theorem :: TRANSGEO:117
  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;
The abstract of the Mizar article:

Transformations in Affine Spaces
