:: Ordered Affine Spaces Defined in Terms of Directed Parallelity - part I
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received May 4, 1990
:: 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 b₁ being Relation of [:X,X:] st
for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in b₁ iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) )

proof end;

uniqueness
for b₁, b₂ being Relation of [:X,X:] st ( for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in b₁ 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 b₂ iff ( [[a,b],[c,d]] in R or [[a,b],[d,c]] in R ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines lambda DIRAF:def 1 :
for X being non empty set
for R, b₃ being Relation of [:X,X:] holds
( b₃ = lambda R iff for a, b, c, d being Element of X holds
( [[a,b],[c,d]] in b₃ 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 Th21, Th22;

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 Th19, Th20;

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

cluster non empty non trivial strict AffinSpace-like for AffinStruct ;

existence
ex b₁ being non trivial AffinStruct st
( b₁ is strict & b₁ is AffinSpace-like )

proof end;

end;

definition

mode AffinSpace is non trivial AffinSpace-like AffinStruct ;

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 Def6, STRUCT_0:def 10;

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 Def6, STRUCT_0:def 10;

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

cluster non empty non trivial strict AffinSpace-like 2-dimensional for AffinStruct ;

existence
ex b₁ being AffinSpace st
( b₁ is strict & b₁ is 2-dimensional )

proof end;

end;

definition

mode AffinPlane is 2-dimensional AffinSpace;

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 Def6, Def7, STRUCT_0:def 10;