:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski

::

:: Received May 31, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let A be set ;

let f, g be Permutation of A;

:: original: *

redefine func g * f -> Permutation of A;

coherence

g * f is Permutation of A

end;
let f, g be Permutation of A;

:: original: *

redefine func g * f -> Permutation of A;

coherence

g * f is Permutation of A

proof 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

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 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 )

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;

coherence

(g * f) * (g ") is Permutation of A ;

end;
let f, g be Permutation of A;

coherence

(g * f) * (g ") is Permutation of A ;

:: deftheorem defines \ TRANSGEO:def 1 :

for A being non empty set

for f, g being Permutation of A holds f \ g = (g * f) * (g ");

for A being non empty set

for f, g being Permutation of A holds f \ g = (g * f) * (g ");

scheme :: TRANSGEO:sch 1

EXPermutation{ F_{1}() -> non empty set , P_{1}[ object , object ] } :

EXPermutation{ F

ex f being Permutation of F_{1}() st

for x, y being Element of F_{1}() holds

( f . x = y iff P_{1}[x,y] )

providedfor x, y being Element of F

( f . x = y iff P

A1:
for x being Element of F_{1}() ex y being Element of F_{1}() st P_{1}[x,y]
and

A2: for y being Element of F_{1}() ex x being Element of F_{1}() st P_{1}[x,y]
and

A3: for x, y, x9 being Element of F_{1}() st P_{1}[x,y] & P_{1}[x9,y] holds

x = x9 and

A4: for x, y, y9 being Element of F_{1}() st P_{1}[x,y] & P_{1}[x,y9] holds

y = y9

A2: for y being Element of F

A3: for x, y, x9 being Element of F

x = x9 and

A4: for x, y, y9 being Element of F

y = y9

proof end;

theorem :: TRANSGEO:3

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 f, g, h being Permutation of A st g * f = h * f holds

g = h

proof end;

theorem :: TRANSGEO:5

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

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;

:: deftheorem 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 );

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

for R being Relation of [:A,A:] st R is_reflexive_in [:A,A:] holds

id A is_FormalIz_of R

proof end;

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

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

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 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 & [[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

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;

:: deftheorem 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 ) );

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 :: TRANSGEO:16

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

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

g * f is_automorphism_of R

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

f is_automorphism_of R

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: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 & [[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

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

f \ g is_FormalIz_of R

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;

:: deftheorem 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 );

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 )

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 ;

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

( ( 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 ) );

:: 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 & 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 ) ) );

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 & 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 ) ) );

registration

existence

ex b_{1} being non empty AffinStruct st

( b_{1} is strict & b_{1} is CongrSpace-like )

end;
ex b

( b

proof 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 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 by Lm4, Th13;

for f being Permutation of the carrier of CS st f is_DIL_of CS holds

f " is_DIL_of CS by Lm4, Th13;

theorem Th25: :: TRANSGEO:25

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

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;

:: deftheorem 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 );

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 ) by Th22;

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 ) by Th22;

definition

let OAS be OAffinSpace;

let f be Permutation of the carrier of OAS;

end;
let f be Permutation of the carrier of OAS;

attr f is negative_dilatation means :: TRANSGEO:def 7

for a, b being Element of OAS holds a,b // f . b,f . a;

for a, b being Element of OAS holds a,b // f . b,f . a;

:: deftheorem 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 );

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

for f being Permutation of the carrier of OAS st f is positive_dilatation holds

f " is positive_dilatation

proof end;

theorem :: TRANSGEO:30

for OAS being OAffinSpace

for f, g being Permutation of the carrier of OAS st f is positive_dilatation & g is positive_dilatation holds

f * g is positive_dilatation

for f, g being Permutation of the carrier of OAS st f is positive_dilatation & g is positive_dilatation holds

f * g is positive_dilatation

proof end;

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 )

for f being Permutation of the carrier of OAS holds

( not f is negative_dilatation or not f is positive_dilatation )

proof end;

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

for f being Permutation of the carrier of OAS st f is negative_dilatation holds

f " is negative_dilatation

proof end;

theorem :: TRANSGEO:33

for OAS being OAffinSpace

for f, g being Permutation of the carrier of OAS st f is positive_dilatation & g is negative_dilatation holds

( f * g is negative_dilatation & g * f is negative_dilatation )

for f, g being Permutation of the carrier of OAS st f is positive_dilatation & g is negative_dilatation holds

( f * g is negative_dilatation & g * f is negative_dilatation )

proof end;

:: deftheorem 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 );

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 )

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 )

proof end;

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

