:: TRANSGEO semantic presentation

definition

let c₁ be set ;
let c₂, c₃ be Permutation of c₁;
redefine func * as c₃ * c₂ -> Permutation of a₁;
coherence

proof end;

end;

theorem Th1: :: TRANSGEO:1

canceled;

theorem Th2: :: TRANSGEO:2

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being Permutation of b₁ ex b₄ being Element of b₁ st b₃ . b₄ = b₂

proof end;

theorem Th3: :: TRANSGEO:3

canceled;

theorem Th4: :: TRANSGEO:4

for b₁ being non empty set
for b₂, b₃ being Element of b₁
for b₄ being Permutation of b₁ holds
( b₄ . b₂ = b₃ iff (b₄ " ) . b₃ = b₂ )

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Permutation of c₁;
func c₂ \ c₃ -> Permutation of a₁ equals :: TRANSGEO:def 1
(a₃ * a₂) * (a₃ " );
coherence ;

end;

:: deftheorem Def1 defines \ TRANSGEO:def 1 :

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

ex b₁ being Permutation of F₁() st
for b₂, b₃ being Element of F₁() holds
( b₁ . b₂ = b₃ iff P₁[b₂,b₃] )

provided

E3: for b₁ being Element of F₁() ex b₂ being Element of F₁() st P₁[b₁,b₂] and
E4: for b₁ being Element of F₁() ex b₂ being Element of F₁() st P₁[b₂,b₁] and
E5: for b₁, b₂, b₃ being Element of F₁() st P₁[b₁,b₂] & P₁[b₃,b₂] holds
b₁ = b₃ and
E6: for b₁, b₂, b₃ being Element of F₁() st P₁[b₁,b₂] & P₁[b₁,b₃] holds
b₂ = b₃

proof end;

theorem Th5: :: TRANSGEO:5

canceled;

theorem Th6: :: TRANSGEO:6

canceled;

theorem Th7: :: TRANSGEO:7

canceled;

theorem Th8: :: TRANSGEO:8

canceled;

theorem Th9: :: TRANSGEO:9

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being Permutation of b₁ holds
( b₃ . ((b₃ " ) . b₂) = b₂ & (b₃ " ) . (b₃ . b₂) = b₂ ) by Th4;

theorem Th10: :: TRANSGEO:10

canceled;

theorem Th11: :: TRANSGEO:11

for b₁ being non empty set
for b₂ being Permutation of b₁ holds b₂ * (id b₁) = (id b₁) * b₂

proof end;

Lemma3: for b₁ being non empty set
for b₂, b₃, b₄ being Permutation of b₁ st b₂ * b₃ = b₂ * b₄ holds
b₃ = b₄

proof end;

Lemma4: for b₁ being non empty set
for b₂, b₃, b₄ being Permutation of b₁ st b₂ * b₃ = b₄ * b₃ holds
b₂ = b₄

proof end;

theorem Th12: :: TRANSGEO:12

canceled;

theorem Th13: :: TRANSGEO:13

for b₁ being non empty set
for b₂, b₃, b₄ being Permutation of b₁ st ( b₂ * b₃ = b₄ * b₃ or b₃ * b₂ = b₃ * b₄ ) holds
b₂ = b₄ by Lemma3, Lemma4;

theorem Th14: :: TRANSGEO:14

canceled;

theorem Th15: :: TRANSGEO:15

canceled;

theorem Th16: :: TRANSGEO:16

for b₁ being non empty set
for b₂, b₃, b₄ being Permutation of b₁ holds (b₂ * b₃) \ b₄ = (b₂ \ b₄) * (b₃ \ b₄)

proof end;

theorem Th17: :: TRANSGEO:17

for b₁ being non empty set
for b₂, b₃ being Permutation of b₁ holds (b₂ " ) \ b₃ = (b₂ \ b₃) "

proof end;

theorem Th18: :: TRANSGEO:18

for b₁ being non empty set
for b₂, b₃, b₄ being Permutation of b₁ holds b₂ \ (b₃ * b₄) = (b₂ \ b₄) \ b₃

proof end;

theorem Th19: :: TRANSGEO:19

for b₁ being non empty set
for b₂ being Permutation of b₁ holds (id b₁) \ b₂ = id b₁

proof end;

theorem Th20: :: TRANSGEO:20

for b₁ being non empty set
for b₂ being Permutation of b₁ holds b₂ \ (id b₁) = b₂

proof end;

theorem Th21: :: TRANSGEO:21

for b₁ being non empty set
for b₂ being Element of b₁
for b₃, b₄ being Permutation of b₁ st b₃ . b₂ = b₂ holds
(b₃ \ b₄) . (b₄ . b₂) = b₄ . b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be Permutation of c₁;
let c₃ be Relation of [:c₁,c₁:];
pred c₂ is_FormalIz_of c₃ means :Def2: :: TRANSGEO:def 2
for b₁, b₂ being Element of a₁ holds [[b₁,b₂],[(a₂ . b₁),(a₂ . b₂)]] in a₃;

end;

:: deftheorem Def2 defines is_FormalIz_of TRANSGEO:def 2 :

theorem Th22: :: TRANSGEO:22

canceled;

theorem Th23: :: TRANSGEO:23

for b₁ being non empty set
for b₂ being Relation of [:b₁,b₁:] st b₂ is_reflexive_in [:b₁,b₁:] holds
id b₁ is_FormalIz_of b₂

proof end;

theorem Th24: :: TRANSGEO:24

for b₁ being non empty set
for b₂ being Permutation of b₁
for b₃ being Relation of [:b₁,b₁:] st b₃ is_symmetric_in [:b₁,b₁:] & b₂ is_FormalIz_of b₃ holds
b₂ " is_FormalIz_of b₃

proof end;

theorem Th25: :: TRANSGEO:25

for b₁ being non empty set
for b₂, b₃ being Permutation of b₁
for b₄ being Relation of [:b₁,b₁:] st b₄ is_transitive_in [:b₁,b₁:] & b₂ is_FormalIz_of b₄ & b₃ is_FormalIz_of b₄ holds
b₂ * b₃ is_FormalIz_of b₄

proof end;

theorem Th26: :: TRANSGEO:26

for b₁ being non empty set
for b₂, b₃ being Permutation of b₁
for b₄ being Relation of [:b₁,b₁:] st ( for b₅, b₆, b₇, b₈, b₉, b₁₀ being Element of b₁ st [[b₇,b₈],[b₅,b₆]] in b₄ & [[b₅,b₆],[b₉,b₁₀]] in b₄ & b₅ <> b₆ holds
[[b₇,b₈],[b₉,b₁₀]] in b₄ ) & ( for b₅, b₆, b₇ being Element of b₁ holds [[b₅,b₅],[b₆,b₇]] in b₄ ) & b₂ is_FormalIz_of b₄ & b₃ is_FormalIz_of b₄ holds
b₂ * b₃ is_FormalIz_of b₄

proof end;

definition

let c₁ be non empty set ;
let c₂ be Permutation of c₁;
let c₃ be Relation of [:c₁,c₁:];
pred c₂ is_automorphism_of c₃ means :Def3: :: TRANSGEO:def 3
for b₁, b₂, b₃, b₄ being Element of a₁ holds
( [[b₁,b₂],[b₃,b₄]] in a₃ iff [[(a₂ . b₁),(a₂ . b₂)],[(a₂ . b₃),(a₂ . b₄)]] in a₃ );

end;

:: deftheorem Def3 defines is_automorphism_of TRANSGEO:def 3 :

theorem Th27: :: TRANSGEO:27

canceled;

theorem Th28: :: TRANSGEO:28

for b₁ being non empty set
for b₂ being Relation of [:b₁,b₁:] holds id b₁ is_automorphism_of b₂

proof end;

theorem Th29: :: TRANSGEO:29

for b₁ being non empty set
for b₂ being Permutation of b₁
for b₃ being Relation of [:b₁,b₁:] st b₂ is_automorphism_of b₃ holds
b₂ " is_automorphism_of b₃

proof end;

theorem Th30: :: TRANSGEO:30

for b₁ being non empty set
for b₂, b₃ being Permutation of b₁
for b₄ being Relation of [:b₁,b₁:] st b₂ is_automorphism_of b₄ & b₃ is_automorphism_of b₄ holds
b₃ * b₂ is_automorphism_of b₄

proof end;

theorem Th31: :: TRANSGEO:31

for b₁ being non empty set
for b₂ being Permutation of b₁
for b₃ being Relation of [:b₁,b₁:] st b₃ is_symmetric_in [:b₁,b₁:] & b₃ is_transitive_in [:b₁,b₁:] & b₂ is_FormalIz_of b₃ holds
b₂ is_automorphism_of b₃

proof end;

theorem Th32: :: TRANSGEO:32

for b₁ being non empty set
for b₂ being Permutation of b₁
for b₃ being Relation of [:b₁,b₁:] st ( for b₄, b₅, b₆, b₇, b₈, b₉ being Element of b₁ st [[b₆,b₇],[b₄,b₅]] in b₃ & [[b₄,b₅],[b₈,b₉]] in b₃ & b₄ <> b₅ holds
[[b₆,b₇],[b₈,b₉]] in b₃ ) & ( for b₄, b₅, b₆ being Element of b₁ holds [[b₄,b₄],[b₅,b₆]] in b₃ ) & b₃ is_symmetric_in [:b₁,b₁:] & b₂ is_FormalIz_of b₃ holds
b₂ is_automorphism_of b₃

proof end;

theorem Th33: :: TRANSGEO:33

for b₁ being non empty set
for b₂, b₃ being Permutation of b₁
for b₄ being Relation of [:b₁,b₁:] st b₂ is_FormalIz_of b₄ & b₃ is_automorphism_of b₄ holds
b₂ \ b₃ is_FormalIz_of b₄

proof end;

definition

let c₁ be non empty AffinStruct ;
let c₂ be Permutation of the carrier of c₁;
pred c₂ is_DIL_of c₁ means :Def4: :: TRANSGEO:def 4
a₂ is_FormalIz_of the CONGR of a₁;

end;

:: deftheorem Def4 defines is_DIL_of TRANSGEO:def 4 :

theorem Th34: :: TRANSGEO:34

canceled;

theorem Th35: :: TRANSGEO:35

for b₁ being non empty AffinStruct
for b₂ being Permutation of the carrier of b₁ holds
( b₂ is_DIL_of b₁ iff for b₃, b₄ being Element of b₁ holds b₃,b₄ // b₂ . b₃,b₂ . b₄ )

proof end;

definition

let c₁ be non empty AffinStruct ;
attr a₁ is CongrSpace-like means :Def5: :: TRANSGEO:def 5
( ( for b₁, b₂, b₃, b₄, b₅, b₆ being Element of a₁ st b₁,b₂ // b₅,b₆ & b₅,b₆ // b₃,b₄ & b₅ <> b₆ holds
b₁,b₂ // b₃,b₄ ) & ( for b₁, b₂, b₃ being Element of a₁ holds b₁,b₁ // b₂,b₃ ) & ( for b₁, b₂, b₃, b₄ being Element of a₁ st b₁,b₂ // b₃,b₄ holds
b₃,b₄ // b₁,b₂ ) & ( for b₁, b₂ being Element of a₁ holds b₁,b₂ // b₁,b₂ ) );

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;

Lemma16: for b₁ being CongrSpace holds the CONGR of b₁ is_reflexive_in [:the carrier of b₁,the carrier of b₁:]

proof end;

Lemma17: for b₁ being CongrSpace holds the CONGR of b₁ is_symmetric_in [:the carrier of b₁,the carrier of b₁:]

proof end;

theorem Th36: :: TRANSGEO:36

canceled;

theorem Th37: :: TRANSGEO:37

for b₁ being CongrSpace holds id the carrier of b₁ is_DIL_of b₁

proof end;

theorem Th38: :: TRANSGEO:38

for b₁ being CongrSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_DIL_of b₁ holds
b₂ " is_DIL_of b₁

proof end;

theorem Th39: :: TRANSGEO:39

for b₁ being CongrSpace
for b₂, b₃ being Permutation of the carrier of b₁ st b₂ is_DIL_of b₁ & b₃ is_DIL_of b₁ holds
b₂ * b₃ is_DIL_of b₁

proof end;

theorem Th40: :: TRANSGEO:40

for b₁ being OAffinSpace holds b₁ is CongrSpace-like

proof end;

definition

let c₁ be OAffinSpace;
let c₂ be Permutation of the carrier of c₁;
attr a₂ is positive_dilatation means :Def6: :: TRANSGEO:def 6
a₂ is_DIL_of a₁;

end;

:: deftheorem Def6 defines positive_dilatation TRANSGEO:def 6 :

notation

let c₁ be OAffinSpace;
let c₂ be Permutation of the carrier of c₁;
synonym c₂ is_CDil for positive_dilatation c₂;

end;

theorem Th41: :: TRANSGEO:41

canceled;

theorem Th42: :: TRANSGEO:42

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of b₁ holds
( b₂ is_CDil iff for b₃, b₄ being Element of b₁ holds b₃,b₄ // b₂ . b₃,b₂ . b₄ )

proof end;

definition

let c₁ be OAffinSpace;
let c₂ be Permutation of the carrier of c₁;
attr a₂ is negative_dilatation means :Def7: :: TRANSGEO:def 7
for b₁, b₂ being Element of a₁ holds b₁,b₂ // a₂ . b₂,a₂ . b₁;

end;

:: deftheorem Def7 defines negative_dilatation TRANSGEO:def 7 :

notation

let c₁ be OAffinSpace;
let c₂ be Permutation of the carrier of c₁;
synonym c₂ is_SDil for negative_dilatation c₂;

end;

theorem Th43: :: TRANSGEO:43

canceled;

theorem Th44: :: TRANSGEO:44

for b₁ being OAffinSpace holds id the carrier of b₁ is_CDil

proof end;

theorem Th45: :: TRANSGEO:45

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_CDil holds
b₂ " is_CDil

proof end;

theorem Th46: :: TRANSGEO:46

for b₁ being OAffinSpace
for b₂, b₃ being Permutation of the carrier of b₁ st b₂ is_CDil & b₃ is_CDil holds
b₂ * b₃ is_CDil

proof end;

theorem Th47: :: TRANSGEO:47

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of b₁ holds
( not b₂ is_SDil or not b₂ is_CDil )

proof end;

theorem Th48: :: TRANSGEO:48

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_SDil holds
b₂ " is_SDil

proof end;

theorem Th49: :: TRANSGEO:49

for b₁ being OAffinSpace
for b₂, b₃ being Permutation of the carrier of b₁ st b₂ is_CDil & b₃ is_SDil holds
( b₂ * b₃ is_SDil & b₃ * b₂ is_SDil )

proof end;

definition

let c₁ be OAffinSpace;
let c₂ be Permutation of the carrier of c₁;
attr a₂ is dilatation means :Def8: :: TRANSGEO:def 8
a₂ is_FormalIz_of lambda the CONGR of a₁;

end;

:: deftheorem Def8 defines dilatation TRANSGEO:def 8 :

notation

let c₁ be OAffinSpace;
let c₂ be Permutation of the carrier of c₁;
synonym c₂ is_Dil for dilatation c₂;

end;

theorem Th50: :: TRANSGEO:50

canceled;

theorem Th51: :: TRANSGEO:51

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of b₁ holds
( b₂ is_Dil iff for b₃, b₄ being Element of b₁ holds b₃,b₄ '||' b₂ . b₃,b₂ . b₄ )

proof end;

theorem Th52: :: TRANSGEO:52

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of b₁ st ( b₂ is_CDil or b₂ is_SDil ) holds
b₂ is_Dil

proof end;

theorem Th53: :: TRANSGEO:53

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_Dil holds
ex b₃ being Permutation of the carrier of (Lambda b₁) st
( b₂ = b₃ & b₃ is_DIL_of Lambda b₁ )

proof end;

theorem Th54: :: TRANSGEO:54

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of (Lambda b₁) st b₂ is_DIL_of Lambda b₁ holds
ex b₃ being Permutation of the carrier of b₁ st
( b₂ = b₃ & b₃ is_Dil )

proof end;

theorem Th55: :: TRANSGEO:55

for b₁ being OAffinSpace holds id the carrier of b₁ is_Dil

proof end;

theorem Th56: :: TRANSGEO:56

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_Dil holds
b₂ " is_Dil

proof end;

theorem Th57: :: TRANSGEO:57

for b₁ being OAffinSpace
for b₂, b₃ being Permutation of the carrier of b₁ st b₂ is_Dil & b₃ is_Dil holds
b₂ * b₃ is_Dil

proof end;

theorem Th58: :: TRANSGEO:58

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_Dil holds
for b₃, b₄, b₅, b₆ being Element of b₁ holds
( b₃,b₄ '||' b₅,b₆ iff b₂ . b₃,b₂ . b₄ '||' b₂ . b₅,b₂ . b₆ )

proof end;

theorem Th59: :: TRANSGEO:59

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_Dil holds
for b₃, b₄, b₅ being Element of b₁ holds
( LIN b₃,b₄,b₅ iff LIN b₂ . b₃,b₂ . b₄,b₂ . b₅ )

proof end;

theorem Th60: :: TRANSGEO:60

for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Permutation of the carrier of b₁ st b₄ is_Dil & LIN b₂,b₄ . b₂,b₃ holds
LIN b₂,b₄ . b₂,b₄ . b₃

proof end;

theorem Th61: :: TRANSGEO:61

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ holds
( not b₂,b₃ '||' b₄,b₅ or b₂,b₄ '||' b₃,b₅ or ex b₆ being Element of b₁ st
( LIN b₂,b₄,b₆ & LIN b₃,b₅,b₆ ) )

proof end;

theorem Th62: :: TRANSGEO:62

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_Dil holds
( ( b₂ = id the carrier of b₁ or for b₃ being Element of b₁ holds b₂ . b₃ <> b₃ ) iff for b₃, b₄ being Element of b₁ holds b₃,b₂ . b₃ '||' b₄,b₂ . b₄ )

proof end;

theorem Th63: :: TRANSGEO:63

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁
for b₅ being Permutation of the carrier of b₁ st b₅ is_Dil & b₅ . b₂ = b₂ & b₅ . b₃ = b₃ & not LIN b₂,b₃,b₄ holds
b₅ . b₄ = b₄

proof end;

theorem Th64: :: TRANSGEO:64

for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Permutation of the carrier of b₁ st b₄ is_Dil & b₄ . b₂ = b₂ & b₄ . b₃ = b₃ & b₂ <> b₃ holds
b₄ = id the carrier of b₁

proof end;

theorem Th65: :: TRANSGEO:65

for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁
for b₄, b₅ being Permutation of the carrier of b₁ st b₄ is_Dil & b₅ is_Dil & b₄ . b₂ = b₅ . b₂ & b₄ . b₃ = b₅ . b₃ & not b₂ = b₃ holds
b₄ = b₅

proof end;

definition

let c₁ be OAffinSpace;
let c₂ be Permutation of the carrier of c₁;
attr a₂ is translation means :Def9: :: TRANSGEO:def 9
( a₂ is_Dil & ( a₂ = id the carrier of a₁ or for b₁ being Element of a₁ holds b₁ <> a₂ . b₁ ) );

end;

:: deftheorem Def9 defines translation TRANSGEO:def 9 :

notation

let c₁ be OAffinSpace;
let c₂ be Permutation of the carrier of c₁;
synonym c₂ is_Tr for translation c₂;

end;

theorem Th66: :: TRANSGEO:66

canceled;

theorem Th67: :: TRANSGEO:67

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_Dil holds
( b₂ is_Tr iff for b₃, b₄ being Element of b₁ holds b₃,b₂ . b₃ '||' b₄,b₂ . b₄ )

proof end;

theorem Th68: :: TRANSGEO:68

canceled;

theorem Th69: :: TRANSGEO:69

for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁
for b₄, b₅ being Permutation of the carrier of b₁ st b₄ is_Tr & b₅ is_Tr & b₄ . b₂ = b₅ . b₂ & not LIN b₂,b₄ . b₂,b₃ holds
b₄ . b₃ = b₅ . b₃

proof end;

theorem Th70: :: TRANSGEO:70

for b₁ being OAffinSpace
for b₂ being Element of b₁
for b₃, b₄ being Permutation of the carrier of b₁ st b₃ is_Tr & b₄ is_Tr & b₃ . b₂ = b₄ . b₂ holds
b₃ = b₄

proof end;

theorem Th71: :: TRANSGEO:71

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_Tr holds
b₂ " is_Tr

proof end;

theorem Th72: :: TRANSGEO:72

for b₁ being OAffinSpace
for b₂, b₃ being Permutation of the carrier of b₁ st b₂ is_Tr & b₃ is_Tr holds
b₂ * b₃ is_Tr

proof end;

Lemma42: for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Permutation of the carrier of b₁ st b₄ is_Tr & not LIN b₂,b₄ . b₂,b₃ holds
( b₂,b₃ // b₄ . b₂,b₄ . b₃ & b₂,b₄ . b₂ // b₃,b₄ . b₃ )

proof end;

Lemma43: for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Permutation of the carrier of b₁ st b₄ is_Tr & b₂ <> b₄ . b₂ & LIN b₂,b₄ . b₂,b₃ holds
b₂,b₄ . b₂ // b₃,b₄ . b₃

proof end;

Lemma44: for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Permutation of the carrier of b₁ st b₄ is_Tr & Mid b₂,b₄ . b₂,b₃ & b₂ <> b₄ . b₂ holds
b₂,b₃ // b₄ . b₂,b₄ . b₃

proof end;

Lemma45: for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Permutation of the carrier of b₁ st b₄ is_Tr & b₂ <> b₄ . b₂ & b₃ <> b₄ . b₂ & Mid b₂,b₃,b₄ . b₂ holds
b₂,b₃ // b₄ . b₂,b₄ . b₃

proof end;

Lemma46: for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Permutation of the carrier of b₁ st b₄ is_Tr & b₂ <> b₄ . b₂ & LIN b₂,b₄ . b₂,b₃ holds
b₂,b₃ // b₄ . b₂,b₄ . b₃

proof end;

theorem Th73: :: TRANSGEO:73

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_Tr holds
b₂ is_CDil

proof end;

theorem Th74: :: TRANSGEO:74

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁
for b₅ being Permutation of the carrier of b₁ st b₅ is_Dil & b₅ . b₂ = b₂ & Mid b₃,b₂,b₅ . b₃ & not LIN b₂,b₃,b₄ holds
Mid b₄,b₂,b₅ . b₄

proof end;

theorem Th75: :: TRANSGEO:75

for b₁ being OAffinSpace
for b₂, b₃, b₄ being Element of b₁
for b₅ being Permutation of the carrier of b₁ st b₅ is_Dil & b₅ . b₂ = b₂ & Mid b₃,b₂,b₅ . b₃ & b₃ <> b₂ holds
Mid b₄,b₂,b₅ . b₄

proof end;

theorem Th76: :: TRANSGEO:76

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆ being Permutation of the carrier of b₁ st b₆ is_Dil & b₆ . b₂ = b₂ & b₃ <> b₂ & Mid b₃,b₂,b₆ . b₃ & not LIN b₂,b₄,b₅ holds
b₄,b₅ // b₆ . b₅,b₆ . b₄

proof end;

theorem Th77: :: TRANSGEO:77

for b₁ being OAffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁
for b₆ being Permutation of the carrier of b₁ st b₆ is_Dil & b₆ . b₂ = b₂ & b₃ <> b₂ & Mid b₃,b₂,b₆ . b₃ & LIN b₂,b₄,b₅ holds
b₄,b₅ // b₆ . b₅,b₆ . b₄

proof end;

theorem Th78: :: TRANSGEO:78

for b₁ being OAffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Permutation of the carrier of b₁ st b₄ is_Dil & b₄ . b₂ = b₂ & b₃ <> b₂ & Mid b₃,b₂,b₄ . b₃ holds
b₄ is_SDil

proof end;

theorem Th79: :: TRANSGEO:79

for b₁ being OAffinSpace
for b₂ being Element of b₁
for b₃ being Permutation of the carrier of b₁ st b₃ is_Dil & b₃ . b₂ = b₂ & ( for b₄ being Element of b₁ holds b₂,b₄ // b₂,b₃ . b₄ ) holds
for b₄, b₅ being Element of b₁ holds b₄,b₅ // b₃ . b₄,b₃ . b₅

proof end;

theorem Th80: :: TRANSGEO:80

for b₁ being OAffinSpace
for b₂ being Permutation of the carrier of b₁ holds
( not b₂ is_Dil or b₂ is_CDil or b₂ is_SDil )

proof end;

theorem Th81: :: TRANSGEO:81

canceled;

theorem Th82: :: TRANSGEO:82

for b₁ being AffinSpace holds b₁ is CongrSpace-like

proof end;

theorem Th83: :: TRANSGEO:83

for b₁ being OAffinSpace holds Lambda b₁ is CongrSpace

proof end;

definition

let c₁ be AffinSpace;
let c₂ be Permutation of the carrier of c₁;
attr a₂ is dilatation means :Def10: :: TRANSGEO:def 10
a₂ is_DIL_of a₁;

end;

:: deftheorem Def10 defines dilatation TRANSGEO:def 10 :

notation

let c₁ be AffinSpace;
let c₂ be Permutation of the carrier of c₁;
synonym c₂ is_Dil for dilatation c₂;

end;

theorem Th84: :: TRANSGEO:84

canceled;

theorem Th85: :: TRANSGEO:85

for b₁ being AffinSpace
for b₂ being Permutation of the carrier of b₁ holds
( b₂ is_Dil iff for b₃, b₄ being Element of b₁ holds b₃,b₄ // b₂ . b₃,b₂ . b₄ )

proof end;

theorem Th86: :: TRANSGEO:86

for b₁ being AffinSpace holds id the carrier of b₁ is_Dil

proof end;

theorem Th87: :: TRANSGEO:87

for b₁ being AffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_Dil holds
b₂ " is_Dil

proof end;

theorem Th88: :: TRANSGEO:88

for b₁ being AffinSpace
for b₂, b₃ being Permutation of the carrier of b₁ st b₂ is_Dil & b₃ is_Dil holds
b₂ * b₃ is_Dil

proof end;

theorem Th89: :: TRANSGEO:89

for b₁ being AffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_Dil holds
for b₃, b₄, b₅, b₆ being Element of b₁ holds
( b₃,b₄ // b₅,b₆ iff b₂ . b₃,b₂ . b₄ // b₂ . b₅,b₂ . b₆ )

proof end;

theorem Th90: :: TRANSGEO:90

for b₁ being AffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_Dil holds
for b₃, b₄, b₅ being Element of b₁ holds
( LIN b₃,b₄,b₅ iff LIN b₂ . b₃,b₂ . b₄,b₂ . b₅ )

proof end;

theorem Th91: :: TRANSGEO:91

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Permutation of the carrier of b₁ st b₄ is_Dil & LIN b₂,b₄ . b₂,b₃ holds
LIN b₂,b₄ . b₂,b₄ . b₃

proof end;

theorem Th92: :: TRANSGEO:92

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅ being Element of b₁ holds
( not b₂,b₃ // b₄,b₅ or b₂,b₄ // b₃,b₅ or ex b₆ being Element of b₁ st
( LIN b₂,b₄,b₆ & LIN b₃,b₅,b₆ ) )

proof end;

theorem Th93: :: TRANSGEO:93

for b₁ being AffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_Dil holds
( ( b₂ = id the carrier of b₁ or for b₃ being Element of b₁ holds b₂ . b₃ <> b₃ ) iff for b₃, b₄ being Element of b₁ holds b₃,b₂ . b₃ // b₄,b₂ . b₄ )

proof end;

theorem Th94: :: TRANSGEO:94

for b₁ being AffinSpace
for b₂, b₃, b₄ being Element of b₁
for b₅ being Permutation of the carrier of b₁ st b₅ is_Dil & b₅ . b₂ = b₂ & b₅ . b₃ = b₃ & not LIN b₂,b₃,b₄ holds
b₅ . b₄ = b₄

proof end;

theorem Th95: :: TRANSGEO:95

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Permutation of the carrier of b₁ st b₄ is_Dil & b₄ . b₂ = b₂ & b₄ . b₃ = b₃ & b₂ <> b₃ holds
b₄ = id the carrier of b₁

proof end;

theorem Th96: :: TRANSGEO:96

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄, b₅ being Permutation of the carrier of b₁ st b₄ is_Dil & b₅ is_Dil & b₄ . b₂ = b₅ . b₂ & b₄ . b₃ = b₅ . b₃ & not b₂ = b₃ holds
b₄ = b₅

proof end;

theorem Th97: :: TRANSGEO:97

for b₁ being AffinSpace
for b₂, b₃, b₄, b₅, b₆ being Element of b₁ st not LIN b₂,b₃,b₄ & b₂,b₃ // b₄,b₅ & b₂,b₃ // b₄,b₆ & b₂,b₄ // b₃,b₅ & b₂,b₄ // b₃,b₆ holds
b₅ = b₆

proof end;

definition

let c₁ be AffinSpace;
let c₂ be Permutation of the carrier of c₁;
attr a₂ is translation means :Def11: :: TRANSGEO:def 11
( a₂ is_Dil & ( a₂ = id the carrier of a₁ or for b₁ being Element of a₁ holds b₁ <> a₂ . b₁ ) );

end;

:: deftheorem Def11 defines translation TRANSGEO:def 11 :

notation

let c₁ be AffinSpace;
let c₂ be Permutation of the carrier of c₁;
synonym c₂ is_Tr for translation c₂;

end;

theorem Th98: :: TRANSGEO:98

canceled;

theorem Th99: :: TRANSGEO:99

for b₁ being AffinSpace holds id the carrier of b₁ is_Tr

proof end;

theorem Th100: :: TRANSGEO:100

for b₁ being AffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_Dil holds
( b₂ is_Tr iff for b₃, b₄ being Element of b₁ holds b₃,b₂ . b₃ // b₄,b₂ . b₄ )

proof end;

theorem Th101: :: TRANSGEO:101

canceled;

theorem Th102: :: TRANSGEO:102

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄, b₅ being Permutation of the carrier of b₁ st b₄ is_Tr & b₅ is_Tr & b₄ . b₂ = b₅ . b₂ & not LIN b₂,b₄ . b₂,b₃ holds
b₄ . b₃ = b₅ . b₃

proof end;

theorem Th103: :: TRANSGEO:103

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃, b₄ being Permutation of the carrier of b₁ st b₃ is_Tr & b₄ is_Tr & b₃ . b₂ = b₄ . b₂ holds
b₃ = b₄

proof end;

theorem Th104: :: TRANSGEO:104

for b₁ being AffinSpace
for b₂ being Permutation of the carrier of b₁ st b₂ is_Tr holds
b₂ " is_Tr

proof end;

theorem Th105: :: TRANSGEO:105

for b₁ being AffinSpace
for b₂, b₃ being Permutation of the carrier of b₁ st b₂ is_Tr & b₃ is_Tr holds
b₂ * b₃ is_Tr

proof end;

definition

let c₁ be AffinSpace;
let c₂ be Permutation of the carrier of c₁;
attr a₂ is collineation means :: TRANSGEO:def 12
a₂ is_automorphism_of the CONGR of a₁;

end;

:: deftheorem Def12 defines collineation TRANSGEO:def 12 :

notation

let c₁ be AffinSpace;
let c₂ be Permutation of the carrier of c₁;
synonym c₂ is_Col for collineation c₂;

end;

theorem Th106: :: TRANSGEO:106

canceled;

theorem Th107: :: TRANSGEO:107

for b₁ being AffinSpace
for b₂ being Permutation of the carrier of b₁ holds
( b₂ is_Col iff for b₃, b₄, b₅, b₆ being Element of b₁ holds
( b₃,b₄ // b₅,b₆ iff b₂ . b₃,b₂ . b₄ // b₂ . b₅,b₂ . b₆ ) )

proof end;

theorem Th108: :: TRANSGEO:108

for b₁ being AffinSpace
for b₂, b₃, b₄ being Element of b₁
for b₅ being Permutation of the carrier of b₁ st b₅ is_Col holds
( LIN b₂,b₃,b₄ iff LIN b₅ . b₂,b₅ . b₃,b₅ . b₄ )

proof end;

theorem Th109: :: TRANSGEO:109

for b₁ being AffinSpace
for b₂, b₃ being Permutation of the carrier of b₁ st b₂ is_Col & b₃ is_Col holds
( b₂ " is_Col & b₂ * b₃ is_Col & id the carrier of b₁ is_Col )

proof end;

theorem Th110: :: TRANSGEO:110

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃ being Permutation of the carrier of b₁
for b₄ being Subset of b₁ st b₂ in b₄ holds
b₃ . b₂ in b₃ .: b₄

proof end;

theorem Th111: :: TRANSGEO:111

for b₁ being AffinSpace
for b₂ being Element of b₁
for b₃ being Permutation of the carrier of b₁
for b₄ being Subset of b₁ holds
( b₂ in b₃ .: b₄ iff ex b₅ being Element of b₁ st
( b₅ in b₄ & b₃ . b₅ = b₂ ) )

proof end;

theorem Th112: :: TRANSGEO:112

for b₁ being AffinSpace
for b₂ being Permutation of the carrier of b₁
for b₃, b₄ being Subset of b₁ st b₂ .: b₃ = b₂ .: b₄ holds
b₃ = b₄

proof end;

theorem Th113: :: TRANSGEO:113

for b₁ being AffinSpace
for b₂, b₃ being Element of b₁
for b₄ being Permutation of the carrier of b₁ st b₄ is_Col holds
b₄ .: (Line b₂,b₃) = Line (b₄ . b₂),(b₄ . b₃)

proof end;

theorem Th114: :: TRANSGEO:114

for b₁ being AffinSpace
for b₂ being Permutation of the carrier of b₁
for b₃ being Subset of b₁ st b₂ is_Col & b₃ is_line holds
b₂ .: b₃ is_line

proof end;

theorem Th115: :: TRANSGEO:115

for b₁ being AffinSpace
for b₂ being Permutation of the carrier of b₁
for b₃, b₄ being Subset of b₁ st b₂ is_Col & b₃ // b₄ holds
b₂ .: b₃ // b₂ .: b₄

proof end;

theorem Th116: :: TRANSGEO:116

for b₁ being AffinPlane
for b₂ being Permutation of the carrier of b₁ st ( for b₃ being Subset of b₁ st b₃ is_line holds
b₂ .: b₃ is_line ) holds
b₂ is_Col

proof end;

theorem Th117: :: TRANSGEO:117

for b₁ being AffinPlane
for b₂ being Subset of b₁
for b₃ being Element of b₁
for b₄ being Permutation of the carrier of b₁ st b₄ is_Col & b₂ is_line & ( for b₅ being Element of b₁ st b₅ in b₂ holds
b₄ . b₅ = b₅ ) & not b₃ in b₂ & b₄ . b₃ = b₃ holds
b₄ = id the carrier of b₁

proof end;