:: TRANSGEO semantic presentation

definition

let A be set ;
let f, g be Permutation of A;
:: original: *
redefine func g * f -> Permutation of A;
coherence

proof end;

end;

theorem :: TRANSGEO:1

canceled;

theorem Th2: :: TRANSGEO:2

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

proof end;

theorem :: TRANSGEO:3

canceled;

theorem Th4: :: TRANSGEO:4

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 )

proof end;

definition

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

end;

:: deftheorem defines \ TRANSGEO:def 1 :

scheme :: TRANSGEO:sch 1
EXPermutation{ F₁() -> non empty set , P₁[ set , set ] } :

ex f being Permutation of F₁() st
for x, y being Element of F₁() holds
( f . x = y iff P₁[x,y] )

provided

A1: for x being Element of F₁() ex y being Element of F₁() st P₁[x,y] and
A2: for y being Element of F₁() ex x being Element of F₁() st P₁[x,y] and
A3: for x, y, x' being Element of F₁() st P₁[x,y] & P₁[x',y] holds
x = x' and
A4: for x, y, y' being Element of F₁() st P₁[x,y] & P₁[x,y'] holds
y = y'

proof end;

theorem :: TRANSGEO:5

canceled;

theorem :: TRANSGEO:6

canceled;

theorem :: TRANSGEO:7

canceled;

theorem :: TRANSGEO:8

canceled;

theorem :: TRANSGEO:9

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

theorem :: TRANSGEO:10

canceled;

theorem :: TRANSGEO:11

for A being non empty set
for f being Permutation of A holds f * (id A) = (id A) * f

proof end;

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

proof end;

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

proof end;

theorem :: TRANSGEO:12

canceled;

theorem :: TRANSGEO:13

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:14

canceled;

theorem :: TRANSGEO:15

canceled;

theorem :: TRANSGEO:16

for A being non empty set
for f, g, h being Permutation of A holds (f * g) \ h = (f \ h) * (g \ h)

proof end;

theorem :: TRANSGEO:17

for A being non empty set
for f, g being Permutation of A holds (f " ) \ g = (f \ g) "

proof end;

theorem :: TRANSGEO:18

for A being non empty set
for f, g, h being Permutation of A holds f \ (g * h) = (f \ h) \ g

proof end;

theorem :: TRANSGEO:19

for A being non empty set
for f being Permutation of A holds (id A) \ f = id A

proof end;

theorem :: TRANSGEO:20

for A being non empty set
for f being Permutation of A holds f \ (id A) = f

proof end;

theorem :: TRANSGEO:21

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

proof end;

definition

let A be non empty set ;
let f be Permutation of A;
let R be Relation of [:A,A:];
pred f 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 :

theorem :: TRANSGEO:22

canceled;

theorem Th23: :: TRANSGEO:23

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

proof end;

theorem Th24: :: TRANSGEO:24

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

proof end;

theorem :: TRANSGEO:25

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

proof end;

theorem Th26: :: TRANSGEO:26

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 & [[a,b],[z,t]] in R & a <> b holds
[[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & f is_FormalIz_of R & g is_FormalIz_of R holds
f * g is_FormalIz_of R

proof end;

definition

let A be non empty set ;
let f be Permutation of A;
let R be Relation of [:A,A:];
pred f 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 :

theorem :: TRANSGEO:27

canceled;

theorem Th28: :: TRANSGEO:28

for A being non empty set
for R being Relation of [:A,A:] holds id A is_automorphism_of R

proof end;

theorem Th29: :: TRANSGEO:29

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

proof end;

theorem Th30: :: TRANSGEO:30

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 & g is_automorphism_of R holds
g * f is_automorphism_of R

proof end;

theorem :: TRANSGEO:31

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:] & R is_transitive_in [:A,A:] & f is_FormalIz_of R holds
f is_automorphism_of R

proof end;

theorem :: TRANSGEO:32

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 & [[a,b],[z,t]] in R & a <> b holds
[[x,y],[z,t]] in R ) & ( for x, y, z being Element of A holds [[x,x],[y,z]] in R ) & R is_symmetric_in [:A,A:] & f is_FormalIz_of R holds
f is_automorphism_of R

proof end;

theorem :: TRANSGEO:33

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 & g is_automorphism_of R holds
f \ g is_FormalIz_of R

proof end;

definition

let AS be non empty AffinStruct ;
let f be Permutation of the carrier of AS;
pred f 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 :

theorem :: TRANSGEO:34

canceled;

theorem Th35: :: TRANSGEO:35

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 )

