:: Ordered Affine Spaces Defined in Terms of Directed Parallelity - part I
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Copyright (c) 1990-2021 Association of Mizar Users

definition
let X be non empty set ;
let R be Relation of [:X,X:];
func lambda R -> Relation of [:X,X:] means :Def1: :: DIRAF:def 1
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 ) )
proof end;
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
proof end;
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 ) ) );

definition
let S be non empty AffinStruct ;
func Lambda S -> strict AffinStruct equals :: DIRAF:def 2
AffinStruct(# the carrier of S,(lambda the CONGR of S) #);
correctness
coherence
AffinStruct(# the carrier of S,(lambda the CONGR of S) #) is strict AffinStruct
;
;
end;

:: deftheorem defines Lambda DIRAF:def 2 :
for S being non empty AffinStruct holds Lambda S = AffinStruct(# the carrier of S,(lambda the CONGR of S) #);

registration
let S be non empty AffinStruct ;
cluster Lambda S -> non empty strict ;
coherence
not Lambda S is empty
;
end;

theorem Th1: :: DIRAF:1
for S being OAffinSpace
for x, y being Element of S holds x,y // x,y
proof end;

Lm1: for S being OAffinSpace
for x, y, z, t being Element of S st x,y // z,t holds
z,t // x,y

proof end;

theorem Th2: :: DIRAF:2
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 )
proof end;

theorem Th3: :: DIRAF:3
for S being OAffinSpace
for x, y, z, t, u, w being Element of S st z <> t & x,y // z,t & z,t // u,w holds
x,y // u,w
proof end;

theorem Th4: :: DIRAF:4
for S being OAffinSpace
for x, y, z being Element of S holds
( x,x // y,z & y,z // x,x )
proof end;

theorem Th5: :: DIRAF:5
for S being OAffinSpace
for x, y, z, t being Element of S st x,y // z,t & x,y // t,z & not x = y holds
z = t
proof end;

theorem Th6: :: DIRAF:6
for S being OAffinSpace
for x, y, z being Element of S holds
( x,y // x,z iff ( x,y // y,z or x,z // z,y ) )
proof end;

definition
let S be non empty AffinStruct ;
let a, b, c be Element of S;
pred Mid a,b,c means :: DIRAF:def 3
a,b // b,c;
end;

:: deftheorem defines Mid DIRAF:def 3 :
for S being non empty AffinStruct
for a, b, c being Element of S holds
( Mid a,b,c iff a,b // b,c );

theorem Th7: :: DIRAF:7
for S being OAffinSpace
for x, y, z being Element of S holds
( x,y // x,z iff ( Mid x,y,z or Mid x,z,y ) ) by Th6;

theorem Th8: :: DIRAF:8
for S being OAffinSpace
for a, b being Element of S st Mid a,b,a holds
a = b by ANALOAF:def 5;

theorem :: DIRAF:9
for S being OAffinSpace
for a, b, c being Element of S st Mid a,b,c holds
Mid c,b,a by Th2;

theorem :: DIRAF:10
for S being OAffinSpace
for x, y being Element of S holds
( Mid x,x,y & Mid x,y,y ) by Th4;

theorem :: DIRAF:11
for S being OAffinSpace
for a, b, c, d being Element of S st Mid a,b,c & Mid a,c,d holds
Mid b,c,d
proof end;

theorem :: DIRAF:12
for S being OAffinSpace
for a, b, c, d being Element of S st b <> c & Mid a,b,c & Mid b,c,d holds
Mid a,c,d
proof end;

theorem Th13: :: DIRAF:13
for S being OAffinSpace
for x, y being Element of S ex z being Element of S st
( Mid x,y,z & y <> z )
proof end;

theorem :: DIRAF:14
for S being OAffinSpace
for x, y, z being Element of S st Mid x,y,z & Mid y,x,z holds
x = y
proof end;

theorem :: DIRAF:15
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
proof end;

theorem :: DIRAF:16
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
proof end;

theorem :: DIRAF:17
for S being OAffinSpace
for x, y, z, t being Element of S st Mid x,y,t & Mid x,z,t & not Mid x,y,z holds
Mid x,z,y
proof end;

definition
let S be non empty AffinStruct ;
let a, b, c, d be Element of S;
pred a,b '||' c,d means :: DIRAF:def 4
( a,b // c,d or a,b // d,c );
end;

:: deftheorem defines '||' DIRAF:def 4 :
for S being non empty AffinStruct
for a, b, c, d being Element of S holds
( a,b '||' c,d iff ( a,b // c,d or a,b // d,c ) );

theorem :: DIRAF:18
for S being OAffinSpace
for a, b, c, d being Element of S holds
( a,b '||' c,d iff [[a,b],[c,d]] in lambda the CONGR of S )
proof end;

theorem Th19: :: DIRAF:19
for S being OAffinSpace
for x, y being Element of S holds
( x,y '||' y,x & x,y '||' x,y ) by Th1;

theorem Th20: :: DIRAF:20
for S being OAffinSpace
for x, y, z being Element of S holds
( x,y '||' z,z & z,z '||' x,y ) by Th4;

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

proof end;

theorem Th21: :: DIRAF:21
for S being OAffinSpace
for x, y, z being Element of S st x,y '||' x,z holds
y,x '||' y,z
proof end;

theorem Th22: :: DIRAF:22
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 ) by Th2;

theorem Th23: :: DIRAF:23
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
proof end;

theorem Th24: :: DIRAF:24
for S being OAffinSpace holds
not for x, y, z being Element of S holds x,y '||' x,z
proof end;

theorem Th25: :: DIRAF:25
for S being OAffinSpace
for x, y, z being Element of S ex t being Element of S st
( x,z '||' y,t & y <> t )
proof end;

theorem Th26: :: DIRAF:26
for S being OAffinSpace
for x, y, z being Element of S ex t being Element of S st
( x,y '||' z,t & x,z '||' y,t )
proof end;

theorem Th27: :: DIRAF:27
for S being OAffinSpace
for x, y, z, t being Element of S st z,x '||' x,t & x <> z holds
ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
proof end;

definition
let S be non empty AffinStruct ;
let a, b, c be Element of S;
pred a,b,c are_collinear means :: DIRAF:def 5
a,b '||' a,c;
end;

:: deftheorem defines are_collinear DIRAF:def 5 :
for S being non empty AffinStruct
for a, b, c being Element of S holds
( a,b,c are_collinear iff a,b '||' a,c );

theorem :: DIRAF:28
for S being OAffinSpace
for a, b, c being Element of S st Mid a,b,c holds
a,b,c are_collinear
proof end;

theorem :: DIRAF:29
for S being OAffinSpace
for a, b, c being Element of S holds
( not a,b,c are_collinear or Mid a,b,c or Mid b,a,c or Mid a,c,b )
proof end;

Lm3: for S being OAffinSpace
for x, y, z being Element of S st x,y,z are_collinear holds
( x,z,y are_collinear & y,x,z are_collinear )

by ;

theorem Th30: :: DIRAF:30
for S being OAffinSpace
for x, y, z being Element of S st x,y,z are_collinear holds
( x,z,y are_collinear & y,x,z are_collinear & y,z,x are_collinear & z,x,y are_collinear & z,y,x are_collinear )
proof end;

theorem Th31: :: DIRAF:31
for S being OAffinSpace
for x, y being Element of S holds
( x,x,y are_collinear & x,y,y are_collinear & x,y,x are_collinear ) by ;

theorem Th32: :: DIRAF:32
for S being OAffinSpace
for x, y, z, t, u being Element of S st x <> y & x,y,z are_collinear & x,y,t are_collinear & x,y,u are_collinear holds
z,t,u are_collinear
proof end;

theorem :: DIRAF:33
for S being OAffinSpace
for x, y, z, t being Element of S st x <> y & x,y,z are_collinear & x,y '||' z,t holds
x,y,t are_collinear
proof end;

theorem :: DIRAF:34
for S being OAffinSpace
for x, y, z, t being Element of S st x,y,z are_collinear & x,y,t are_collinear holds
x,y '||' z,t
proof end;

theorem :: DIRAF:35
for S being OAffinSpace
for x, y, z, u, w being Element of S st u <> z & x,y,u are_collinear & x,y,z are_collinear & u,z,w are_collinear holds
x,y,w are_collinear
proof end;

theorem Th36: :: DIRAF:36
for S being OAffinSpace holds
not for x, y, z being Element of S holds x,y,z are_collinear
proof end;

theorem :: DIRAF:37
for S being OAffinSpace
for x, y being Element of S st x <> y holds
ex z being Element of S st not x,y,z are_collinear
proof end;

theorem Th38: :: DIRAF:38
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 )
proof end;

theorem Th39: :: DIRAF:39
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 ) ) )
proof end;

definition
let IT be non empty AffinStruct ;
attr IT is AffinSpace-like means :Def6: :: DIRAF:def 6
( ( 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 ) ) ) );

registration
existence
ex b1 being non trivial AffinStruct st
( b1 is strict & b1 is AffinSpace-like )
proof end;
end;

definition end;

theorem :: DIRAF:40
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 ;

theorem Th41: :: DIRAF:41
for S being OAffinSpace holds Lambda S is AffinSpace
proof end;

theorem :: DIRAF:42
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 ;

theorem Th43: :: DIRAF:43
for S being OAffinPlane
for x, y, z, t being Element of S st not x,y '||' z,t holds
ex u being Element of S st
( x,y '||' x,u & z,t '||' z,u )
proof end;

theorem Th44: :: DIRAF:44
for AS being non empty AffinStruct
for S being OAffinPlane st AS = Lambda S holds
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 )
proof end;

definition
let IT be non empty AffinStruct ;
attr IT is 2-dimensional means :Def7: :: DIRAF:def 7
for x, y, z, t being Element of IT st not x,y // z,t holds
ex u being Element of IT st
( x,y // x,u & z,t // z,u );
end;

:: deftheorem Def7 defines 2-dimensional DIRAF:def 7 :
for IT being non empty AffinStruct holds
( IT is 2-dimensional iff for x, y, z, t being Element of IT st not x,y // z,t holds
ex u being Element of IT st
( x,y // x,u & z,t // z,u ) );

registration
existence
ex b1 being AffinSpace st
( b1 is strict & b1 is 2-dimensional )
proof end;
end;

definition end;

theorem :: DIRAF:45
for S being OAffinPlane holds Lambda S is AffinPlane
proof end;

theorem :: DIRAF:46
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 ;