:: Fano-Desargues Parallelity Spaces :: by Eugeniusz Kusak and Wojciech Leo\'nczuk :: :: Received March 23, 1990 :: 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 RLVECT_1, ALGSTR_0, XBOOLE_0, SUBSET_1, ARYTM_1, SUPINF_2, ARYTM_3, VECTSP_1, PARSP_1, ZFMISC_1, STRUCT_0, RELAT_1, GROUP_1, MESFUNC1, PARSP_2, RECDEF_2, PENCIL_1; notations TARSKI, ZFMISC_1, XTUPLE_0, SUBSET_1, MCART_1, DOMAIN_1, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, PARSP_1; constructors DOMAIN_1, PARSP_1, XTUPLE_0; registrations STRUCT_0, VECTSP_1, PARSP_1, XTUPLE_0, MCART_1; begin reserve F for Field; theorem :: PARSP_2:1 MPS(F) is ParSp; reserve a,b,c,d,p,q,r for Element of MPS(F); reserve e,f,g,h,i,j,k,l,m,n,o,w for Element of [:the carrier of F,the carrier of F,the carrier of F:]; reserve K,L,M,N,R,S for Element of F; theorem :: PARSP_2:2 a,b '||' c,d iff ex e,f,g,h st [[a,b],[c,d]] = [[e,f],[g,h]] & ((ex K st K*(e`1_3-f`1_3) = g`1_3-h`1_3 & K*(e`2_3-f`2_3) = g`2_3-h`2_3 & K*(e`3_3-f`3_3) = g`3_3-h`3_3) or e`1_3-f `1_3 = 0.F & e`2_3-f`2_3 = 0.F & e`3_3-f`3_3 = 0.F ); theorem :: PARSP_2:3 not a,b '||' a,c & [[a,b],[a,c]]=[[e,f],[e,g]] implies e<>f & e<>g & f<>g; theorem :: PARSP_2:4 not a,b '||' a,c & [[a,b],[a,c]] = [[e,f],[e,g]] & K*(e`1_3-f`1_3)=L*(e`1_3-g`1_3 ) & K*(e`2_3-f`2_3)=L*(e`2_3-g`2_3) & K*(e`3_3-f`3_3)=L*(e`3_3-g`3_3) implies K=0.F & L=0.F; theorem :: PARSP_2:5 not a,b '||' a,c & a,b '||' c,d & a,c '||' b,d & [[a,b],[c,d]] = [[e,f],[g,h]] implies h`1_3=f`1_3+g`1_3-e`1_3 & h`2_3=f`2_3+g`2_3-e`2_3 & h`3_3=f`3_3+g`3_3-e`3_3; theorem :: PARSP_2:6 ex a,b,c st not a,b '||' a,c; theorem :: PARSP_2:7 1_F+1_F<>0.F & b,c '||' a,d & a,b '||' c,d & a,c '||' b,d implies a,b '||' a,c; theorem :: PARSP_2:8 not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r implies b,c '||' q,r; :: 2. DEFINITION OF A FANO-DESARGUES SPACE definition let IT be ParSp; attr IT is FanodesSp-like means :: PARSP_2:def 1 (ex a,b,c being Element of IT st not a,b '||' a,c) & (for a,b,c,d being Element of IT holds b,c '||' a,d & a,b '||' c,d & a,c '||' b,d implies a,b '||' a,c) & for a,b,c,p,q,r being Element of IT holds not a,p '||' a,b & not a,p '||' a,c & a,p '||' b,q & a,p '||' c,r & a,b '||' p,q & a,c '||' p,r implies b,c '||' q,r; end; registration cluster strict FanodesSp-like for ParSp; end; definition mode FanodesSp is FanodesSp-like ParSp; end; reserve FdSp for FanodesSp; reserve a,b,c,d,p,q,r,s,o,x,y for Element of FdSp; :: 3. AXIOMS OF A FANO-DESARGUES PARALLELITY SPACE theorem :: PARSP_2:9 p<>q implies ex r st not p,q '||' p,r; definition let FdSp,a,b,c; pred a,b,c are_collinear means :: PARSP_2:def 2 a,b '||' a,c; end; theorem :: PARSP_2:10 a,b,c are_collinear implies a,c,b are_collinear & c,b,a are_collinear & b,a,c are_collinear & b,c,a are_collinear & c,a,b are_collinear; theorem :: PARSP_2:11 not a,b,c are_collinear & a,b '||' p,q & a,c '||' p,r & p<>q & p <>r implies not p,q,r are_collinear; theorem :: PARSP_2:12 a=b or b=c or c =a implies a,b,c are_collinear; theorem :: PARSP_2:13 a<>b & a,b,p are_collinear & a,b,q are_collinear & a,b,r are_collinear implies p,q,r are_collinear; theorem :: PARSP_2:14 p<>q implies ex r st not p,q,r are_collinear; theorem :: PARSP_2:15 a,b,c are_collinear & a,b,d are_collinear implies a,b '||' c,d; theorem :: PARSP_2:16 not a,b,c are_collinear & a,b '||' c,d implies not a,b,d are_collinear; theorem :: PARSP_2:17 not a,b,c are_collinear & a,b '||' c,d & c <>d implies not a,b,x are_collinear or not c,d,x are_collinear; theorem :: PARSP_2:18 not o,a,b are_collinear implies not o,a,x are_collinear or not o,b,x are_collinear or o=x; theorem :: PARSP_2:19 o<>a & o<>b & o,a,b are_collinear & o,a,p are_collinear & o,b,q are_collinear implies a,b '||' p,q; theorem :: PARSP_2:20 not a,b '||' c,d & a,b,p are_collinear & a,b,q are_collinear & c,d,p are_collinear & c,d,q are_collinear implies p=q; theorem :: PARSP_2:21 a<>b & a,b,c are_collinear & a,b '||' c,d implies a,c '||' b,d; theorem :: PARSP_2:22 a<>b & a,b,c are_collinear & a,b '||' c,d implies c,b '||' c,d; theorem :: PARSP_2:23 not o,a,c are_collinear & o,a,b are_collinear & o,c,p are_collinear & o,c ,q are_collinear & a,c '||' b,p & a,c '||' b,q implies p=q; theorem :: PARSP_2:24 a<>b & a,b,c are_collinear & a,b,d are_collinear implies a,c,d are_collinear; theorem :: PARSP_2:25 a,b,c are_collinear & a,c,d are_collinear & a<>c implies b,c,d are_collinear; definition let FdSp,a,b,c,d; pred parallelogram a,b,c,d means :: PARSP_2:def 3 not a,b,c are_collinear & a,b '||' c, d & a,c '||' b,d; end; theorem :: PARSP_2:26 parallelogram a,b,c,d implies a<>b & b<>c & c <>a & a<>d & b<>d & c <>d; theorem :: PARSP_2:27 parallelogram a,b,c,d implies not a,b,c are_collinear & not b,a,d are_collinear & not c,d,a are_collinear & not d,c,b are_collinear; theorem :: PARSP_2:28 parallelogram a,b,c,d implies not a,b,c are_collinear & not b,a,d are_collinear & not c,d,a are_collinear & not d,c,b are_collinear & not a,c,b are_collinear & not b,a,c are_collinear & not b,c,a are_collinear & not c,a,b are_collinear & not c,b,a are_collinear & not b,d,a are_collinear & not a,b,d are_collinear & not a,d,b are_collinear & not d,a,b are_collinear & not d,b,a are_collinear & not c,a,d are_collinear & not a,c,d are_collinear & not a,d,c are_collinear & not d,a,c are_collinear & not d,c,a are_collinear & not d,b,c are_collinear & not b,c,d are_collinear & not b,d,c are_collinear & not c,b,d are_collinear & not c,d,b are_collinear; theorem :: PARSP_2:29 parallelogram a,b,c,d implies not a,b,x are_collinear or not c,d, x are_collinear; theorem :: PARSP_2:30 parallelogram a,b,c,d implies parallelogram a,c,b,d; theorem :: PARSP_2:31 parallelogram a,b,c,d implies parallelogram c,d,a,b; theorem :: PARSP_2:32 parallelogram a,b,c,d implies parallelogram b,a,d,c; theorem :: PARSP_2:33 parallelogram a,b,c,d implies parallelogram a,c,b,d & parallelogram c,d,a,b & parallelogram b,a,d,c & parallelogram c,a,d,b & parallelogram d,b,c,a & parallelogram b,d,a,c & parallelogram d,c,b,a; theorem :: PARSP_2:34 not a,b,c are_collinear implies ex d st parallelogram a,b,c,d; theorem :: PARSP_2:35 parallelogram a,b,c,p & parallelogram a,b,c,q implies p=q; theorem :: PARSP_2:36 parallelogram a,b,c,d implies not a,d '||' b,c; theorem :: PARSP_2:37 parallelogram a,b,c,d implies not parallelogram a,b,d,c; theorem :: PARSP_2:38 a<>b implies ex c st a,b,c are_collinear & c <>a & c <>b; theorem :: PARSP_2:39 parallelogram a,p,b,q & parallelogram a,p,c,r implies b,c '||' q ,r; theorem :: PARSP_2:40 not b,q,c are_collinear & parallelogram a,p,b,q & parallelogram a ,p,c,r implies parallelogram b,q,c,r; theorem :: PARSP_2:41 a,b,c are_collinear & b<>c & parallelogram a,p,b,q & parallelogram a,p,c,r implies parallelogram b,q,c,r; theorem :: PARSP_2:42 parallelogram a,p,b,q & parallelogram a,p,c,r & parallelogram b, q,d,s implies c,d '||' r,s; theorem :: PARSP_2:43 a<>b implies ex c,d st parallelogram a,b,c,d; theorem :: PARSP_2:44 a<>d implies ex b,c st parallelogram a,b,c,d; definition let FdSp,a,b,r,s; pred a,b congr r,s means :: PARSP_2:def 4 a=b & r=s or ex p,q st parallelogram p,q,a,b & parallelogram p,q,r,s; end; theorem :: PARSP_2:45 a,a congr b,c implies b=c; theorem :: PARSP_2:46 a,b congr c,c implies a=b; theorem :: PARSP_2:47 a,b congr b,a implies a=b; theorem :: PARSP_2:48 a,b congr c,d implies a,b '||' c,d; theorem :: PARSP_2:49 a,b congr c,d implies a,c '||' b,d; theorem :: PARSP_2:50 a,b congr c,d & not a,b,c are_collinear implies parallelogram a,b ,c,d; theorem :: PARSP_2:51 parallelogram a,b,c,d implies a,b congr c,d; theorem :: PARSP_2:52 a,b congr c,d & a,b,c are_collinear & parallelogram r,s,a,b implies parallelogram r,s,c,d; theorem :: PARSP_2:53 a,b congr c,x & a,b congr c,y implies x=y; theorem :: PARSP_2:54 ex d st a,b congr c,d; theorem :: PARSP_2:55 a,b congr a,b; theorem :: PARSP_2:56 r,s congr a,b & r,s congr c,d implies a,b congr c,d; theorem :: PARSP_2:57 a,b congr c,d implies c,d congr a,b; theorem :: PARSP_2:58 a,b congr c,d implies b,a congr d,c;