:: Transformations in Affine Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received May 31, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let A be set ;
let f, g be Permutation of A;
:: original:*
redefine funcg * f ->  Permutation of A;
coherence
 g * f is Permutation of A
proofend;
end;

theorem Th1: :: TRANSGEO:1
for A being non empty set
for y being Element of A
for f being Permutation of A ex x being Element of A st f . x = y
proofend;

theorem Th2: :: TRANSGEO:2
for A being non empty set
for x, y being Element of A
for f being Permutation of A holds
( f . x = y iff (f ") . y = x )
proofend;

definition
let A be non empty set ;
let f, g be Permutation of A;
funcf \ g ->  Permutation of A equals :: TRANSGEO:def 1
(g * f) * (g ");
coherence
 (g * f) * (g ") is Permutation of A ;
end;

:: deftheorem  defines \ TRANSGEO:def_1_:_
 for A being non empty set
for f, g being Permutation of A holds f \ g = (g * f) * (g ");

scheme :: TRANSGEO:sch 1
EXPermutation{ F1() ->  non empty set , P1[ set , set ] } :
 ex f being Permutation of F1() st
for x, y being Element of F1() holds
( f . x = y iff P1[x,y] )
provided
A1: for x being Element of F1() ex y being Element of F1() st P1[x,y] and
A2: for y being Element of F1() ex x being Element of F1() st P1[x,y] and
A3: for x, y, x9 being Element of F1() st P1[x,y] & P1[x9,y] holds
x = x9 and
A4: for x, y, y9 being Element of F1() st P1[x,y] & P1[x,y9] holds
y = y9
proofend;

theorem :: TRANSGEO:3
for A being non empty set
for x being Element of A
for f being Permutation of A holds
( f . ((f ") . x) = x & (f ") . (f . x) = x ) by Th2;

theorem :: TRANSGEO:4
for A being non empty set
for f being Permutation of A holds f * (id A) = (id A) * f
proofend;

Lm1:  for A being non empty set
for f, g, h being Permutation of A st f * g = f * h holds
g = h
proofend;

Lm2:  for A being non empty set
for g, f, h being Permutation of A st g * f = h * f holds
g = h
proofend;

theorem :: TRANSGEO:5
for A being non empty set
for g, f, h being Permutation of A st ( g * f = h * f or f * g = f * h ) holds
g = h by Lm1, Lm2;

theorem :: TRANSGEO:6
for A being non empty set
for f, g, h being Permutation of A holds (f * g) \ h = (f \ h) * (g \ h)
proofend;

theorem :: TRANSGEO:7
for A being non empty set
for f, g being Permutation of A holds (f ") \ g = (f \ g) "
proofend;

theorem :: TRANSGEO:8
for A being non empty set
for f, g, h being Permutation of A holds f \ (g * h) = (f \ h) \ g
proofend;

theorem :: TRANSGEO:9
for A being non empty set
for f being Permutation of A holds (id A) \ f = id A
proofend;

theorem :: TRANSGEO:10
for A being non empty set
for f being Permutation of A holds f \ (id A) = f
proofend;

theorem :: TRANSGEO:11
for A being non empty set
for a being Element of A
for f, g being Permutation of A st f . a = a holds
(f \ g) . (g . a) = g . a
proofend;

definition
let A be non empty set ;
let f be Permutation of A;
let R be Relation of [:A,A:];
predf is_FormalIz_of R means :Def2: :: TRANSGEO:def 2
 for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R;
end;

:: deftheorem Def2 defines is_FormalIz_of TRANSGEO:def_2_:_
 for A being non empty set
for f being Permutation of A
for R being Relation of [:A,A:] holds
( f is_FormalIz_of R iff for x, y being Element of A holds [[x,y],[(f . x),(f . y)]] in R );

theorem Th12: :: TRANSGEO:12
for A being non empty set
for R being Relation of [:A,A:] st R is_reflexive_in [:A,A:] holds
id A is_FormalIz_of R
proofend;

theorem Th13: :: TRANSGEO:13
for A being non empty set
for f being Permutation of A
for R being Relation of [:A,A:] st R is_symmetric_in [:A,A:] & f is_FormalIz_of R holds
f " is_FormalIz_of R
proofend;

theorem :: TRANSGEO:14
for A being non empty set
for f, g being Permutation of A
for R being Relation of [:A,A:] st R is_transitive_in [:A,A:] & f is_FormalIz_of R & g is_FormalIz_of R holds
f * g is_FormalIz_of R
proofend;

theorem Th15: :: TRANSGEO:15
for A being non empty set
for f, g being Permutation of A
for R being Relation of [:A,A:] st ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R &amp; [[a,b],[z,t]] in R &amp; a <> b holds
[[x,y],[z,t]] in R ) &amp; ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) &amp; f is_FormalIz_of R &amp; g is_FormalIz_of R holds
f * g is_FormalIz_of R
proofend;

definition
let A be non empty set ;
let f be Permutation of A;
let R be Relation of [:A,A:];
predf is_automorphism_of R means :Def3: :: TRANSGEO:def 3
 for x, y, z, t being Element of A holds
( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R );
end;

:: deftheorem Def3 defines is_automorphism_of TRANSGEO:def_3_:_
 for A being non empty set
for f being Permutation of A
for R being Relation of [:A,A:] holds
( f is_automorphism_of R iff for x, y, z, t being Element of A holds
( [[x,y],[z,t]] in R iff [[(f . x),(f . y)],[(f . z),(f . t)]] in R ) );

theorem Th16: :: TRANSGEO:16
for A being non empty set
for R being Relation of [:A,A:] holds id A is_automorphism_of R
proofend;

theorem Th17: :: TRANSGEO:17
for A being non empty set
for f being Permutation of A
for R being Relation of [:A,A:] st f is_automorphism_of R holds
f " is_automorphism_of R
proofend;

theorem Th18: :: TRANSGEO:18
for A being non empty set
for f, g being Permutation of A
for R being Relation of [:A,A:] st f is_automorphism_of R &amp; g is_automorphism_of R holds
g * f is_automorphism_of R
proofend;

theorem :: TRANSGEO:19
for A being non empty set
for f being Permutation of A
for R being Relation of [:A,A:] st R is_symmetric_in [:A,A:] &amp; R is_transitive_in [:A,A:] &amp; f is_FormalIz_of R holds
f is_automorphism_of R
proofend;

theorem :: TRANSGEO:20
for A being non empty set
for f being Permutation of A
for R being Relation of [:A,A:] st ( for a, b, x, y, z, t being Element of A st [[x,y],[a,b]] in R &amp; [[a,b],[z,t]] in R &amp; a <> b holds
[[x,y],[z,t]] in R ) &amp; ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) &amp; R is_symmetric_in [:A,A:] &amp; f is_FormalIz_of R holds
f is_automorphism_of R
proofend;

theorem :: TRANSGEO:21
for A being non empty set
for f, g being Permutation of A
for R being Relation of [:A,A:] st f is_FormalIz_of R &amp; g is_automorphism_of R holds
f \ g is_FormalIz_of R
proofend;

definition
let AS be non empty AffinStruct ;
let f be Permutation of the carrier of AS;
predf is_DIL_of AS means :Def4: :: TRANSGEO:def 4
f is_FormalIz_of the CONGR of AS;
end;

:: deftheorem Def4 defines is_DIL_of TRANSGEO:def_4_:_
 for AS being non empty AffinStruct
for f being Permutation of the carrier of AS holds
( f is_DIL_of AS iff f is_FormalIz_of the CONGR of AS );

theorem Th22: :: TRANSGEO:22
for AS being non empty AffinStruct
for f being Permutation of the carrier of AS holds
( f is_DIL_of AS iff for a, b being Element of AS holds a,b // f . a,f . b )
proofend;

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

:: deftheorem Def5 defines CongrSpace-like TRANSGEO:def_5_:_
 for IT being non empty AffinStruct holds
( IT is CongrSpace-like iff ( ( for x, y, z, t, a, b being Element of IT st x,y // a,b &amp; a,b // z,t &amp; a <> b holds
x,y // z,t ) &amp; ( for x, y, z being Element of IT holds x,x // y,z ) &amp; ( for x, y, z, t being Element of IT st x,y // z,t holds
z,t // x,y ) &amp; ( for x, y being Element of IT holds x,y // x,y ) ) );

registration
cluster non empty strict CongrSpace-like for AffinStruct ;
existence
 ex b1 being non empty AffinStruct st
( b1 is strict &amp; b1 is CongrSpace-like )
proofend;
end;

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

Lm3:  for CS being CongrSpace holds the CONGR of CS is_reflexive_in [: the carrier of CS, the carrier of CS:]
proofend;

Lm4:  for CS being CongrSpace holds the CONGR of CS is_symmetric_in [: the carrier of CS, the carrier of CS:]
proofend;

theorem Th23: :: TRANSGEO:23
for CS being CongrSpace holds id the carrier of CS is_DIL_of CS
proofend;

theorem Th24: :: TRANSGEO:24
for CS being CongrSpace
for f being Permutation of the carrier of CS st f is_DIL_of CS holds
f " is_DIL_of CS
proofend;

theorem Th25: :: TRANSGEO:25
for CS being CongrSpace
for f, g being Permutation of the carrier of CS st f is_DIL_of CS &amp; g is_DIL_of CS holds
f * g is_DIL_of CS
proofend;

theorem Th26: :: TRANSGEO:26
for OAS being OAffinSpace holds OAS is CongrSpace-like
proofend;

definition
let OAS be OAffinSpace;
let f be Permutation of the carrier of OAS;
attrf is positive_dilatation  means :Def6: :: TRANSGEO:def 6
f is_DIL_of OAS;
end;

:: deftheorem Def6 defines positive_dilatation TRANSGEO:def_6_:_
 for OAS being OAffinSpace
for f being Permutation of the carrier of OAS holds
( f is positive_dilatation iff f is_DIL_of OAS );

theorem Th27: :: TRANSGEO:27
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS holds
( f is positive_dilatation iff for a, b being Element of OAS holds a,b // f . a,f . b )
proofend;

definition
let OAS be OAffinSpace;
let f be Permutation of the carrier of OAS;
attrf is negative_dilatation  means :Def7: :: TRANSGEO:def 7
 for a, b being Element of OAS holds a,b // f . b,f . a;
end;

:: deftheorem Def7 defines negative_dilatation TRANSGEO:def_7_:_
 for OAS being OAffinSpace
for f being Permutation of the carrier of OAS holds
( f is negative_dilatation iff for a, b being Element of OAS holds a,b // f . b,f . a );

theorem Th28: :: TRANSGEO:28
for OAS being OAffinSpace holds id the carrier of OAS is positive_dilatation
proofend;

theorem :: TRANSGEO:29
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is positive_dilatation holds
f " is positive_dilatation
proofend;

theorem :: TRANSGEO:30
for OAS being OAffinSpace
for f, g being Permutation of the carrier of OAS st f is positive_dilatation &amp; g is positive_dilatation holds
f * g is positive_dilatation
proofend;

theorem :: TRANSGEO:31
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS holds
( not f is negative_dilatation or not f is positive_dilatation )
proofend;

theorem :: TRANSGEO:32
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is negative_dilatation holds
f " is negative_dilatation
proofend;

theorem :: TRANSGEO:33
for OAS being OAffinSpace
for f, g being Permutation of the carrier of OAS st f is positive_dilatation &amp; g is negative_dilatation holds
( f * g is negative_dilatation &amp; g * f is negative_dilatation )
proofend;

definition
let OAS be OAffinSpace;
let f be Permutation of the carrier of OAS;
attrf is dilatation  means :Def8: :: TRANSGEO:def 8
f is_FormalIz_of lambda the CONGR of OAS;
end;

:: deftheorem Def8 defines dilatation TRANSGEO:def_8_:_
 for OAS being OAffinSpace
for f being Permutation of the carrier of OAS holds
( f is dilatation iff f is_FormalIz_of lambda the CONGR of OAS );

theorem Th34: :: TRANSGEO:34
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS holds
( f is dilatation iff for a, b being Element of OAS holds a,b '||' f . a,f . b )
proofend;

theorem :: TRANSGEO:35
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st ( f is positive_dilatation or f is negative_dilatation ) holds
f is dilatation
proofend;

theorem :: TRANSGEO:36
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is dilatation holds
ex f9 being Permutation of the carrier of (Lambda OAS) st
( f = f9 &amp; f9 is_DIL_of Lambda OAS )
proofend;

theorem :: TRANSGEO:37
for OAS being OAffinSpace
for f being Permutation of the carrier of (Lambda OAS) st f is_DIL_of Lambda OAS holds
ex f9 being Permutation of the carrier of OAS st
( f = f9 &amp; f9 is dilatation )
proofend;

theorem :: TRANSGEO:38
for OAS being OAffinSpace holds id the carrier of OAS is dilatation
proofend;

theorem Th39: :: TRANSGEO:39
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is dilatation holds
f " is dilatation
proofend;

theorem Th40: :: TRANSGEO:40
for OAS being OAffinSpace
for f, g being Permutation of the carrier of OAS st f is dilatation &amp; g is dilatation holds
f * g is dilatation
proofend;

theorem Th41: :: TRANSGEO:41
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is dilatation holds
for a, b, c, d being Element of OAS holds
( a,b '||' c,d iff f . a,f . b '||' f . c,f . d )
proofend;

theorem Th42: :: TRANSGEO:42
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is dilatation holds
for a, b, c being Element of OAS holds
( LIN a,b,c iff LIN f . a,f . b,f . c )
proofend;

theorem Th43: :: TRANSGEO:43
for OAS being OAffinSpace
for x, y being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation &amp; LIN x,f . x,y holds
LIN x,f . x,f . y
proofend;

theorem Th44: :: TRANSGEO:44
for OAS being OAffinSpace
for a, b, c, d being Element of OAS holds
( not a,b '||' c,d or a,c '||' b,d or ex x being Element of OAS st
( LIN a,c,x &amp; LIN b,d,x ) )
proofend;

theorem Th45: :: TRANSGEO:45
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is dilatation holds
( ( f = id the carrier of OAS or for x being Element of OAS holds f . x <> x ) iff for x, y being Element of OAS holds x,f . x '||' y,f . y )
proofend;

theorem Th46: :: TRANSGEO:46
for OAS being OAffinSpace
for a, b, x being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation &amp; f . a = a &amp; f . b = b &amp; not LIN a,b,x holds
f . x = x
proofend;

theorem Th47: :: TRANSGEO:47
for OAS being OAffinSpace
for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation &amp; f . a = a &amp; f . b = b &amp; a <> b holds
f = id the carrier of OAS
proofend;

theorem :: TRANSGEO:48
for OAS being OAffinSpace
for a, b being Element of OAS
for f, g being Permutation of the carrier of OAS st f is dilatation &amp; g is dilatation &amp; f . a = g . a &amp; f . b = g . b &amp; not a = b holds
f = g
proofend;

definition
let OAS be OAffinSpace;
let f be Permutation of the carrier of OAS;
attrf is translation  means :Def9: :: TRANSGEO:def 9
( f is dilatation &amp; ( f = id the carrier of OAS or for a being Element of OAS holds a <> f . a ) );
end;

:: deftheorem Def9 defines translation TRANSGEO:def_9_:_
 for OAS being OAffinSpace
for f being Permutation of the carrier of OAS holds
( f is translation iff ( f is dilatation &amp; ( f = id the carrier of OAS or for a being Element of OAS holds a <> f . a ) ) );

theorem Th49: :: TRANSGEO:49
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is dilatation holds
( f is translation iff for x, y being Element of OAS holds x,f . x '||' y,f . y )
proofend;

theorem Th50: :: TRANSGEO:50
for OAS being OAffinSpace
for a, x being Element of OAS
for f, g being Permutation of the carrier of OAS st f is translation &amp; g is translation &amp; f . a = g . a &amp; not LIN a,f . a,x holds
f . x = g . x
proofend;

theorem Th51: :: TRANSGEO:51
for OAS being OAffinSpace
for a being Element of OAS
for f, g being Permutation of the carrier of OAS st f is translation &amp; g is translation &amp; f . a = g . a holds
f = g
proofend;

theorem Th52: :: TRANSGEO:52
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is translation holds
f " is translation
proofend;

theorem :: TRANSGEO:53
for OAS being OAffinSpace
for f, g being Permutation of the carrier of OAS st f is translation &amp; g is translation holds
f * g is translation
proofend;

Lm5:  for OAS being OAffinSpace
for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is translation &amp; not LIN a,f . a,b holds
( a,b // f . a,f . b &amp; a,f . a // b,f . b )
proofend;

Lm6:  for OAS being OAffinSpace
for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is translation &amp; a <> f . a &amp; LIN a,f . a,b holds
a,f . a // b,f . b
proofend;

Lm7:  for OAS being OAffinSpace
for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is translation &amp; Mid a,f . a,b &amp; a <> f . a holds
a,b // f . a,f . b
proofend;

Lm8:  for OAS being OAffinSpace
for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is translation &amp; a <> f . a &amp; b <> f . a &amp; Mid a,b,f . a holds
a,b // f . a,f . b
proofend;

Lm9:  for OAS being OAffinSpace
for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is translation &amp; a <> f . a &amp; LIN a,f . a,b holds
a,b // f . a,f . b
proofend;

theorem Th54: :: TRANSGEO:54
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is translation holds
f is positive_dilatation
proofend;

theorem Th55: :: TRANSGEO:55
for OAS being OAffinSpace
for p, q, x being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation &amp; f . p = p &amp; Mid q,p,f . q &amp; not LIN p,q,x holds
Mid x,p,f . x
proofend;

theorem Th56: :: TRANSGEO:56
for OAS being OAffinSpace
for p, q, x being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation &amp; f . p = p &amp; Mid q,p,f . q &amp; q <> p holds
Mid x,p,f . x
proofend;

theorem Th57: :: TRANSGEO:57
for OAS being OAffinSpace
for p, q, x, y being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation &amp; f . p = p &amp; q <> p &amp; Mid q,p,f . q &amp; not LIN p,x,y holds
x,y // f . y,f . x
proofend;

theorem Th58: :: TRANSGEO:58
for OAS being OAffinSpace
for p, q, x, y being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation &amp; f . p = p &amp; q <> p &amp; Mid q,p,f . q &amp; LIN p,x,y holds
x,y // f . y,f . x
proofend;

theorem Th59: :: TRANSGEO:59
for OAS being OAffinSpace
for p, q being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation &amp; f . p = p &amp; q <> p &amp; Mid q,p,f . q holds
f is negative_dilatation
proofend;

theorem Th60: :: TRANSGEO:60
for OAS being OAffinSpace
for p being Element of OAS
for f being Permutation of the carrier of OAS st f is dilatation &amp; f . p = p &amp; ( for x being Element of OAS holds p,x // p,f . x ) holds
for y, z being Element of OAS holds y,z // f . y,f . z
proofend;

theorem :: TRANSGEO:61
for OAS being OAffinSpace
for f being Permutation of the carrier of OAS holds
( not f is dilatation or f is positive_dilatation or f is negative_dilatation )
proofend;

theorem Th62: :: TRANSGEO:62
for AFS being AffinSpace holds AFS is CongrSpace-like
proofend;

theorem :: TRANSGEO:63
for OAS being OAffinSpace holds Lambda OAS is CongrSpace
proofend;

definition
let AFS be AffinSpace;
let f be Permutation of the carrier of AFS;
attrf is dilatation  means :Def10: :: TRANSGEO:def 10
f is_DIL_of AFS;
end;

:: deftheorem Def10 defines dilatation TRANSGEO:def_10_:_
 for AFS being AffinSpace
for f being Permutation of the carrier of AFS holds
( f is dilatation iff f is_DIL_of AFS );

theorem Th64: :: TRANSGEO:64
for AFS being AffinSpace
for f being Permutation of the carrier of AFS holds
( f is dilatation iff for a, b being Element of AFS holds a,b // f . a,f . b )
proofend;

theorem Th65: :: TRANSGEO:65
for AFS being AffinSpace holds id the carrier of AFS is dilatation
proofend;

theorem Th66: :: TRANSGEO:66
for AFS being AffinSpace
for f being Permutation of the carrier of AFS st f is dilatation holds
f " is dilatation
proofend;

theorem Th67: :: TRANSGEO:67
for AFS being AffinSpace
for f, g being Permutation of the carrier of AFS st f is dilatation &amp; g is dilatation holds
f * g is dilatation
proofend;

theorem Th68: :: TRANSGEO:68
for AFS being AffinSpace
for f being Permutation of the carrier of AFS st f is dilatation holds
for a, b, c, d being Element of AFS holds
( a,b // c,d iff f . a,f . b // f . c,f . d )
proofend;

theorem :: TRANSGEO:69
for AFS being AffinSpace
for f being Permutation of the carrier of AFS st f is dilatation holds
for a, b, c being Element of AFS holds
( LIN a,b,c iff LIN f . a,f . b,f . c )
proofend;

theorem Th70: :: TRANSGEO:70
for AFS being AffinSpace
for x, y being Element of AFS
for f being Permutation of the carrier of AFS st f is dilatation &amp; LIN x,f . x,y holds
LIN x,f . x,f . y
proofend;

theorem Th71: :: TRANSGEO:71
for AFS being AffinSpace
for a, b, c, d being Element of AFS holds
( not a,b // c,d or a,c // b,d or ex x being Element of AFS st
( LIN a,c,x &amp; LIN b,d,x ) )
proofend;

theorem Th72: :: TRANSGEO:72
for AFS being AffinSpace
for f being Permutation of the carrier of AFS st f is dilatation holds
( ( f = id the carrier of AFS or for x being Element of AFS holds f . x <> x ) iff for x, y being Element of AFS holds x,f . x // y,f . y )
proofend;

theorem Th73: :: TRANSGEO:73
for AFS being AffinSpace
for a, b, x being Element of AFS
for f being Permutation of the carrier of AFS st f is dilatation &amp; f . a = a &amp; f . b = b &amp; not LIN a,b,x holds
f . x = x
proofend;

theorem Th74: :: TRANSGEO:74
for AFS being AffinSpace
for a, b being Element of AFS
for f being Permutation of the carrier of AFS st f is dilatation &amp; f . a = a &amp; f . b = b &amp; a <> b holds
f = id the carrier of AFS
proofend;

theorem :: TRANSGEO:75
for AFS being AffinSpace
for a, b being Element of AFS
for f, g being Permutation of the carrier of AFS st f is dilatation &amp; g is dilatation &amp; f . a = g . a &amp; f . b = g . b &amp; not a = b holds
f = g
proofend;

theorem Th76: :: TRANSGEO:76
for AFS being AffinSpace
for a, b, c, d1, d2 being Element of AFS st not LIN a,b,c &amp; a,b // c,d1 &amp; a,b // c,d2 &amp; a,c // b,d1 &amp; a,c // b,d2 holds
d1 = d2
proofend;

definition
let AFS be AffinSpace;
let f be Permutation of the carrier of AFS;
attrf is translation  means :Def11: :: TRANSGEO:def 11
( f is dilatation &amp; ( f = id the carrier of AFS or for a being Element of AFS holds a <> f . a ) );
end;

:: deftheorem Def11 defines translation TRANSGEO:def_11_:_
 for AFS being AffinSpace
for f being Permutation of the carrier of AFS holds
( f is translation iff ( f is dilatation &amp; ( f = id the carrier of AFS or for a being Element of AFS holds a <> f . a ) ) );

theorem :: TRANSGEO:77
for AFS being AffinSpace holds id the carrier of AFS is translation
proofend;

theorem Th78: :: TRANSGEO:78
for AFS being AffinSpace
for f being Permutation of the carrier of AFS st f is dilatation holds
( f is translation iff for x, y being Element of AFS holds x,f . x // y,f . y )
proofend;

theorem Th79: :: TRANSGEO:79
for AFS being AffinSpace
for a, x being Element of AFS
for f, g being Permutation of the carrier of AFS st f is translation &amp; g is translation &amp; f . a = g . a &amp; not LIN a,f . a,x holds
f . x = g . x
proofend;

theorem Th80: :: TRANSGEO:80
for AFS being AffinSpace
for a being Element of AFS
for f, g being Permutation of the carrier of AFS st f is translation &amp; g is translation &amp; f . a = g . a holds
f = g
proofend;

theorem Th81: :: TRANSGEO:81
for AFS being AffinSpace
for f being Permutation of the carrier of AFS st f is translation holds
f " is translation
proofend;

theorem :: TRANSGEO:82
for AFS being AffinSpace
for f, g being Permutation of the carrier of AFS st f is translation &amp; g is translation holds
f * g is translation
proofend;

definition
let AFS be AffinSpace;
let f be Permutation of the carrier of AFS;
attrf is collineation  means :: TRANSGEO:def 12
f is_automorphism_of the CONGR of AFS;
end;

:: deftheorem  defines collineation TRANSGEO:def_12_:_
 for AFS being AffinSpace
for f being Permutation of the carrier of AFS holds
( f is collineation iff f is_automorphism_of the CONGR of AFS );

theorem Th83: :: TRANSGEO:83
for AFS being AffinSpace
for f being Permutation of the carrier of AFS holds
( f is collineation iff for x, y, z, t being Element of AFS holds
( x,y // z,t iff f . x,f . y // f . z,f . t ) )
proofend;

theorem Th84: :: TRANSGEO:84
for AFS being AffinSpace
for x, y, z being Element of AFS
for f being Permutation of the carrier of AFS st f is collineation holds
( LIN x,y,z iff LIN f . x,f . y,f . z )
proofend;

theorem :: TRANSGEO:85
for AFS being AffinSpace
for f, g being Permutation of the carrier of AFS st f is collineation &amp; g is collineation holds
( f " is collineation &amp; f * g is collineation &amp; id the carrier of AFS is collineation )
proofend;

theorem Th86: :: TRANSGEO:86
for AFS being AffinSpace
for a being Element of AFS
for f being Permutation of the carrier of AFS
for A being Subset of AFS st a in A holds
f . a in f .: A
proofend;

theorem Th87: :: TRANSGEO:87
for AFS being AffinSpace
for x being Element of AFS
for f being Permutation of the carrier of AFS
for A being Subset of AFS holds
( x in f .: A iff ex y being Element of AFS st
( y in A &amp; f . y = x ) )
proofend;

theorem Th88: :: TRANSGEO:88
for AFS being AffinSpace
for f being Permutation of the carrier of AFS
for A, C being Subset of AFS st f .: A = f .: C holds
A = C
proofend;

theorem Th89: :: TRANSGEO:89
for AFS being AffinSpace
for a, b being Element of AFS
for f being Permutation of the carrier of AFS st f is collineation holds
f .: (Line (a,b)) = Line ((f . a),(f . b))
proofend;

theorem :: TRANSGEO:90
for AFS being AffinSpace
for f being Permutation of the carrier of AFS
for K being Subset of AFS st f is collineation &amp; K is being_line holds
f .: K is being_line
proofend;

theorem Th91: :: TRANSGEO:91
for AFS being AffinSpace
for f being Permutation of the carrier of AFS
for A, C being Subset of AFS st f is collineation &amp; A // C holds
f .: A // f .: C
proofend;

theorem :: TRANSGEO:92
for AFP being AffinPlane
for f being Permutation of the carrier of AFP st ( for A being Subset of AFP st A is being_line holds
f .: A is being_line ) holds
f is collineation
proofend;

theorem :: TRANSGEO:93
for AFP being AffinPlane
for K being Subset of AFP
for p being Element of AFP
for f being Permutation of the carrier of AFP st f is collineation &amp; K is being_line &amp; ( for x being Element of AFP st x in K holds
f . x = x ) &amp; not p in K &amp; f . p = p holds
f = id the carrier of AFP
proofend;