:: 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-2017 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, SUBSET_1, RELAT_1, ZFMISC_1, ANALOAF, STRUCT_0, PARSP_1, DIRAF, PENCIL_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELSET_1, STRUCT_0, ANALOAF; constructors DOMAIN_1, ANALOAF; registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, ANALOAF; requirements SUBSET, BOOLE; begin reserve x,y for set; reserve X for non empty set; reserve a,b,c,d for Element of X; definition let X; let R be Relation of [:X,X:]; func lambda(R) -> Relation of [:X,X:] means :: 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); end; 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) #); end; registration let S be non empty AffinStruct; cluster Lambda S -> non empty; end; reserve S for OAffinSpace; reserve a,b,c,d,p,q,r,x,y,z,t,u,w for Element of S; theorem :: DIRAF:1 x,y // x,y; theorem :: DIRAF:2 x,y // z,t implies y,x // t,z & z,t // x,y & t,z // y,x; theorem :: DIRAF:3 z<>t & x,y // z,t & z,t // u,w implies x,y // u,w; theorem :: DIRAF:4 x,x // y,z & y,z // x,x; theorem :: DIRAF:5 x,y // z,t & x,y // t,z implies x=y or z=t; theorem :: DIRAF:6 x,y // x,z iff x,y // y,z or x,z // z,y; 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; theorem :: DIRAF:7 x,y // x,z iff Mid x,y,z or Mid x,z,y; theorem :: DIRAF:8 Mid a,b,a implies a=b; theorem :: DIRAF:9 Mid a,b,c implies Mid c,b,a; theorem :: DIRAF:10 Mid x,x,y & Mid x,y,y; theorem :: DIRAF:11 Mid a,b,c & Mid a,c,d implies Mid b,c,d; theorem :: DIRAF:12 b<>c & Mid a,b,c & Mid b,c,d implies Mid a,c,d; theorem :: DIRAF:13 ex z st Mid x,y,z & y<>z; theorem :: DIRAF:14 Mid x,y,z & Mid y,x,z implies x=y; theorem :: DIRAF:15 x<>y & Mid x,y,z & Mid x,y,t implies Mid y,z,t or Mid y,t,z; theorem :: DIRAF:16 x<>y & Mid x,y,z & Mid x,y,t implies Mid x,z,t or Mid x,t,z; theorem :: DIRAF:17 Mid x,y,t & Mid x,z,t implies Mid x,y,z or Mid x,z,y; 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; theorem :: DIRAF:18 a,b '||' c,d iff [[a,b],[c,d]] in lambda(the CONGR of S); theorem :: DIRAF:19 x,y '||' y,x & x,y '||' x,y; theorem :: DIRAF:20 x,y '||' z,z & z,z '||' x,y; theorem :: DIRAF:21 x,y '||' x,z implies y,x '||' y,z; theorem :: DIRAF:22 x,y '||' z,t implies 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 :: DIRAF:23 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 ) implies x,y '||' z,t; theorem :: DIRAF:24 ex x,y,z st not x,y '||' x,z; theorem :: DIRAF:25 ex t st x,z '||' y,t & y<>t; theorem :: DIRAF:26 ex t st x,y '||' z,t & x,z '||' y,t; theorem :: DIRAF:27 z,x '||' x,t & x<>z implies ex u st y,x '||' x,u & y,z '||' t,u; 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; theorem :: DIRAF:28 Mid a,b,c implies a,b,c are_collinear; theorem :: DIRAF:29 a,b,c are_collinear implies Mid a,b,c or Mid b,a,c or Mid a,c,b; theorem :: DIRAF:30 x,y,z are_collinear implies 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; theorem :: DIRAF:31 x,x,y are_collinear & x,y,y are_collinear & x,y,x are_collinear; theorem :: DIRAF:32 x<>y & x,y,z are_collinear & x,y,t are_collinear & x,y,u are_collinear implies z,t,u are_collinear; theorem :: DIRAF:33 x<>y & x,y,z are_collinear & x,y '||' z,t implies x,y,t are_collinear; theorem :: DIRAF:34 x,y,z are_collinear & x,y,t are_collinear implies x,y '||' z,t; theorem :: DIRAF:35 u<>z & x,y,u are_collinear & x,y,z are_collinear & u,z,w are_collinear implies x,y,w are_collinear; theorem :: DIRAF:36 ex x,y,z st not x,y,z are_collinear; theorem :: DIRAF:37 x<>y implies ex z st not x,y,z are_collinear; reserve AS for non empty AffinStruct; theorem :: DIRAF:38 AS=Lambda(S) implies for a,b,c,d being Element of S, 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 :: DIRAF:39 AS = Lambda(S) implies (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)) & ( ex x,y,z being Element of AS st not 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 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 :: 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)) & (ex x,y,z being Element of IT st not 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 ex u being Element of IT st y,x // x,u & y,z // t,u; end; registration cluster strict AffinSpace-like for non trivial AffinStruct; end; definition mode AffinSpace is AffinSpace-like non trivial 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)) & (ex x,y,z being Element of AS st not 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 ex u being Element of AS st y,x // x,u & y,z // t,u; theorem :: DIRAF:41 Lambda(S) is AffinSpace; theorem :: DIRAF:42 (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)) & (ex x,y,z being Element of AS st not 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 ex u being Element of AS st y,x // x,u & y,z // t,u) iff AS is AffinSpace; reserve S for OAffinPlane; reserve x,y,z,t,u for Element of S; theorem :: DIRAF:43 not x,y '||' z,t implies ex u st x,y '||' x,u & z,t '||' z,u; theorem :: DIRAF:44 AS = Lambda(S) implies for x,y,z,t being Element of AS st not x, y // z,t ex u being Element of AS st x,y // x,u & z,t // z,u; definition let IT be non empty AffinStruct; attr IT is 2-dimensional means :: DIRAF:def 7 for x,y,z,t being Element of IT st not x,y // z,t ex u being Element of IT st x,y // x,u & z,t // z,u; end; registration cluster strict 2-dimensional for AffinSpace; end; definition mode AffinPlane is 2-dimensional AffinSpace; end; theorem :: DIRAF:45 Lambda(S) is AffinPlane; theorem :: DIRAF:46 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)) & (ex x,y,z being Element of AS st not 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 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 ex u being Element of AS st x ,y // x,u & z,t // z,u;