:: 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-2012 Association of Mizar Users begin 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 ) ) proofend; 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 proofend; 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 proofend; Lm1: for S being OAffinSpace for x, y, z, t being Element of S st x,y // z,t holds z,t // x,y proofend; 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 ) proofend; theorem Th3: :: DIRAF:3 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 proofend; 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 ) proofend; 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 proofend; 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 ) ) proofend; definition let S be non empty AffinStruct ; let a, b, c be Element of S; pred Mid a,b,c means :Def3: :: DIRAF:def 3 a,b // b,c; end; :: deftheorem Def3 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 ) ) proofend; theorem Th8: :: DIRAF:8 for S being OAffinSpace for a, b being Element of S st Mid a,b,a holds a = b proofend; 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 proofend; theorem :: DIRAF:10 for S being OAffinSpace for x, y being Element of S holds ( Mid x,x,y & Mid x,y,y ) proofend; 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 proofend; theorem :: DIRAF:12 for S being OAffinSpace for b, c, a, d being Element of S st b <> c & Mid a,b,c & Mid b,c,d holds Mid a,c,d proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; theorem :: DIRAF:17 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 proofend; definition let S be non empty AffinStruct ; let a, b, c, d be Element of S; preda,b '||' c,d means :Def4: :: DIRAF:def 4 ( a,b // c,d or a,b // d,c ); end; :: deftheorem Def4 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 ) proofend; theorem Th19: :: DIRAF:19 for S being OAffinSpace for x, y being Element of S holds ( x,y '||' y,x & x,y '||' x,y ) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 proofend; theorem Th24: :: DIRAF:24 for S being OAffinSpace holds not for x, y, z being Element of S holds x,y '||' x,z proofend; theorem Th25: :: DIRAF:25 for S being OAffinSpace for x, z, y being Element of S ex t being Element of S st ( x,z '||' y,t & y <> t ) proofend; 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 ) proofend; theorem Th27: :: DIRAF:27 for S being OAffinSpace for z, x, t, y 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 ) proofend; definition let S be non empty AffinStruct ; let a, b, c be Element of S; pred LIN a,b,c means :Def5: :: DIRAF:def 5 a,b '||' a,c; end; :: deftheorem Def5 defines LIN DIRAF:def_5_:_ for S being non empty AffinStruct for a, b, c being Element of S holds ( LIN a,b,c iff a,b '||' a,c ); notation let S be non empty AffinStruct ; let a, b, c be Element of S; synonym a,b,c is_collinear for LIN a,b,c; end; theorem :: DIRAF:28 for S being OAffinSpace for a, b, c being Element of S st Mid a,b,c holds a,b,c is_collinear proofend; theorem :: DIRAF:29 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 ) proofend; 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 ) proofend; theorem Th30: :: DIRAF:30 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 ) proofend; theorem Th31: :: DIRAF:31 for S being OAffinSpace for x, y being Element of S holds ( x,x,y is_collinear & x,y,y is_collinear & x,y,x is_collinear ) proofend; theorem Th32: :: DIRAF:32 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 proofend; theorem :: DIRAF:33 for S being OAffinSpace for x, y, z, t being Element of S st x <> y & x,y,z is_collinear & x,y '||' z,t holds x,y,t is_collinear proofend; theorem :: DIRAF:34 for S being OAffinSpace for x, y, z, t being Element of S st x,y,z is_collinear & x,y,t is_collinear holds x,y '||' z,t proofend; theorem :: DIRAF:35 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 proofend; theorem Th36: :: DIRAF:36 for S being OAffinSpace holds not for x, y, z being Element of S holds x,y,z is_collinear proofend; 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 is_collinear proofend; 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 ) proofend; 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 ) ) ) proofend; definition let IT be non empty AffinStruct ; attrIT 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 b1 being non trivial AffinStruct st ( b1 is strict & b1 is AffinSpace-like ) proofend; 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 proofend; 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 ) proofend; 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 ) proofend; definition let IT be non empty AffinStruct ; attrIT 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 b1 being AffinSpace st ( b1 is strict & b1 is 2-dimensional ) proofend; end; definition mode AffinPlane is 2-dimensional AffinSpace; end; theorem :: DIRAF:45 for S being OAffinPlane holds Lambda S is AffinPlane proofend; 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;