begin
theorem
canceled;
theorem Th2:
theorem
canceled;
theorem Th4:
:: 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
EXPermutation{
F1()
-> non
empty set ,
P1[
set ,
set ] } :
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
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
Lm1:
for A being non empty set
for f, g, h being Permutation of A st f * g = f * h holds
g = h
Lm2:
for A being non empty set
for g, f, h being Permutation of A st g * f = h * f holds
g = h
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
:: 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
canceled;
theorem Th23:
theorem Th24:
theorem
theorem Th26:
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
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:
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
canceled;
theorem Th28:
theorem Th29:
theorem Th30:
theorem
theorem
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
theorem
:: 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
canceled;
theorem Th35:
definition
let IT be non
empty AffinStruct ;
attr IT is
CongrSpace-like means :
Def5:
( ( 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 :
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 ) ) );
Lm3:
for CS being CongrSpace holds the CONGR of CS is_reflexive_in [: the carrier of CS, the carrier of CS:]
Lm4:
for CS being CongrSpace holds the CONGR of CS is_symmetric_in [: the carrier of CS, the carrier of CS:]
theorem
canceled;
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
:: 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
canceled;
theorem Th42:
:: 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
canceled;
theorem Th44:
theorem
theorem
theorem
theorem
theorem
:: 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
canceled;
theorem Th51:
theorem
theorem
theorem
theorem
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
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 ) )
theorem Th62:
theorem Th63:
theorem Th64:
theorem
:: 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 & ( f = id the carrier of OAS or for a being Element of OAS holds a <> f . a ) ) );
theorem
canceled;
theorem Th67:
theorem
canceled;
theorem Th69:
theorem Th70:
theorem Th71:
theorem
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 LIN a,f . a,b holds
( a,b // f . a,f . b & a,f . a // b,f . b )
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 & LIN a,f . a,b holds
a,f . a // b,f . b
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
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
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 & LIN a,f . a,b holds
a,b // f . a,f . b
theorem Th73:
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem
theorem
canceled;
theorem Th82:
theorem
:: 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
canceled;
theorem Th85:
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
theorem
theorem Th91:
theorem Th92:
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 ) )
theorem Th93:
theorem Th94:
theorem Th95:
theorem
theorem Th97:
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
:: 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 & ( f = id the carrier of AFS or for a being Element of AFS holds a <> f . a ) ) );
theorem
canceled;
theorem
theorem Th100:
theorem
canceled;
theorem Th102:
theorem Th103:
theorem Th104:
theorem
:: 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
canceled;
theorem Th107:
theorem Th108:
theorem
theorem Th110:
theorem Th111:
theorem Th112:
theorem Th113:
theorem
theorem Th115:
theorem
theorem