:: Parallelity Spaces :: by Eugeniusz Kusak, Wojciech Leo\'nczuk and Micha{\l} Muzalewski :: :: Received November 23, 1989 :: Copyright (c) 1990-2021 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 VECTSP_1, SUBSET_1, RLVECT_1, ALGSTR_0, XBOOLE_0, ARYTM_1, ARYTM_3, RELAT_1, SUPINF_2, ZFMISC_1, STRUCT_0, BINOP_1, FUNCT_1, TARSKI, PARSP_1, RECDEF_2, ANALOAF; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, DOMAIN_1, FUNCT_2, BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, RELSET_1; constructors BINOP_1, DOMAIN_1, VECTSP_1, RLVECT_1, RELSET_1, ZFMISC_1, GROUP_1; registrations XBOOLE_0, SUBSET_1, STRUCT_0, VECTSP_1, XTUPLE_0, MCART_1; requirements SUBSET, BOOLE; begin reserve F for Field, a,b,c,d,e,f,g,h for Element of F; :: :: 1. A THREE-DIMENSION CARTESIAN GROUP :: reserve x,y for Element of [:the carrier of F,the carrier of F,the carrier of F:]; definition let F; func c3add(F) -> BinOp of [:the carrier of F,the carrier of F,the carrier of F:] means :: PARSP_1:def 1 it.(x,y) = [x`1_3+y`1_3,x`2_3+y`2_3,x`3_3+y`3_3]; end; definition let F,x,y; func x+y -> Element of [:the carrier of F,the carrier of F,the carrier of F :] equals :: PARSP_1:def 2 (c3add(F)).(x,y); end; theorem :: PARSP_1:1 x+y = [x`1_3+y`1_3,x`2_3+y`2_3,x`3_3+y`3_3]; theorem :: PARSP_1:2 [a,b,c]+[f,g,h]=[a+f,b+g,c+h]; definition let F; func c3compl(F) -> UnOp of [:the carrier of F,the carrier of F,the carrier of F:] means :: PARSP_1:def 3 it.(x) = [-x`1_3,-x`2_3,-x`3_3]; end; definition let F,x; func -x -> Element of [:the carrier of F,the carrier of F,the carrier of F:] equals :: PARSP_1:def 4 (c3compl(F)).(x); end; theorem :: PARSP_1:3 -x = [-x`1_3,-x`2_3,-x`3_3]; :: :: 2. PARALLELITY STRUCTURE :: definition ::$CD struct(1-sorted) ParStr (# carrier -> set, CONGR -> Relation of [:the carrier, the carrier :] #); end; registration cluster non empty for ParStr; end; reserve F for Field; reserve PS for non empty ParStr; definition let PS; let a,b,c,d be Element of PS; pred a,b '||' c,d means :: PARSP_1:def 6 [[a,b],[c,d]] in the CONGR of PS; end; definition let F; func C_3(F) -> set equals :: PARSP_1:def 7 [:the carrier of F,the carrier of F,the carrier of F:]; end; registration let F; cluster C_3(F) -> non empty; end; definition let F; func 4C_3(F) -> set equals :: PARSP_1:def 8 [:[:C_3(F),C_3(F):],[:C_3(F),C_3(F):]:]; end; registration let F; cluster 4C_3(F) -> non empty; end; reserve x for set, a,b,c,d,e,f,g,h,i,j,k,l for Element of [:the carrier of F, the carrier of F,the carrier of F:]; definition let F; func PRs(F) -> set means :: PARSP_1:def 9 for x being object holds x in it iff x in 4C_3(F) & ex a,b,c,d st x =[[a,b],[c,d]] & (a`1_3-b`1_3)*(c`2_3-d`2_3) - (c`1_3-d`1_3)*(a`2_3-b`2_3) = 0.F & (a`1_3-b`1_3)*(c`3_3-d`3_3) - (c`1_3-d`1_3)*(a`3_3-b`3_3) = 0.F & (a`2_3-b`2_3)*(c`3_3-d`3_3) - (c`2_3-d`2_3)*(a`3_3-b`3_3) = 0.F; end; theorem :: PARSP_1:4 PRs(F) c= [:[:C_3(F),C_3(F):],[:C_3(F),C_3(F):]:]; definition let F; func PR(F) -> Relation of [:C_3 F,C_3 F:] equals :: PARSP_1:def 10 PRs(F); end; definition let F; func MPS(F) -> ParStr equals :: PARSP_1:def 11 ParStr (# C_3(F),PR(F) #); end; registration let F; cluster MPS(F) -> strict non empty; end; theorem :: PARSP_1:5 the carrier of MPS(F) = C_3(F); theorem :: PARSP_1:6 the CONGR of MPS(F) = PR(F); reserve a,b,c,d,p,q,r,s for Element of MPS(F); theorem :: PARSP_1:7 a,b '||' c,d iff [[a,b],[c,d]] in PR(F); theorem :: PARSP_1:8 [[a,b],[c,d]] in PR(F) iff ([[a,b],[c,d]] in 4C_3(F) & ex e,f,g,h st [[a,b],[c,d]] = [[e,f],[g,h]] & (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F & (e`1_3-f`1_3)*(g`3_3-h`3_3) - (g`1_3-h`1_3)*(e`3_3-f`3_3) = 0.F & (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F); theorem :: PARSP_1:9 a,b '||' c,d iff ([[a,b],[c,d]] in 4C_3(F) & ex e,f,g,h st [[a,b],[c,d]] = [[e,f],[g,h]] & (e`1_3-f`1_3)*(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F & (e`1_3-f`1_3)*(g`3_3- h`3_3) - (g`1_3-h`1_3)*(e`3_3-f`3_3) = 0.F & (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F); theorem :: PARSP_1:10 the carrier of MPS(F) = [:the carrier of F,the carrier of F,the carrier of F:]; theorem :: PARSP_1:11 [[a,b],[c,d]] in 4C_3(F); theorem :: PARSP_1:12 a,b '||' c,d iff ex e,f,g,h st [[a,b],[c,d]] = [[e,f],[g,h]] & (e`1_3-f`1_3) *(g`2_3-h`2_3) - (g`1_3-h`1_3)*(e`2_3-f`2_3) = 0.F & (e`1_3-f`1_3)*(g`3_3-h`3_3) - (g`1_3-h`1_3)*(e`3_3-f `3_3) = 0.F & (e`2_3-f`2_3)*(g`3_3-h`3_3) - (g`2_3-h`2_3)*(e`3_3-f`3_3) = 0.F ; theorem :: PARSP_1:13 a,b '||' b,a; theorem :: PARSP_1:14 a,b '||' c,c; theorem :: PARSP_1:15 a,b '||' p,q & a,b '||' r,s implies p,q '||' r,s or a=b; theorem :: PARSP_1:16 a,b '||' a,c implies b,a '||' b,c; theorem :: PARSP_1:17 ex d st a,b '||' c,d & a,c '||' b,d; :: :: 3. DEFINITION OF PARALLELITY SPACE :: definition let IT be non empty ParStr; attr IT is ParSp-like means :: PARSP_1:def 12 for a,b,c,d,p,q,r,s being Element of IT holds a,b '||' b,a & a,b '||' c,c & (a,b '||' p,q & a,b '||' r,s implies p,q '||' r,s or a=b) & (a,b '||' a,c implies b,a '||' b,c) & ex x being Element of IT st a,b '||' c,x & a,c '||' b,x; end; registration cluster strict ParSp-like for non empty ParStr; end; definition mode ParSp is ParSp-like non empty ParStr; end; reserve PS for ParSp, a,b,c,d,p,q,r,s for Element of PS; theorem :: PARSP_1:18 a,b '||' a,b; theorem :: PARSP_1:19 a,b '||' c,d implies c,d '||' a,b; theorem :: PARSP_1:20 a,a '||' b,c; theorem :: PARSP_1:21 a,b '||' c,d implies b,a '||' c,d; theorem :: PARSP_1:22 a,b '||' c,d implies a,b '||' d,c; theorem :: PARSP_1:23 a,b '||' c,d implies b,a '||' c,d & a,b '||' d,c & b,a '||' d,c & c,d '||' a,b & d,c '||' a,b & c,d '||' b,a & d,c '||' b,a; theorem :: PARSP_1:24 a,b '||' a,c implies a,c '||' a,b & b,a '||' a,c & a,b '||' c,a & a,c '||' b,a & b,a '||' c,a & c,a '||' a,b & c,a '||' b,a & b,a '||' b,c & a, b '||' b,c & b,a '||' c,b & b,c '||' b,a & a,b '||' c,b & c,b '||' b,a & b,c '||' a,b & c,b '||' a,b & c,a '||' c,b & a,c '||' c,b & c,a '||' b,c & a,c '||' b,c & c,b '||' c,a & b,c '||' c,a & c,b '||' a,c & b,c '||' a,c; theorem :: PARSP_1:25 a=b or c = d or a=c & b=d or a=d & b=c implies a,b '||' c,d; theorem :: PARSP_1:26 a<>b & p,q '||' a,b & a,b '||' r,s implies p,q '||' r,s; theorem :: PARSP_1:27 not a,b '||' a,c implies a<>b & b<>c & c <>a; theorem :: PARSP_1:28 not a,b '||' c,d implies a<>b & c <>d; theorem :: PARSP_1:29 not a,b '||' a,c implies not a,c '||' a,b & not b,a '||' a,c & not a,b '||' c,a & not a,c '||' b,a & not b,a '||' c,a & not c,a '||' a,b & not c,a '||' b,a & not b,a '||' b,c & not a,b '||' b,c & not b,a '||' c,b & not b,c '||' b,a & not b,a '||' c,b & not c,b '||' b,a & not b,c '||' a,b & not c,b '||' a,b & not c,a '||' c,b & not a,c '||' c,b & not c,a '||' b,c & not a,c '||' b,c & not c,b '||' c,a & not b,c '||' c,a & not c,b '||' a,c & not b,c '||' a,c; theorem :: PARSP_1:30 not a,b '||' c,d & a,b '||' p,q & c,d '||' r,s & p<>q & r<>s implies not p,q '||' r,s; theorem :: PARSP_1:31 not a,b '||' a,c & a,b '||' p,q & a,c '||' p,r & b,c '||' q,r & p<>q implies not p,q '||' p,r; theorem :: PARSP_1:32 not a,b '||' a,c & a,c '||' p,r & b,c '||' p,r implies p=r; theorem :: PARSP_1:33 not p,q '||' p,r & p,r '||' p,s & q,r '||' q,s implies r=s; theorem :: PARSP_1:34 not a,b '||' a,c & a,b '||' p,q & a,c '||' p,r & a,c '||' p,s & b,c '||' q,r & b,c '||' q,s implies r=s; theorem :: PARSP_1:35 a,b '||' a,c & a,b '||' a,d implies a,b '||' c,d; theorem :: PARSP_1:36 (for a,b holds a=b) implies for p,q,r,s holds p,q '||' r,s; theorem :: PARSP_1:37 (ex a,b st a<>b & for c holds a,b '||' a,c) implies for p,q,r,s holds p,q '||' r,s; theorem :: PARSP_1:38 not a,b '||' a,c & p<>q implies not p,q '||' p,a or not p,q '||' p,b or not p,q '||' p,c;