for f being Permutation of the carrier of OAS st ( f is positive_dilatation or f is negative_dilatation ) holds

f is dilatation

proof end;

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 & f9 is_DIL_of Lambda OAS )

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 & f9 is_DIL_of Lambda OAS )

proof end;

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 & f9 is dilatation )

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 & f9 is dilatation )

proof end;

theorem :: TRANSGEO:39

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

for f being Permutation of the carrier of OAS st ( f is positive_dilatation or f is negative_dilatation ) holds

f is dilatation

proof end;

theorem :: TRANSGEO:40

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 & f9 is_DIL_of Lambda OAS )

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 & f9 is_DIL_of Lambda OAS )

proof end;

theorem :: TRANSGEO:41

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 & f9 is dilatation )

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 & f9 is dilatation )

proof end;

theorem Th43: :: TRANSGEO:43

for OAS being OAffinSpace

for f being Permutation of the carrier of OAS st f is dilatation holds

f " is dilatation

for f being Permutation of the carrier of OAS st f is dilatation holds

f " is dilatation

proof end;

theorem Th44: :: TRANSGEO:44

for OAS being OAffinSpace

for f, g being Permutation of the carrier of OAS st f is dilatation & g is dilatation holds

f * g is dilatation

for f, g being Permutation of the carrier of OAS st f is dilatation & g is dilatation holds

f * g is dilatation

proof end;

theorem Th45: :: TRANSGEO:45

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 )

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 )

proof end;

theorem Th46: :: TRANSGEO:46

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

( a,b,c are_collinear iff f . a,f . b,f . c are_collinear )

for f being Permutation of the carrier of OAS st f is dilatation holds

for a, b, c being Element of OAS holds

( a,b,c are_collinear iff f . a,f . b,f . c are_collinear )

proof end;

theorem Th47: :: TRANSGEO:47

for OAS being OAffinSpace

for x, y being Element of OAS

for f being Permutation of the carrier of OAS st f is dilatation & x,f . x,y are_collinear holds

x,f . x,f . y are_collinear

for x, y being Element of OAS

for f being Permutation of the carrier of OAS st f is dilatation & x,f . x,y are_collinear holds

x,f . x,f . y are_collinear

proof end;

theorem Th48: :: TRANSGEO:48

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

( a,c,x are_collinear & b,d,x are_collinear ) )

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

( a,c,x are_collinear & b,d,x are_collinear ) )

proof end;

theorem Th49: :: TRANSGEO:49

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 )

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 )

proof end;

theorem Th50: :: TRANSGEO:50

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 & f . a = a & f . b = b & not a,b,x are_collinear holds

f . x = x

for a, b, x being Element of OAS

for f being Permutation of the carrier of OAS st f is dilatation & f . a = a & f . b = b & not a,b,x are_collinear holds

f . x = x

proof end;

theorem Th51: :: TRANSGEO:51

for OAS being OAffinSpace

for a, b being Element of OAS

for f being Permutation of the carrier of OAS st f is dilatation & f . a = a & f . b = b & a <> b holds

f = id the carrier of OAS

for a, b being Element of OAS

for f being Permutation of the carrier of OAS st f is dilatation & f . a = a & f . b = b & a <> b holds

f = id the carrier of OAS

proof end;

theorem :: TRANSGEO:52

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 & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds

f = g

for a, b being Element of OAS

for f, g being Permutation of the carrier of OAS st f is dilatation & g is dilatation & 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;

end;
let f be Permutation of the carrier of OAS;

attr f is translation means :: TRANSGEO:def 9

( f is dilatation & ( f = id the carrier of OAS or for a being Element of OAS holds a <> f . a ) );

( f is dilatation & ( f = id the carrier of OAS or for a being Element of OAS holds a <> f . a ) );

:: deftheorem 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 & ( f = id the carrier of OAS or for a being Element of OAS holds a <> f . a ) ) );

for OAS being OAffinSpace

for f being Permutation of the carrier of OAS holds

( f is translation iff ( f is dilatation & ( f = id the carrier of OAS or for a being Element of OAS holds a <> f . a ) ) );

theorem Th53: :: TRANSGEO:53

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 ) by Th49;

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 ) by Th49;

theorem Th54: :: TRANSGEO:54

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 & g is translation & f . a = g . a & not a,f . a,x are_collinear holds

f . x = g . x

for a, x being Element of OAS

for f, g being Permutation of the carrier of OAS st f is translation & g is translation & f . a = g . a & not a,f . a,x are_collinear holds

f . x = g . x

proof end;

theorem Th55: :: TRANSGEO:55

for OAS being OAffinSpace

for a being Element of OAS

