Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Transformations in Affine Spaces

by
Henryk Oryszczyszyn, and
Krzysztof Prazmowski

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