proof end;

definition

let IT be non empty AffinStruct ;
attr IT is CongrSpace-like means :Def5: :: 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;

:: deftheorem Def5 defines CongrSpace-like TRANSGEO:def 5 :

registration

cluster non empty strict CongrSpace-like AffinStruct ;
existence

proof end;

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:]

proof end;

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

proof end;

theorem :: TRANSGEO:36

canceled;

theorem Th37: :: TRANSGEO:37

for CS being CongrSpace holds id the carrier of CS is_DIL_of CS

proof end;

theorem Th38: :: TRANSGEO:38

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

proof end;

theorem Th39: :: TRANSGEO:39

for CS being CongrSpace
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 end;

theorem Th40: :: TRANSGEO:40

for OAS being OAffinSpace holds OAS is CongrSpace-like

proof end;

definition

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

end;

:: deftheorem Def6 defines positive_dilatation TRANSGEO:def 6 :

notation

let OAS be OAffinSpace;
let f be Permutation of the carrier of OAS;
synonym f is_CDil for positive_dilatation f;

end;

theorem :: TRANSGEO:41

canceled;

theorem Th42: :: TRANSGEO:42

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS holds
( f is_CDil iff for a, b being Element of OAS holds a,b // f . a,f . b )

proof end;

definition

let OAS be OAffinSpace;
let f be Permutation of the carrier of OAS;
attr f 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 :

notation

let OAS be OAffinSpace;
let f be Permutation of the carrier of OAS;
synonym f is_SDil for negative_dilatation f;

end;

theorem :: TRANSGEO:43

canceled;

theorem Th44: :: TRANSGEO:44

for OAS being OAffinSpace holds id the carrier of OAS is_CDil

proof end;

theorem :: TRANSGEO:45

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is_CDil holds
f " is_CDil

proof end;

theorem :: TRANSGEO:46

for OAS being OAffinSpace
for f, g being Permutation of the carrier of OAS st f is_CDil & g is_CDil holds
f * g is_CDil

proof end;

theorem :: TRANSGEO:47

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS holds
( not f is_SDil or not f is_CDil )

proof end;

theorem :: TRANSGEO:48

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is_SDil holds
f " is_SDil

proof end;

theorem :: TRANSGEO:49

for OAS being OAffinSpace
for f, g being Permutation of the carrier of OAS st f is_CDil & g is_SDil holds
( f * g is_SDil & g * f is_SDil )

proof end;

definition

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

end;

:: deftheorem Def8 defines dilatation TRANSGEO:def 8 :

notation

let OAS be OAffinSpace;
let f be Permutation of the carrier of OAS;
synonym f is_Dil for dilatation f;

end;

theorem :: TRANSGEO:50

canceled;

theorem Th51: :: TRANSGEO:51

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS holds
( f is_Dil iff for a, b being Element of OAS holds a,b '||' f . a,f . b )

proof end;

theorem :: TRANSGEO:52

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st ( f is_CDil or f is_SDil ) holds
f is_Dil

proof end;

theorem :: TRANSGEO:53

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is_Dil holds
ex f' being Permutation of the carrier of (Lambda OAS) st
( f = f' & f' is_DIL_of Lambda OAS )

proof end;

theorem :: TRANSGEO:54

for OAS being OAffinSpace
for f being Permutation of the carrier of (Lambda OAS) st f is_DIL_of Lambda OAS holds
ex f' being Permutation of the carrier of OAS st
( f = f' & f' is_Dil )

proof end;

theorem :: TRANSGEO:55

for OAS being OAffinSpace holds id the carrier of OAS is_Dil

proof end;

theorem Th56: :: TRANSGEO:56

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is_Dil holds
f " is_Dil

proof end;

theorem Th57: :: TRANSGEO:57

for OAS being OAffinSpace
for f, g being Permutation of the carrier of OAS st f is_Dil & g is_Dil holds
f * g is_Dil

proof end;

theorem Th58: :: TRANSGEO:58

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is_Dil holds
for a, b, c, d being Element of OAS holds
( a,b '||' c,d iff f . a,f . b '||' f . c,f . d )

proof end;

theorem Th59: :: TRANSGEO:59

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is_Dil holds
for a, b, c being Element of OAS holds
( LIN a,b,c iff LIN f . a,f . b,f . c )

proof end;

theorem Th60: :: TRANSGEO:60

for OAS being OAffinSpace
for x, y being Element of OAS
for f being Permutation of the carrier of OAS st f is_Dil & LIN x,f . x,y holds
LIN x,f . x,f . y

proof end;

theorem Th61: :: TRANSGEO:61

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 & LIN b,d,x ) )

