begin
definition
let X be non
empty set ;
let R be
Relation of
[:X,X:];
func lambda R -> Relation of
[:X,X:] means :
Def1:
for
a,
b,
c,
d being
Element of
X holds
(
[[a,b],[c,d]] in it iff (
[[a,b],[c,d]] in R or
[[a,b],[d,c]] in R ) );
existence
ex b1 being Relation of [:X,X:] st
for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in b1 iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) )
uniqueness
for b1, b2 being Relation of [:X,X:] st ( for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in b1 iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) ) & ( for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in b2 iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) ) holds
b1 = b2
end;
::
deftheorem Def1 defines
lambda DIRAF:def 1 :
for X being non empty set
for R, b3 being Relation of [:X,X:] holds
( b3 = lambda R iff for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in b3 iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) );
Lm1:
for S being OAffinSpace
for x, y, z, t being Element of S st x,y // z,t holds
z,t // x,y
theorem Th2:
for
S being
OAffinSpace for
x,
y,
z,
t being
Element of
S st
x,
y // z,
t holds
(
y,
x // t,
z &
z,
t // x,
y &
t,
z // y,
x )
theorem Th3:
for
S being
OAffinSpace for
z,
t,
x,
y,
u,
w being
Element of
S st
z <> t &
x,
y // z,
t &
z,
t // u,
w holds
x,
y // u,
w
theorem
for
S being
OAffinSpace for
x,
y,
z,
t being
Element of
S st
x <> y &
Mid x,
y,
z &
Mid x,
y,
t & not
Mid y,
z,
t holds
Mid y,
t,
z
theorem
for
S being
OAffinSpace for
x,
y,
z,
t being
Element of
S st
x <> y &
Mid x,
y,
z &
Mid x,
y,
t & not
Mid x,
z,
t holds
Mid x,
t,
z
theorem
for
S being
OAffinSpace for
x,
y,
t,
z being
Element of
S st
Mid x,
y,
t &
Mid x,
z,
t & not
Mid x,
y,
z holds
Mid x,
z,
y
Lm2:
for S being OAffinSpace
for x, y, z, t, u, w being Element of S st x <> y & x,y '||' z,t & x,y '||' u,w holds
z,t '||' u,w
theorem Th22:
for
S being
OAffinSpace for
x,
y,
z,
t being
Element of
S st
x,
y '||' z,
t holds
(
x,
y '||' t,
z &
y,
x '||' z,
t &
y,
x '||' t,
z &
z,
t '||' x,
y &
z,
t '||' y,
x &
t,
z '||' x,
y &
t,
z '||' y,
x )
theorem Th23:
for
S being
OAffinSpace for
a,
b,
x,
y,
z,
t being
Element of
S st
a <> b & ( (
a,
b '||' x,
y &
a,
b '||' z,
t ) or (
a,
b '||' x,
y &
z,
t '||' a,
b ) or (
x,
y '||' a,
b &
z,
t '||' a,
b ) or (
x,
y '||' a,
b &
a,
b '||' z,
t ) ) holds
x,
y '||' z,
t
theorem
for
S being
OAffinSpace for
a,
b,
c being
Element of
S holds
( not
a,
b,
c is_collinear or
Mid a,
b,
c or
Mid b,
a,
c or
Mid a,
c,
b )
Lm3:
for S being OAffinSpace
for x, y, z being Element of S st x,y,z is_collinear holds
( x,z,y is_collinear & y,x,z is_collinear )
theorem Th30:
for
S being
OAffinSpace for
x,
y,
z being
Element of
S st
x,
y,
z is_collinear holds
(
x,
z,
y is_collinear &
y,
x,
z is_collinear &
y,
z,
x is_collinear &
z,
x,
y is_collinear &
z,
y,
x is_collinear )
theorem Th32:
for
S being
OAffinSpace for
x,
y,
z,
t,
u being
Element of
S st
x <> y &
x,
y,
z is_collinear &
x,
y,
t is_collinear &
x,
y,
u is_collinear holds
z,
t,
u is_collinear
theorem
for
S being
OAffinSpace for
u,
z,
x,
y,
w being
Element of
S st
u <> z &
x,
y,
u is_collinear &
x,
y,
z is_collinear &
u,
z,
w is_collinear holds
x,
y,
w is_collinear
theorem Th38:
for
S being
OAffinSpace for
AS being non
empty AffinStruct st
AS = Lambda S holds
for
a,
b,
c,
d being
Element of
S for
a9,
b9,
c9,
d9 being
Element of
AS st
a = a9 &
b = b9 &
c = c9 &
d = d9 holds
(
a9,
b9 // c9,
d9 iff
a,
b '||' c,
d )
theorem Th39:
for
S being
OAffinSpace for
AS being non
empty AffinStruct st
AS = Lambda S holds
( ex
x,
y being
Element of
AS st
x <> y & ( for
x,
y,
z,
t,
u,
w being
Element of
AS holds
(
x,
y // y,
x &
x,
y // z,
z & (
x <> y &
x,
y // z,
t &
x,
y // u,
w implies
z,
t // u,
w ) & (
x,
y // x,
z implies
y,
x // y,
z ) ) ) & not for
x,
y,
z being
Element of
AS holds
x,
y // x,
z & ( for
x,
y,
z being
Element of
AS ex
t being
Element of
AS st
(
x,
z // y,
t &
y <> t ) ) & ( for
x,
y,
z being
Element of
AS ex
t being
Element of
AS st
(
x,
y // z,
t &
x,
z // y,
t ) ) & ( for
x,
y,
z,
t being
Element of
AS st
z,
x // x,
t &
x <> z holds
ex
u being
Element of
AS st
(
y,
x // x,
u &
y,
z // t,
u ) ) )
definition
let IT be non
empty AffinStruct ;
attr IT is
AffinSpace-like means :
Def6:
( ( for
x,
y,
z,
t,
u,
w being
Element of
IT holds
(
x,
y // y,
x &
x,
y // z,
z & (
x <> y &
x,
y // z,
t &
x,
y // u,
w implies
z,
t // u,
w ) & (
x,
y // x,
z implies
y,
x // y,
z ) ) ) & not for
x,
y,
z being
Element of
IT holds
x,
y // x,
z & ( for
x,
y,
z being
Element of
IT ex
t being
Element of
IT st
(
x,
z // y,
t &
y <> t ) ) & ( for
x,
y,
z being
Element of
IT ex
t being
Element of
IT st
(
x,
y // z,
t &
x,
z // y,
t ) ) & ( for
x,
y,
z,
t being
Element of
IT st
z,
x // x,
t &
x <> z holds
ex
u being
Element of
IT st
(
y,
x // x,
u &
y,
z // t,
u ) ) );
end;
::
deftheorem Def6 defines
AffinSpace-like DIRAF:def 6 :
for IT being non empty AffinStruct holds
( IT is AffinSpace-like iff ( ( for x, y, z, t, u, w being Element of IT holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of IT holds x,y // x,z & ( for x, y, z being Element of IT ex t being Element of IT st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of IT ex t being Element of IT st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of IT st z,x // x,t & x <> z holds
ex u being Element of IT st
( y,x // x,u & y,z // t,u ) ) ) );
theorem
for
AS being
AffinSpace holds
( ex
x,
y being
Element of
AS st
x <> y & ( for
x,
y,
z,
t,
u,
w being
Element of
AS holds
(
x,
y // y,
x &
x,
y // z,
z & (
x <> y &
x,
y // z,
t &
x,
y // u,
w implies
z,
t // u,
w ) & (
x,
y // x,
z implies
y,
x // y,
z ) ) ) & not for
x,
y,
z being
Element of
AS holds
x,
y // x,
z & ( for
x,
y,
z being
Element of
AS ex
t being
Element of
AS st
(
x,
z // y,
t &
y <> t ) ) & ( for
x,
y,
z being
Element of
AS ex
t being
Element of
AS st
(
x,
y // z,
t &
x,
z // y,
t ) ) & ( for
x,
y,
z,
t being
Element of
AS st
z,
x // x,
t &
x <> z holds
ex
u being
Element of
AS st
(
y,
x // x,
u &
y,
z // t,
u ) ) )
by Def6, STRUCT_0:def 10;
theorem
for
AS being non
empty AffinStruct holds
( ( ex
x,
y being
Element of
AS st
x <> y & ( for
x,
y,
z,
t,
u,
w being
Element of
AS holds
(
x,
y // y,
x &
x,
y // z,
z & (
x <> y &
x,
y // z,
t &
x,
y // u,
w implies
z,
t // u,
w ) & (
x,
y // x,
z implies
y,
x // y,
z ) ) ) & not for
x,
y,
z being
Element of
AS holds
x,
y // x,
z & ( for
x,
y,
z being
Element of
AS ex
t being
Element of
AS st
(
x,
z // y,
t &
y <> t ) ) & ( for
x,
y,
z being
Element of
AS ex
t being
Element of
AS st
(
x,
y // z,
t &
x,
z // y,
t ) ) & ( for
x,
y,
z,
t being
Element of
AS st
z,
x // x,
t &
x <> z holds
ex
u being
Element of
AS st
(
y,
x // x,
u &
y,
z // t,
u ) ) ) iff
AS is
AffinSpace )
by Def6, STRUCT_0:def 10;
theorem
for
AS being non
empty AffinStruct holds
(
AS is
AffinPlane iff ( ex
x,
y being
Element of
AS st
x <> y & ( for
x,
y,
z,
t,
u,
w being
Element of
AS holds
(
x,
y // y,
x &
x,
y // z,
z & (
x <> y &
x,
y // z,
t &
x,
y // u,
w implies
z,
t // u,
w ) & (
x,
y // x,
z implies
y,
x // y,
z ) ) ) & not for
x,
y,
z being
Element of
AS holds
x,
y // x,
z & ( for
x,
y,
z being
Element of
AS ex
t being
Element of
AS st
(
x,
z // y,
t &
y <> t ) ) & ( for
x,
y,
z being
Element of
AS ex
t being
Element of
AS st
(
x,
y // z,
t &
x,
z // y,
t ) ) & ( for
x,
y,
z,
t being
Element of
AS st
z,
x // x,
t &
x <> z holds
ex
u being
Element of
AS st
(
y,
x // x,
u &
y,
z // t,
u ) ) & ( for
x,
y,
z,
t being
Element of
AS st not
x,
y // z,
t holds
ex
u being
Element of
AS st
(
x,
y // x,
u &
z,
t // z,
u ) ) ) )
by Def6, Def7, STRUCT_0:def 10;