Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### A Construction of an Abstract Space of Congruence of Vectors

**by****Grzegorz Lewandowski, and****Krzysztof Prazmowski**- Received May 23, 1990
- MML identifier: TDGROUP

- [ Mizar article, MML identifier index ]

environ vocabulary RLVECT_1, VECTSP_1, FUNCT_1, ARYTM_1, RELAT_1, ANALOAF, REALSET1, TDGROUP, ARYTM_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, REAL_1, STRUCT_0, ANALOAF, FUNCT_1, RELSET_1, BINOP_1, RLVECT_1, VECTSP_1, REALSET1; constructors DOMAIN_1, ANALOAF, BINOP_1, REAL_1, MEMBERED, XBOOLE_0; clusters ANALOAF, VECTSP_1, RELSET_1, STRUCT_0, MEMBERED, ZFMISC_1, XBOOLE_0; requirements NUMERALS, SUBSET, BOOLE, ARITHM; begin canceled; theorem :: TDGROUP:2 for a being Element of G_Real holds ex b being Element of G_Real st b + b = a; theorem :: TDGROUP:3 for a being Element of G_Real st a + a = 0.G_Real holds a = 0.G_Real; definition let IT be non empty LoopStr; 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; definition cluster G_Real -> Fanoian Two_Divisible; end; definition cluster strict Fanoian Two_Divisible add-associative right_zeroed right_complementable Abelian (non empty LoopStr); end; definition mode Two_Divisible_Group is Two_Divisible add-associative right_zeroed right_complementable Abelian (non empty LoopStr); end; definition mode Uniquely_Two_Divisible_Group is Fanoian Two_Divisible add-associative right_zeroed right_complementable Abelian (non empty LoopStr); end; canceled 3; theorem :: TDGROUP:7 for AG being add-associative right_zeroed right_complementable Abelian (non empty LoopStr) 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,a',b',c',p,q for Element of ADG; reserve x,y for set; definition let ADG be non empty LoopStr; let a,b be Element of ADG; redefine func a+b; synonym a # b; end; definition let ADG be non empty LoopStr; canceled 2; func CONGRD(ADG) -> Relation of [:the carrier of ADG,the carrier of ADG:] means :: TDGROUP:def 4 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 LoopStr; func AV(ADG) -> strict AffinStruct equals :: TDGROUP:def 5 AffinStruct(#the carrier of ADG,CONGRD(ADG)#); end; definition let ADG be non empty LoopStr; cluster AV ADG -> non empty; end; canceled; theorem :: TDGROUP:9 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 6 [[a,b],[c,d]] in the CONGR of AV(ADG); end; theorem :: TDGROUP:10 a,b ==> c,d iff a # d = b # c; theorem :: TDGROUP:11 ex a,b being Element of G_Real st a<>b; theorem :: TDGROUP:12 ex ADG st ex a,b st a<>b; theorem :: TDGROUP:13 a,b ==> c,c implies a=b; theorem :: TDGROUP:14 a,b ==> p,q & c,d ==> p,q implies a,b ==> c,d; theorem :: TDGROUP:15 ex d st (a,b ==> c,d); theorem :: TDGROUP:16 a,b ==> a',b' & a,c ==> a',c' implies b,c ==> b',c'; theorem :: TDGROUP:17 ex b st (a,b ==> b,c); theorem :: TDGROUP:18 a,b ==> b,c & a,b' ==> b',c implies b=b'; theorem :: TDGROUP:19 a,b ==> c,d implies a,c ==> b,d; reserve AS for non empty AffinStruct; theorem :: TDGROUP:20 (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,a',b',c' being Element of AV(ADG) st a,b // a',b' & a,c // a',c' holds b,c // b',c') & (for a,c being Element of AV(ADG) ex b being Element of AV(ADG) st a,b // b,c) & (for a,b,c,b' being Element of AV(ADG) st a,b // b,c & a,b' // b',c holds b = b') & (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; canceled; attr IT is AffVect-like means :: TDGROUP:def 8 (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,a',b',c' being Element of IT st a,b // a',b' & a,c // a',c' holds b,c // b',c') & (for a,c being Element of IT ex b being Element of IT st a,b // b,c) & (for a,b,c,b' being Element of IT st a,b // b,c & a,b' // b',c holds b = b') & (for a,b,c,d being Element of IT st a,b // c,d holds a,c // b,d); end; definition cluster strict non trivial AffVect-like (non empty AffinStruct); end; definition mode AffVect is non trivial AffVect-like (non empty AffinStruct); end; theorem :: TDGROUP:21 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,a',b',c' being Element of AS st a,b // a',b' & a,c // a',c' holds b,c // b',c') & (for a,c being Element of AS ex b being Element of AS st a,b // b,c) & (for a,b,c,b' being Element of AS st a,b // b,c & a,b' // b',c holds b = b') & (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:22 (ex a,b being Element of ADG st a<>b) implies AV(ADG) is AffVect;

Back to top