proof end;

theorem Th62: :: TRANSGEO:62

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is_Dil 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 )

proof end;

theorem Th63: :: TRANSGEO:63

for OAS being OAffinSpace
for a, b, x being Element of OAS
for f being Permutation of the carrier of OAS st f is_Dil & f . a = a & f . b = b & not LIN a,b,x holds
f . x = x

proof end;

theorem Th64: :: TRANSGEO:64

for OAS being OAffinSpace
for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is_Dil & f . a = a & f . b = b & a <> b holds
f = id the carrier of OAS

proof end;

theorem :: TRANSGEO:65

for OAS being OAffinSpace
for a, b being Element of OAS
for f, g being Permutation of the carrier of OAS st f is_Dil & g is_Dil & f . a = g . a & f . b = g . b & not a = b holds
f = g

proof end;

definition

let OAS be OAffinSpace;
let f be Permutation of the carrier of OAS;
attr f is translation means :Def9: :: TRANSGEO:def 9
( f is_Dil & ( 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 :

notation

let OAS be OAffinSpace;
let f be Permutation of the carrier of OAS;
synonym f is_Tr for translation f;

end;

theorem :: TRANSGEO:66

canceled;

theorem Th67: :: TRANSGEO:67

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is_Dil holds
( f is_Tr iff for x, y being Element of OAS holds x,f . x '||' y,f . y )

proof end;

theorem :: TRANSGEO:68

canceled;

theorem Th69: :: TRANSGEO:69

for OAS being OAffinSpace
for a, x being Element of OAS
for f, g being Permutation of the carrier of OAS st f is_Tr & g is_Tr & f . a = g . a & not LIN a,f . a,x holds
f . x = g . x

proof end;

theorem Th70: :: TRANSGEO:70

for OAS being OAffinSpace
for a being Element of OAS
for f, g being Permutation of the carrier of OAS st f is_Tr & g is_Tr & f . a = g . a holds
f = g

proof end;

theorem Th71: :: TRANSGEO:71

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is_Tr holds
f " is_Tr

proof end;

theorem :: TRANSGEO:72

for OAS being OAffinSpace
for f, g being Permutation of the carrier of OAS st f is_Tr & g is_Tr holds
f * g is_Tr

proof end;

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

proof end;

Lm6: for OAS being OAffinSpace
for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is_Tr & a <> f . a & LIN a,f . a,b holds
a,f . a // b,f . b

proof end;

Lm7: for OAS being OAffinSpace
for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is_Tr & Mid a,f . a,b & a <> f . a holds
a,b // f . a,f . b

proof end;

Lm8: for OAS being OAffinSpace
for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is_Tr & a <> f . a & b <> f . a & Mid a,b,f . a holds
a,b // f . a,f . b

proof end;

Lm9: for OAS being OAffinSpace
for a, b being Element of OAS
for f being Permutation of the carrier of OAS st f is_Tr & a <> f . a & LIN a,f . a,b holds
a,b // f . a,f . b

proof end;

theorem Th73: :: TRANSGEO:73

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS st f is_Tr holds
f is_CDil

proof end;

theorem Th74: :: TRANSGEO:74

for OAS being OAffinSpace
for p, q, x being Element of OAS
for f being Permutation of the carrier of OAS st f is_Dil & f . p = p & Mid q,p,f . q & not LIN p,q,x holds
Mid x,p,f . x

proof end;

theorem Th75: :: TRANSGEO:75

for OAS being OAffinSpace
for p, q, x being Element of OAS
for f being Permutation of the carrier of OAS st f is_Dil & f . p = p & Mid q,p,f . q & q <> p holds
Mid x,p,f . x

proof end;

theorem Th76: :: TRANSGEO:76

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_Dil & f . p = p & q <> p & Mid q,p,f . q & not LIN p,x,y holds
x,y // f . y,f . x

proof end;

theorem Th77: :: TRANSGEO:77

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_Dil & f . p = p & q <> p & Mid q,p,f . q & LIN p,x,y holds
x,y // f . y,f . x

proof end;

theorem Th78: :: TRANSGEO:78

for OAS being OAffinSpace
for p, q being Element of OAS
for f being Permutation of the carrier of OAS st f is_Dil & f . p = p & q <> p & Mid q,p,f . q holds
f is_SDil

proof end;

theorem Th79: :: TRANSGEO:79

for OAS being OAffinSpace
for p being Element of OAS
for f being Permutation of the carrier of OAS st f is_Dil & f . p = p & ( 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

proof end;

theorem :: TRANSGEO:80

for OAS being OAffinSpace
for f being Permutation of the carrier of OAS holds
( not f is_Dil or f is_CDil or f is_SDil )

proof end;

theorem :: TRANSGEO:81

canceled;

theorem Th82: :: TRANSGEO:82

for AFS being AffinSpace holds AFS is CongrSpace-like

proof end;

theorem :: TRANSGEO:83

for OAS being OAffinSpace holds Lambda OAS is CongrSpace

proof end;

definition

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

end;

:: deftheorem Def10 defines dilatation TRANSGEO:def 10 :

notation

let AFS be AffinSpace;
let f be Permutation of the carrier of AFS;
synonym f is_Dil for dilatation f;

end;

theorem :: TRANSGEO:84

canceled;

theorem Th85: :: TRANSGEO:85

for AFS being AffinSpace
for f being Permutation of the carrier of AFS holds
( f is_Dil iff for a, b being Element of AFS holds a,b // f . a,f . b )

proof end;

theorem Th86: :: TRANSGEO:86

for AFS being AffinSpace holds id the carrier of AFS is_Dil

proof end;

theorem Th87: :: TRANSGEO:87

for AFS being AffinSpace
for f being Permutation of the carrier of AFS st f is_Dil holds
f " is_Dil

proof end;

theorem Th88: :: TRANSGEO:88

for AFS being AffinSpace
for f, g being Permutation of the carrier of AFS st f is_Dil & g is_Dil holds
f * g is_Dil

proof end;

theorem Th89: :: TRANSGEO:89

for AFS being AffinSpace
for f being Permutation of the carrier of AFS st f is_Dil holds
for a, b, c, d being Element of AFS holds
( a,b // c,d iff f . a,f . b // f . c,f . d )

proof end;

theorem :: TRANSGEO:90

for AFS being AffinSpace
for f being Permutation of the carrier of AFS st f is_Dil holds
for a, b, c being Element of AFS holds
( LIN a,b,c iff LIN f . a,f . b,f . c )

proof end;

theorem Th91: :: TRANSGEO:91

for AFS being AffinSpace
for x, y being Element of AFS
for f being Permutation of the carrier of AFS st f is_Dil & LIN x,f . x,y holds
LIN x,f . x,f . y

proof end;

theorem Th92: :: TRANSGEO:92

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 & LIN b,d,x ) )

proof end;

theorem Th93: :: TRANSGEO:93

for AFS being AffinSpace
for f being Permutation of the carrier of AFS st f is_Dil 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 )

proof end;

theorem Th94: :: TRANSGEO:94

for AFS being AffinSpace
for a, b, x being Element of AFS
for f being Permutation of the carrier of AFS st f is_Dil & f . a = a & f . b = b & not LIN a,b,x holds
f . x = x

proof end;

theorem Th95: :: TRANSGEO:95

for AFS being AffinSpace
for a, b being Element of AFS
for f being Permutation of the carrier of AFS st f is_Dil & f . a = a & f . b = b & a <> b holds
f = id the carrier of AFS

proof end;

theorem :: TRANSGEO:96

for AFS being AffinSpace
for a, b being Element of AFS
for f, g being Permutation of the carrier of AFS st f is_Dil & g is_Dil & f . a = g . a & f . b = g . b & not a = b holds
f = g

proof end;

theorem Th97: :: TRANSGEO:97

for AFS being AffinSpace
for a, b, c, d1, d2 being Element of AFS st not LIN a,b,c & a,b // c,d1 & a,b // c,d2 & a,c // b,d1 & a,c // b,d2 holds
d1 = d2

proof end;

definition

let AFS be AffinSpace;
let f be Permutation of the carrier of AFS;
attr f is translation means :Def11: :: TRANSGEO:def 11
( f is_Dil & ( 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 :

notation

let AFS be AffinSpace;
let f be Permutation of the carrier of AFS;
synonym f is_Tr for translation f;

end;

theorem :: TRANSGEO:98

canceled;

theorem :: TRANSGEO:99

for AFS being AffinSpace holds id the carrier of AFS is_Tr

proof end;

theorem Th100: :: TRANSGEO:100

for AFS being AffinSpace
for f being Permutation of the carrier of AFS st f is_Dil holds
( f is_Tr iff for x, y being Element of AFS holds x,f . x // y,f . y )

proof end;

theorem :: TRANSGEO:101

canceled;

theorem Th102: :: TRANSGEO:102

for AFS being AffinSpace
for a, x being Element of AFS
for f, g being Permutation of the carrier of AFS st f is_Tr & g is_Tr & f . a = g . a & not LIN a,f . a,x holds
f . x = g . x

proof end;

theorem Th103: :: TRANSGEO:103

for AFS being AffinSpace
for a being Element of AFS
for f, g being Permutation of the carrier of AFS st f is_Tr & g is_Tr & f . a = g . a holds
f = g

proof end;

theorem Th104: :: TRANSGEO:104

for AFS being AffinSpace
for f being Permutation of the carrier of AFS st f is_Tr holds
f " is_Tr

proof end;

theorem :: TRANSGEO:105

for AFS being AffinSpace
for f, g being Permutation of the carrier of AFS st f is_Tr & g is_Tr holds
f * g is_Tr

proof end;

definition

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

end;

:: deftheorem defines collineation TRANSGEO:def 12 :

notation

let AFS be AffinSpace;
let f be Permutation of the carrier of AFS;
synonym f is_Col for collineation f;

end;

theorem :: TRANSGEO:106

canceled;

theorem Th107: :: TRANSGEO:107

for AFS being AffinSpace
for f being Permutation of the carrier of AFS holds
( f is_Col iff for x, y, z, t being Element of AFS holds
( x,y // z,t iff f . x,f . y // f . z,f . t ) )

proof end;

theorem Th108: :: TRANSGEO:108

for AFS being AffinSpace
for x, y, z being Element of AFS
for f being Permutation of the carrier of AFS st f is_Col holds
( LIN x,y,z iff LIN f . x,f . y,f . z )

proof end;

theorem :: TRANSGEO:109

for AFS being AffinSpace
for f, g being Permutation of the carrier of AFS st f is_Col & g is_Col holds
( f " is_Col & f * g is_Col & id the carrier of AFS is_Col )

proof end;

theorem Th110: :: TRANSGEO:110

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

proof end;

theorem Th111: :: TRANSGEO:111

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 & f . y = x ) )

proof end;

theorem Th112: :: TRANSGEO:112

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

proof end;

theorem Th113: :: TRANSGEO:113

for AFS being AffinSpace
for a, b being Element of AFS
for f being Permutation of the carrier of AFS st f is_Col holds
f .: (Line a,b) = Line (f . a),(f . b)

proof end;

theorem :: TRANSGEO:114

for AFS being AffinSpace
for f being Permutation of the carrier of AFS
for K being Subset of AFS st f is_Col & K is_line holds
f .: K is_line

proof end;

theorem Th115: :: TRANSGEO:115

for AFS being AffinSpace
for f being Permutation of the carrier of AFS
for A, C being Subset of AFS st f is_Col & A // C holds
f .: A // f .: C

proof end;

theorem :: TRANSGEO:116

for AFP being AffinPlane
for f being Permutation of the carrier of AFP st ( for A being Subset of AFP st A is_line holds
f .: A is_line ) holds
f is_Col

proof end;

theorem :: TRANSGEO:117

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_Col & K is_line & ( for x being Element of AFP st x in K holds
f . x = x ) & not p in K & f . p = p holds
f = id the carrier of AFP

proof end;