for f, g being Permutation of the carrier of OAS st f is translation & g is translation & f . a = g . a holds

f = g

for a being Element of OAS

for f, g being Permutation of the carrier of OAS st f is translation & g is translation & f . a = g . a holds

f = g

proof end;

theorem Th56: :: TRANSGEO:56

for OAS being OAffinSpace

for f being Permutation of the carrier of OAS st f is translation holds

f " is translation

for f being Permutation of the carrier of OAS st f is translation holds

f " is translation

proof end;

theorem :: TRANSGEO:57

for OAS being OAffinSpace

for f, g being Permutation of the carrier of OAS st f is translation & g is translation holds

f * g is translation

for f, g being Permutation of the carrier of OAS st f is translation & g is translation holds

f * g is translation

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 translation & not a,f . a,b are_collinear 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 translation & a <> f . a & a,f . a,b are_collinear 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 translation & 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 translation & 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 translation & a <> f . a & a,f . a,b are_collinear holds

a,b // f . a,f . b

proof end;

theorem Th58: :: TRANSGEO:58

for OAS being OAffinSpace

for f being Permutation of the carrier of OAS st f is translation holds

f is positive_dilatation

for f being Permutation of the carrier of OAS st f is translation holds

f is positive_dilatation

proof end;

theorem Th59: :: TRANSGEO:59

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 & f . p = p & Mid q,p,f . q & not p,q,x are_collinear holds

Mid x,p,f . x

for p, q, x being Element of OAS

for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & not p,q,x are_collinear holds

Mid x,p,f . x

proof end;

theorem Th60: :: TRANSGEO:60

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 & f . p = p & Mid q,p,f . q & q <> p holds

Mid x,p,f . x

for p, q, x being Element of OAS

for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & Mid q,p,f . q & q <> p holds

Mid x,p,f . x

proof end;

theorem Th61: :: TRANSGEO:61

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

x,y // f . y,f . x

for p, q, x, y being Element of OAS

for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q & not p,x,y are_collinear holds

x,y // f . y,f . x

proof end;

theorem Th62: :: TRANSGEO:62

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

x,y // f . y,f . x

for p, q, x, y being Element of OAS

for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q & p,x,y are_collinear holds

x,y // f . y,f . x

proof end;

theorem Th63: :: TRANSGEO:63

for OAS being OAffinSpace

for p, q being Element of OAS

for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q holds

f is negative_dilatation

for p, q being Element of OAS

for f being Permutation of the carrier of OAS st f is dilatation & f . p = p & q <> p & Mid q,p,f . q holds

f is negative_dilatation

proof end;

theorem Th64: :: TRANSGEO:64

for OAS being OAffinSpace

for p being Element of OAS

for f being Permutation of the carrier of OAS st f is dilatation & 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

for p being Element of OAS

for f being Permutation of the carrier of OAS st f is dilatation & 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:65

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 )

for f being Permutation of the carrier of OAS holds

( not f is dilatation or f is positive_dilatation or f is negative_dilatation )

proof end;

:: deftheorem 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 );

for AFS being AffinSpace

for f being Permutation of the carrier of AFS holds

( f is dilatation iff f is_DIL_of AFS );

theorem Th68: :: TRANSGEO:68

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 ) by Th22;

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 ) by Th22;

theorem Th70: :: TRANSGEO:70

for AFS being AffinSpace

for f being Permutation of the carrier of AFS st f is dilatation holds

f " is dilatation

for f being Permutation of the carrier of AFS st f is dilatation holds

f " is dilatation

proof end;

theorem Th71: :: TRANSGEO:71

for AFS being AffinSpace

for f, g being Permutation of the carrier of AFS st f is dilatation & g is dilatation holds

f * g is dilatation

for f, g being Permutation of the carrier of AFS st f is dilatation & g is dilatation holds

f * g is dilatation

proof end;

theorem Th72: :: TRANSGEO:72

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 )

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 )

proof end;

theorem :: TRANSGEO:73

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 )

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 )

proof end;

theorem Th74: :: TRANSGEO:74

for AFS being AffinSpace

for x, y being Element of AFS

for f being Permutation of the carrier of AFS st f is dilatation & LIN x,f . x,y holds

LIN x,f . x,f . y

for x, y being Element of AFS

for f being Permutation of the carrier of AFS st f is dilatation & LIN x,f . x,y holds

LIN x,f . x,f . y

proof end;

theorem Th75: :: TRANSGEO:75

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 ) )

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 Th76: :: TRANSGEO:76

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 )

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 )

proof end;

theorem Th77: :: TRANSGEO:77

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 & f . a = a & f . b = b & not LIN a,b,x holds

