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;