begin
definition
let X be non
empty set ;
let R be
Relation of ;
func lambda R -> Relation of
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 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 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 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 ) ) );
:: deftheorem defines Lambda DIRAF:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
Lm1:
for S being OAffinSpace
for x, y, z, t being Element of st x,y // z,t holds
z,t // x,y
theorem Th5:
for
S being
OAffinSpace for
x,
y,
z,
t being
Element of st
x,
y // z,
t holds
(
y,
x // t,
z &
z,
t // x,
y &
t,
z // y,
x )
theorem Th6:
for
S being
OAffinSpace for
z,
t,
x,
y,
u,
w being
Element of st
z <> t &
x,
y // z,
t &
z,
t // u,
w holds
x,
y // u,
w
theorem Th7:
theorem Th8:
theorem Th9:
:: deftheorem Def3 defines Mid DIRAF:def 3 :
theorem
canceled;
theorem Th11:
theorem Th12:
theorem
theorem
theorem
theorem
theorem Th17:
theorem
theorem
for
S being
OAffinSpace for
x,
y,
z,
t being
Element of 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 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 st
Mid x,
y,
t &
Mid x,
z,
t & not
Mid x,
y,
z holds
Mid x,
z,
y
:: deftheorem Def4 defines '||' DIRAF:def 4 :
theorem
canceled;
theorem
theorem Th24:
theorem Th25:
Lm2:
for S being OAffinSpace
for x, y, z, t, u, w being Element of st x <> y & x,y '||' z,t & x,y '||' u,w holds
z,t '||' u,w
theorem Th26:
theorem Th27:
for
S being
OAffinSpace for
x,
y,
z,
t being
Element of 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 Th28:
for
S being
OAffinSpace for
a,
b,
x,
y,
z,
t being
Element of 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 Th29:
theorem Th30:
theorem Th31:
theorem Th32:
:: deftheorem Def5 defines LIN DIRAF:def 5 :
theorem
canceled;
theorem
theorem
for
S being
OAffinSpace for
a,
b,
c being
Element of 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 st x,y,z is_collinear holds
( x,z,y is_collinear & y,x,z is_collinear )
theorem Th36:
for
S being
OAffinSpace for
x,
y,
z being
Element of 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 Th37:
theorem Th38:
for
S being
OAffinSpace for
x,
y,
z,
t,
u being
Element of 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
theorem
theorem
for
S being
OAffinSpace for
u,
z,
x,
y,
w being
Element of 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 Th42:
theorem
theorem
canceled;
theorem Th45:
for
S being
OAffinSpace for
AS being non
empty AffinStruct st
AS = Lambda S holds
for
a,
b,
c,
d being
Element of
for
a',
b',
c',
d' being
Element of st
a = a' &
b = b' &
c = c' &
d = d' holds
(
a',
b' // c',
d' iff
a,
b '||' c,
d )
theorem Th46:
for
S being
OAffinSpace for
AS being non
empty AffinStruct st
AS = Lambda S holds
( ex
x,
y being
Element of st
x <> y & ( for
x,
y,
z,
t,
u,
w being
Element of 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 holds
x,
y // x,
z & ( for
x,
y,
z being
Element of ex
t being
Element of st
(
x,
z // y,
t &
y <> t ) ) & ( for
x,
y,
z being
Element of ex
t being
Element of st
(
x,
y // z,
t &
x,
z // y,
t ) ) & ( for
x,
y,
z,
t being
Element of st
z,
x // x,
t &
x <> z holds
ex
u being
Element of st
(
y,
x // x,
u &
y,
z // t,
u ) ) )
definition
let IT be non
empty AffinStruct ;
canceled;attr IT is
AffinSpace-like means :
Def7:
( ( for
x,
y,
z,
t,
u,
w being
Element of 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 holds
x,
y // x,
z & ( for
x,
y,
z being
Element of ex
t being
Element of st
(
x,
z // y,
t &
y <> t ) ) & ( for
x,
y,
z being
Element of ex
t being
Element of st
(
x,
y // z,
t &
x,
z // y,
t ) ) & ( for
x,
y,
z,
t being
Element of st
z,
x // x,
t &
x <> z holds
ex
u being
Element of st
(
y,
x // x,
u &
y,
z // t,
u ) ) );
end;
:: deftheorem DIRAF:def 6 :
canceled;
:: deftheorem Def7 defines AffinSpace-like DIRAF:def 7 :
for
IT being non
empty AffinStruct holds
(
IT is
AffinSpace-like iff ( ( for
x,
y,
z,
t,
u,
w being
Element of 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 holds
x,
y // x,
z & ( for
x,
y,
z being
Element of ex
t being
Element of st
(
x,
z // y,
t &
y <> t ) ) & ( for
x,
y,
z being
Element of ex
t being
Element of st
(
x,
y // z,
t &
x,
z // y,
t ) ) & ( for
x,
y,
z,
t being
Element of st
z,
x // x,
t &
x <> z holds
ex
u being
Element of st
(
y,
x // x,
u &
y,
z // t,
u ) ) ) );
theorem
for
AS being
AffinSpace holds
( ex
x,
y being
Element of st
x <> y & ( for
x,
y,
z,
t,
u,
w being
Element of 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 holds
x,
y // x,
z & ( for
x,
y,
z being
Element of ex
t being
Element of st
(
x,
z // y,
t &
y <> t ) ) & ( for
x,
y,
z being
Element of ex
t being
Element of st
(
x,
y // z,
t &
x,
z // y,
t ) ) & ( for
x,
y,
z,
t being
Element of st
z,
x // x,
t &
x <> z holds
ex
u being
Element of st
(
y,
x // x,
u &
y,
z // t,
u ) ) )
by Def7, STRUCT_0:def 10;
theorem Th48:
theorem
for
AS being non
empty AffinStruct holds
( ( ex
x,
y being
Element of st
x <> y & ( for
x,
y,
z,
t,
u,
w being
Element of 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 holds
x,
y // x,
z & ( for
x,
y,
z being
Element of ex
t being
Element of st
(
x,
z // y,
t &
y <> t ) ) & ( for
x,
y,
z being
Element of ex
t being
Element of st
(
x,
y // z,
t &
x,
z // y,
t ) ) & ( for
x,
y,
z,
t being
Element of st
z,
x // x,
t &
x <> z holds
ex
u being
Element of st
(
y,
x // x,
u &
y,
z // t,
u ) ) ) iff
AS is
AffinSpace )
by Def7, STRUCT_0:def 10;
theorem Th50:
theorem Th51:
:: deftheorem Def8 defines 2-dimensional DIRAF:def 8 :
theorem
canceled;
theorem
theorem
for
AS being non
empty AffinStruct holds
(
AS is
AffinPlane iff ( ex
x,
y being
Element of st
x <> y & ( for
x,
y,
z,
t,
u,
w being
Element of 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 holds
x,
y // x,
z & ( for
x,
y,
z being
Element of ex
t being
Element of st
(
x,
z // y,
t &
y <> t ) ) & ( for
x,
y,
z being
Element of ex
t being
Element of st
(
x,
y // z,
t &
x,
z // y,
t ) ) & ( for
x,
y,
z,
t being
Element of st
z,
x // x,
t &
x <> z holds
ex
u being
Element of st
(
y,
x // x,
u &
y,
z // t,
u ) ) & ( for
x,
y,
z,
t being
Element of st not
x,
y // z,
t holds
ex
u being
Element of st
(
x,
y // x,
u &
z,
t // z,
u ) ) ) )
by Def7, Def8, STRUCT_0:def 10;