f . x = x

for a, b, x being Element of AFS

for f being Permutation of the carrier of AFS st f is dilatation & f . a = a & f . b = b & not LIN a,b,x holds

f . x = x

proof end;

theorem Th78: :: TRANSGEO:78

for AFS being AffinSpace

for a, b being Element of AFS

for f being Permutation of the carrier of AFS st f is dilatation & f . a = a & f . b = b & a <> b holds

f = id the carrier of AFS

for a, b being Element of AFS

for f being Permutation of the carrier of AFS st f is dilatation & f . a = a & f . b = b & a <> b holds

f = id the carrier of AFS

proof end;

theorem :: TRANSGEO:79

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 & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds

f = g

for a, b being Element of AFS

for f, g being Permutation of the carrier of AFS st f is dilatation & g is dilatation & f . a = g . a & f . b = g . b & not a = b holds

f = g

proof end;

theorem Th80: :: TRANSGEO:80

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

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;

end;
let f be Permutation of the carrier of AFS;

attr f is translation means :: TRANSGEO:def 11

( f is dilatation & ( f = id the carrier of AFS or for a being Element of AFS holds a <> f . a ) );

( f is dilatation & ( f = id the carrier of AFS or for a being Element of AFS holds a <> f . a ) );

:: deftheorem 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 & ( f = id the carrier of AFS or for a being Element of AFS holds a <> f . a ) ) );

for AFS being AffinSpace

for f being Permutation of the carrier of AFS holds

( f is translation iff ( f is dilatation & ( f = id the carrier of AFS or for a being Element of AFS holds a <> f . a ) ) );

theorem Th82: :: TRANSGEO:82

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 ) by Th76;

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 ) by Th76;

theorem Th83: :: TRANSGEO:83

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 & g is translation & f . a = g . a & not LIN a,f . a,x holds

f . x = g . x

for a, x being Element of AFS

for f, g being Permutation of the carrier of AFS st f is translation & g is translation & f . a = g . a & not LIN a,f . a,x holds

f . x = g . x

proof end;

theorem Th84: :: TRANSGEO:84

for AFS being AffinSpace

for a being Element of AFS

for f, g being Permutation of the carrier of AFS st f is translation & g is translation & f . a = g . a holds

f = g

for a being Element of AFS

for f, g being Permutation of the carrier of AFS st f is translation & g is translation & f . a = g . a holds

f = g

proof end;

theorem Th85: :: TRANSGEO:85

for AFS being AffinSpace

for f being Permutation of the carrier of AFS st f is translation holds

f " is translation

for f being Permutation of the carrier of AFS st f is translation holds

f " is translation

proof end;

theorem :: TRANSGEO:86

for AFS being AffinSpace

for f, g being Permutation of the carrier of AFS st f is translation & g is translation holds

f * g is translation

for f, g being Permutation of the carrier of AFS st f is translation & g is translation holds

f * g is translation

proof 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 );

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 Th87: :: TRANSGEO:87

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 ) )

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 ) )

proof end;

theorem Th88: :: TRANSGEO:88

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 )

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 )

proof end;

theorem :: TRANSGEO:89

for AFS being AffinSpace

for f, g being Permutation of the carrier of AFS st f is collineation & g is collineation holds

( f " is collineation & f * g is collineation & id the carrier of AFS is collineation )

for f, g being Permutation of the carrier of AFS st f is collineation & g is collineation holds

( f " is collineation & f * g is collineation & id the carrier of AFS is collineation )

proof end;

theorem Th90: :: TRANSGEO:90

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

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 Th91: :: TRANSGEO:91

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 ) )

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 Th92: :: TRANSGEO:92

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

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 Th93: :: TRANSGEO:93

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))

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))

proof end;

theorem :: TRANSGEO:94

for AFS being AffinSpace

for f being Permutation of the carrier of AFS

for K being Subset of AFS st f is collineation & K is being_line holds

f .: K is being_line

for f being Permutation of the carrier of AFS

for K being Subset of AFS st f is collineation & K is being_line holds

f .: K is being_line

proof end;

theorem Th95: :: TRANSGEO:95

for AFS being AffinSpace

for f being Permutation of the carrier of AFS

for A, C being Subset of AFS st f is collineation & A // C holds

f .: A // f .: C

for f being Permutation of the carrier of AFS

for A, C being Subset of AFS st f is collineation & A // C holds

f .: A // f .: C

proof end;

theorem :: TRANSGEO:96

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

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

proof end;

theorem :: TRANSGEO:97

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 & K is being_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

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 & K is being_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;