:: A Construction of an Abstract Space of Congruence of Vectors :: by Grzegorz Lewandowski and Krzysztof Pra\.zmowski :: :: Received May 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 SUBSET_1, VECTSP_1, ARYTM_3, NUMBERS, SUPINF_2, XBOOLE_0, ALGSTR_0, STRUCT_0, RLVECT_1, PBOOLE, RELAT_1, ZFMISC_1, ANALOAF, CARD_1, ARYTM_1, TDGROUP; notations TARSKI, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, REAL_1, STRUCT_0, ALGSTR_0, ANALOAF, RELSET_1, RLVECT_1, VECTSP_1; constructors BINOP_2, ANALOAF, REAL_1, DOMAIN_1, VECTSP_1, MEMBERED, NUMBERS; registrations RELSET_1, STRUCT_0, VECTSP_1, ANALOAF, MEMBERED, XREAL_0; requirements NUMERALS, SUBSET, BOOLE, ARITHM; begin theorem :: TDGROUP:1 for a being Element of G_Real holds ex b being Element of G_Real st b + b = a ; theorem :: TDGROUP:2 for a being Element of G_Real st a + a = 0.G_Real holds a = 0.G_Real; definition let IT be non empty addLoopStr; attr IT is Two_Divisible means :: TDGROUP:def 1 for a being Element of IT holds ex b being Element of IT st b + b = a; end; registration cluster G_Real -> Fanoian Two_Divisible; end; registration cluster strict Fanoian Two_Divisible add-associative right_zeroed right_complementable Abelian for non empty addLoopStr; end; definition mode Two_Divisible_Group is Two_Divisible add-associative right_zeroed right_complementable Abelian non empty addLoopStr; end; definition mode Uniquely_Two_Divisible_Group is Fanoian Two_Divisible add-associative right_zeroed right_complementable Abelian non empty addLoopStr; end; theorem :: TDGROUP:3 for AG being add-associative right_zeroed right_complementable Abelian non empty addLoopStr holds (AG is Uniquely_Two_Divisible_Group iff (for a being Element of AG holds (ex b being Element of AG st b + b = a)) & (for a being Element of AG st a + a = 0.AG holds a = 0.AG)); reserve ADG for Uniquely_Two_Divisible_Group; reserve a,b,c,d,a9,b9,c9,p,q for Element of ADG; reserve x,y for set; notation let ADG be non empty addLoopStr; let a,b be Element of ADG; synonym a # b for a+b; end; definition let ADG be non empty addLoopStr; func CONGRD(ADG) -> Relation of [:the carrier of ADG,the carrier of ADG:] means :: TDGROUP:def 2 for a,b,c,d being Element of ADG holds [[a,b],[c,d]] in it iff a # d = b # c; end; definition let ADG be non empty addLoopStr; func AV(ADG) -> strict AffinStruct equals :: TDGROUP:def 3 AffinStruct(#the carrier of ADG, CONGRD(ADG)#); end; registration let ADG be non empty addLoopStr; cluster AV ADG -> non empty; end; theorem :: TDGROUP:4 the carrier of AV(ADG) = the carrier of ADG & the CONGR of AV(ADG) = CONGRD(ADG); definition let ADG; let a,b,c,d; pred a,b ==> c,d means :: TDGROUP:def 4 [[a,b],[c,d]] in the CONGR of AV(ADG); end; theorem :: TDGROUP:5 a,b ==> c,d iff a # d = b # c; theorem :: TDGROUP:6 ex a,b being Element of G_Real st a<>b; theorem :: TDGROUP:7 ex ADG st ex a,b st a<>b; theorem :: TDGROUP:8 a,b ==> c,c implies a=b; theorem :: TDGROUP:9 a,b ==> p,q & c,d ==> p,q implies a,b ==> c,d; theorem :: TDGROUP:10 ex d st a,b ==> c,d; theorem :: TDGROUP:11 a,b ==> a9,b9 & a,c ==> a9,c9 implies b,c ==> b9,c9; theorem :: TDGROUP:12 ex b st a,b ==> b,c; theorem :: TDGROUP:13 a,b ==> b,c & a,b9 ==> b9,c implies b=b9; theorem :: TDGROUP:14 a,b ==> c,d implies a,c ==> b,d; reserve AS for non empty AffinStruct; theorem :: TDGROUP:15 (ex a,b being Element of ADG st a<>b) implies (ex a,b being Element of AV(ADG) st a<>b) & (for a,b,c being Element of AV(ADG) st a,b // c,c holds a=b) & (for a,b,c,d,p,q being Element of AV(ADG) st a,b // p,q & c,d // p ,q holds a,b // c,d) & (for a,b,c being Element of AV(ADG) ex d being Element of AV(ADG) st a,b // c,d) & (for a,b,c,a9,b9,c9 being Element of AV(ADG) st a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9) & (for a,c being Element of AV(ADG) ex b being Element of AV(ADG) st a,b // b,c) & (for a,b,c,b9 being Element of AV(ADG) st a,b // b,c & a,b9 // b9,c holds b = b9) & for a,b,c,d being Element of AV(ADG) st a,b // c,d holds a,c // b,d; definition let IT be non empty AffinStruct; attr IT is AffVect-like means :: TDGROUP:def 5 (for a,b,c being Element of IT st a,b // c,c holds a=b) & (for a,b,c,d,p,q being Element of IT st a,b // p,q & c,d // p,q holds a,b // c,d) & (for a,b,c being Element of IT ex d being Element of IT st a,b // c,d) & (for a,b,c,a9,b9,c9 being Element of IT st a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9) & (for a,c being Element of IT ex b being Element of IT st a,b // b,c) & (for a,b,c,b9 being Element of IT st a,b // b,c & a,b9 // b9,c holds b = b9) & for a,b,c,d being Element of IT st a,b // c,d holds a,c // b,d; end; registration cluster strict AffVect-like for non trivial AffinStruct; end; definition mode AffVect is AffVect-like non trivial AffinStruct; end; theorem :: TDGROUP:16 for AS holds (ex a,b being Element of AS st a<>b) & (for a,b,c being Element of AS st a,b // c,c holds a=b) & (for a,b,c,d,p,q being Element of AS st a,b // p,q & c,d // p,q holds a,b // c,d) & (for a,b,c being Element of AS ex d being Element of AS st a,b // c,d) & (for a,b,c,a9,b9,c9 being Element of AS st a,b // a9,b9 & a,c // a9,c9 holds b,c // b9,c9) & (for a,c being Element of AS ex b being Element of AS st a,b // b,c) & (for a,b,c,b9 being Element of AS st a,b // b,c & a,b9 // b9,c holds b = b9) & (for a,b,c,d being Element of AS st a,b // c,d holds a,c // b,d) iff AS is AffVect; theorem :: TDGROUP:17 (ex a,b being Element of ADG st a<>b) implies AV(ADG) is AffVect;