:: Semi-Affine Space :: by Eugeniusz Kusak and Krzysztof Radziszewski :: :: Received November 30, 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 XBOOLE_0, ANALOAF, SUBSET_1, DIRAF, PARSP_2, FDIFF_1, SEMI_AF1, PENCIL_1; notations STRUCT_0, ANALOAF, DIRAF; constructors DIRAF; registrations ANALOAF, STRUCT_0; begin definition let IT be non empty AffinStruct; attr IT is Semi_Affine_Space-like means :: SEMI_AF1:def 1 (for a,b being Element of IT holds a,b // b,a) & (for a,b,c being Element of IT holds a,b // c,c) & (for a,b,p,q,r,s being Element of IT holds ( a<>b & a,b // p,q & a,b // r,s implies p,q // r,s )) & (for a,b,c being Element of IT holds ( a,b // a,c implies b,a // b,c )) & (ex a,b,c being Element of IT st not a,b // a,c) & (for a,b,p being Element of IT ex q being Element of IT st ( a,b // p,q & a,p // b,q )) & (for o,a being Element of IT holds (ex p being Element of IT st (for b,c being Element of IT holds o,a // o,p & (ex d being Element of IT st ( o,p // o,b implies o,c // o,d & p,c // b,d ))))) & (for o,a,a9,b,b9,c,c9 being Element of IT holds ( not o,a // o,b & not o,a // o,c & o,a // o,a9 & o,b // o,b9 & o,c // o,c9 & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )) & (for a,a9,b,b9,c,c9 being Element of IT holds ( not a,a9 // a,b & not a,a9 // a,c & a,a9 // b,b9 & a,a9 // c,c9 & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )) & (for a1,a2,a3,b1,b2,b3 being Element of IT holds ( a1,a2 // a1,a3 & b1,b2 // b1,b3 & a1,b2 // a2,b1 & a2,b3 // a3,b2 implies a3,b1 // a1,b3 )) & for a,b,c,d being Element of IT holds ( not a,b // a,c & a,b // c,d & a,c // b,d implies not a,d // b,c ); end; registration cluster Semi_Affine_Space-like for non empty AffinStruct; end; definition mode Semi_Affine_Space is Semi_Affine_Space-like non empty AffinStruct; end; :: :: AXIOMS OF SEMI_AFFINE SPACE :: reserve SAS for Semi_Affine_Space; reserve a,a9,a1,a2,a3,a4,b,b9,c,c9,d,d9,d1,d2,o,p,p1,p2,q,r,r1,r2,s,x, y,t,z for Element of SAS; theorem :: SEMI_AF1:1 a,b // a,b; theorem :: SEMI_AF1:2 a,b // c,d implies c,d // a,b; theorem :: SEMI_AF1:3 a,a // b,c; theorem :: SEMI_AF1:4 a,b // c,d implies b,a // c,d; theorem :: SEMI_AF1:5 a,b // c,d implies a,b // d,c; theorem :: SEMI_AF1:6 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 :: SEMI_AF1:7 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 :: SEMI_AF1:8 a<>b & p,q // a,b & a,b // r,s implies p,q // r,s; theorem :: SEMI_AF1:9 not a,b // a,d implies a<>b & b<>d & d<>a; theorem :: SEMI_AF1:10 not a,b // p,q implies a<>b & p<>q; theorem :: SEMI_AF1:11 a,b // a,x & b,c // b,x & c,a // c,x implies a,b // a,c; theorem :: SEMI_AF1:12 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; theorem :: SEMI_AF1:13 p<>q implies ex r st not p,q // p,r; theorem :: SEMI_AF1:14 not a,b // a,c implies not a,b // c,a & not b,a // a,c & not b,a // c,a & not a,c // a,b & not a,c // b,a & not c,a // a,b & not c,a // b,a & not b,a // b,c & not b,a // c,b & not a,b // b,c & not a,b // c,b & not b,c // b,a & not b,c // a,b & not c,b // a,b & not c,b // b,a & not c,b // c,a & not c ,b // a,c & not b,c // c,a & not b,c // a,c & not c,a // c,b & not c,a // b,c & not a,c // b,c & not a,c // c,b; theorem :: SEMI_AF1:15 not a,b // c,d & a,b // p,q & c,d // r,s & p<>q & r<>s implies not p,q // r,s ; theorem :: SEMI_AF1:16 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 :: SEMI_AF1:17 not a,b // a,c & a,c // p,r & b,c // p,r implies p=r; theorem :: SEMI_AF1:18 not p,q // p,r1 & p,r1 // p,r2 & q,r1 // q,r2 implies r1=r2; theorem :: SEMI_AF1:19 not a,b // a,c & a,b // p,q & a,c // p,r1 & a,c // p,r2 & b,c // q,r1 & b,c // q,r2 implies r1=r2; theorem :: SEMI_AF1:20 a=b or c =d or a=c & b=d or a=d & b=c implies a,b // c,d; theorem :: SEMI_AF1:21 a=b or a=c or b=c implies a,b // a,c; :: :: BASIC FACTS ABOUT COLLINEARITY RELATION :: definition let SAS,a,b,c; pred a,b,c are_collinear means :: SEMI_AF1:def 2 a,b // a,c; end; theorem :: SEMI_AF1:22 a1,a2,a3 are_collinear implies a1,a3,a2 are_collinear & a2,a1,a3 are_collinear & a2,a3,a1 are_collinear & a3,a1,a2 are_collinear & a3,a2,a1 are_collinear; theorem :: SEMI_AF1:23 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 :: SEMI_AF1:24 a=b or b=c or c =a implies a,b,c are_collinear; theorem :: SEMI_AF1:25 p<>q implies ex r st not p,q,r are_collinear; theorem :: SEMI_AF1:26 a,b,c are_collinear & a,b,d are_collinear implies a,b // c,d; theorem :: SEMI_AF1:27 not a,b,c are_collinear & a,b // c,d implies not a,b,d are_collinear; theorem :: SEMI_AF1:28 not a,b,c are_collinear & a,b // c,d & c <>d & c,d,x are_collinear implies not a,b,x are_collinear; theorem :: SEMI_AF1:29 not o,a,b are_collinear & o,a,x are_collinear & o,b,x are_collinear implies o=x; theorem :: SEMI_AF1:30 o<>a & o<>b & o,a,b are_collinear & o,a,a9 are_collinear & o,b,b9 are_collinear implies a,b // a9,b9; theorem :: SEMI_AF1:31 not a,b // c,d & a,b,p1 are_collinear & a,b,p2 are_collinear & c,d,p1 are_collinear & c,d,p2 are_collinear implies p1=p2; theorem :: SEMI_AF1:32 a<>b & a,b,c are_collinear & a,b // c,d implies a,c // b,d; theorem :: SEMI_AF1:33 a<>b & a,b,c are_collinear & a,b // c,d implies c,b // c,d; theorem :: SEMI_AF1:34 not o,a,c are_collinear & o,a,b are_collinear & o,c,d1 are_collinear & o,c,d2 are_collinear & a,c // b,d1 & a,c // b,d2 implies d1=d2; theorem :: SEMI_AF1:35 a<>b & a,b,c are_collinear & a,b,d are_collinear implies a,c,d are_collinear; :: :: PARALLELOGRAM :: definition let SAS,a,b,c,d; pred parallelogram a,b,c,d means :: SEMI_AF1:def 3 not a,b,c are_collinear & a,b // c,d & a,c // b,d; end; theorem :: SEMI_AF1:36 parallelogram a,b,c,d implies a<>b & a<>c & c <>b & a<>d & b<>d & c <>d; theorem :: SEMI_AF1:37 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 :: SEMI_AF1:38 parallelogram a1,a2,a3,a4 implies not a1,a2,a3 are_collinear & not a1,a3,a2 are_collinear & not a1,a2,a4 are_collinear & not a1,a4,a2 are_collinear & not a1,a3,a4 are_collinear & not a1,a4,a3 are_collinear & not a2, a1,a3 are_collinear & not a2,a3,a1 are_collinear & not a2,a1,a4 are_collinear & not a2,a4,a1 are_collinear & not a2,a3,a4 are_collinear & not a2,a4,a3 are_collinear & not a3,a1,a2 are_collinear & not a3,a2,a1 are_collinear & not a3, a1,a4 are_collinear & not a3,a4,a1 are_collinear & not a3,a2,a4 are_collinear & not a3,a4,a2 are_collinear & not a4,a1,a2 are_collinear & not a4,a2,a1 are_collinear & not a4,a1,a3 are_collinear & not a4,a3,a1 are_collinear & not a4, a2,a3 are_collinear & not a4,a3,a2 are_collinear; theorem :: SEMI_AF1:39 parallelogram a,b,c,d implies not a,b,x are_collinear or not c,d, x are_collinear; theorem :: SEMI_AF1:40 parallelogram a,b,c,d implies parallelogram a,c,b,d; theorem :: SEMI_AF1:41 parallelogram a,b,c,d implies parallelogram c,d,a,b; theorem :: SEMI_AF1:42 parallelogram a,b,c,d implies parallelogram b,a,d,c; theorem :: SEMI_AF1:43 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; theorem :: SEMI_AF1:44 not a,b,c are_collinear implies ex d st parallelogram a,b,c,d; theorem :: SEMI_AF1:45 parallelogram a,b,c,d1 & parallelogram a,b,c,d2 implies d1=d2; theorem :: SEMI_AF1:46 parallelogram a,b,c,d implies not a,d // b,c; theorem :: SEMI_AF1:47 parallelogram a,b,c,d implies not parallelogram a,b,d,c; theorem :: SEMI_AF1:48 a<>b implies ex c st a,b,c are_collinear & c <>a & c <>b; theorem :: SEMI_AF1:49 parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 implies b,c // b9,c9; theorem :: SEMI_AF1:50 not b,b9,c are_collinear & parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 implies parallelogram b,b9,c,c9; theorem :: SEMI_AF1:51 a,b,c are_collinear & b<>c & parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 implies parallelogram b,b9,c,c9; theorem :: SEMI_AF1:52 parallelogram a,a9,b,b9 & parallelogram a,a9,c,c9 & parallelogram b,b9,d,d9 implies c,d // c9,d9; theorem :: SEMI_AF1:53 a<>d implies ex b,c st parallelogram a,b,c,d; :: :: CONGRUENCE :: definition let SAS,a,b,r,s; pred congr a,b,r,s means :: SEMI_AF1:def 4 a=b & r =s or ex p,q st parallelogram p,q,a, b & parallelogram p,q,r,s; end; theorem :: SEMI_AF1:54 congr a,a,b,c implies b=c; theorem :: SEMI_AF1:55 congr a,b,c,c implies a=b; theorem :: SEMI_AF1:56 congr a,b,b,a implies a=b; theorem :: SEMI_AF1:57 congr a,b,c,d implies a,b // c,d; theorem :: SEMI_AF1:58 congr a,b,c,d implies a,c // b,d; theorem :: SEMI_AF1:59 congr a,b,c,d & not a,b,c are_collinear implies parallelogram a,b ,c,d; theorem :: SEMI_AF1:60 parallelogram a,b,c,d implies congr a,b,c,d; theorem :: SEMI_AF1:61 congr a,b,c,d & a,b,c are_collinear & parallelogram r,s,a,b implies parallelogram r,s,c,d; theorem :: SEMI_AF1:62 congr a,b,c,x & congr a,b,c,y implies x=y; theorem :: SEMI_AF1:63 ex d st congr a,b,c,d; theorem :: SEMI_AF1:64 congr a,b,a,b; theorem :: SEMI_AF1:65 congr r,s,a,b & congr r,s,c,d implies congr a,b,c,d; theorem :: SEMI_AF1:66 congr a,b,c,d implies congr c,d,a,b; theorem :: SEMI_AF1:67 congr a,b,c,d implies congr b,a,d,c; theorem :: SEMI_AF1:68 congr a,b,c,d implies congr a,c,b,d; theorem :: SEMI_AF1:69 congr a,b,c,d implies congr c,d,a,b & congr b,a,d,c & congr a,c, b,d & congr d,c,b,a & congr b,d,a,c & congr c,a,d,b & congr d,b,c,a; theorem :: SEMI_AF1:70 congr a,b,p,q & congr b,c,q,s implies congr a,c,p,s; theorem :: SEMI_AF1:71 congr b,a,p,q & congr c,a,p,r implies congr b,c,r,q; theorem :: SEMI_AF1:72 congr a,o,o,p & congr b,o,o,q implies congr a,b,q,p; theorem :: SEMI_AF1:73 congr b,a,p,q & congr c,a,p,r implies b,c // q,r; theorem :: SEMI_AF1:74 congr a,o,o,p & congr b,o,o,q implies a,b // p,q; :: :: A VECTOR' GROUP :: definition let SAS,a,b,o; func sum(a,b,o) -> Element of SAS means :: SEMI_AF1:def 5 congr o,a,b,it; end; definition let SAS,a,o; func opposite(a,o) -> Element of SAS means :: SEMI_AF1:def 6 sum(a,it,o) = o; end; definition let SAS,a,b,o; func diff(a,b,o) -> Element of SAS equals :: SEMI_AF1:def 7 sum(a,opposite(b,o),o); end; theorem :: SEMI_AF1:75 sum(a,o,o)=a; theorem :: SEMI_AF1:76 ex x st sum(a,x,o)=o; theorem :: SEMI_AF1:77 sum(sum(a,b,o),c,o)=sum(a,sum(b,c,o),o); theorem :: SEMI_AF1:78 sum(a,b,o)=sum(b,a,o); theorem :: SEMI_AF1:79 sum(a,a,o)=o implies a=o; theorem :: SEMI_AF1:80 sum(a,x,o)=sum(a,y,o) implies x=y; theorem :: SEMI_AF1:81 congr a,o,o,opposite(a,o); theorem :: SEMI_AF1:82 opposite(a,o)=opposite(b,o) implies a=b; theorem :: SEMI_AF1:83 a,b // opposite(a,o),opposite(b,o); theorem :: SEMI_AF1:84 opposite(o,o)=o; theorem :: SEMI_AF1:85 p,q // sum(p,r,o),sum(q,r,o); theorem :: SEMI_AF1:86 p,q // r,s implies p,q // sum(p,r,o),sum(q,s,o); theorem :: SEMI_AF1:87 diff(a,b,o)=o iff a=b; theorem :: SEMI_AF1:88 o,diff(b,a,o) // a,b; theorem :: SEMI_AF1:89 o,diff(b,a,o),diff(d,c,o) are_collinear iff a,b // c,d; :: :: A TRAPEZIUM RELATION :: definition let SAS,a,b,c,d,o; pred trap a,b,c,d,o means :: SEMI_AF1:def 8 not o,a,c are_collinear & o,a,b are_collinear & o,c,d are_collinear & a,c // b,d; end; definition let SAS,o,p; pred qtrap o,p means :: SEMI_AF1:def 9 for b,c holds ex d st ( o,p,b are_collinear implies o,c,d are_collinear & p,c // b,d); end; theorem :: SEMI_AF1:90 trap a,b,c,d,o implies o<>a & a<>c & c <>o; theorem :: SEMI_AF1:91 trap a,b,c,x,o & trap a,b,c,y,o implies x=y; theorem :: SEMI_AF1:92 not o,a,b are_collinear implies trap a,o,b,o,o; theorem :: SEMI_AF1:93 trap a,b,c,d,o implies trap c,d,a,b,o; theorem :: SEMI_AF1:94 trap a,b,c,d,d implies d=b; theorem :: SEMI_AF1:95 o<>b & trap a,b,c,d,o implies not o,b,d are_collinear; theorem :: SEMI_AF1:96 o<>b & trap a,b,c,d,o implies trap b,a,d,c,o; theorem :: SEMI_AF1:97 trap a,b,c,d,b implies b=d; theorem :: SEMI_AF1:98 trap a,p,b,q,o & trap a,p,c,r,o implies b,c // q,r; theorem :: SEMI_AF1:99 trap a,p,b,q,o & trap a,p,c,r,o & not o,b,c are_collinear implies trap b,q,c,r,o; theorem :: SEMI_AF1:100 trap a,p,b,q,o & trap a,p,c,r,o & trap b,q,d,s,o implies c,d // r,s; theorem :: SEMI_AF1:101 for o,a holds ex p st o,a,p are_collinear & qtrap o,p; theorem :: SEMI_AF1:102 ex x,y,z st x<>y & y<>z & z<>x; theorem :: SEMI_AF1:103 qtrap o,p implies o<>p; theorem :: SEMI_AF1:104 qtrap o,p implies ex q st not o,p,q are_collinear & qtrap o,q; theorem :: SEMI_AF1:105 not o,p,c are_collinear & o,p,b are_collinear & qtrap o,p implies ex d st trap p,b,c,d,o;