:: From Loops to Abelian Multiplicative Groups with Zero
::  by Micha{\l} Muzalewski and Wojciech Skaba
::
:: Received July 10, 1990
:: Copyright (c) 1990 Association of Mizar Users

environ

 vocabularies RLVECT_1, BOOLE, ARYTM_1, VECTSP_1, CAT_1, BINOP_1, RELAT_1,
      ARYTM_3, ALGSTR_1, GROUP_1, VECTSP_2, ARYTM, ALGSTR_0;
 notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, REAL_1, BINOP_2, STRUCT_0,
      ALGSTR_0, GROUP_1, VECTSP_1, RLVECT_1;
 constructors BINOP_1, BINOP_2, VECTSP_1, RLVECT_1, FUNCT_5;
 registrations NUMBERS, VECTSP_1, ALGSTR_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: GROUPS

reserve L for non empty addLoopStr;
reserve a,b,c,x,y,z for Element of L;

theorem :: ALGSTR_1:1
  (for a holds a + 0.L = a) & (for a ex x st a+x = 0.L)
  & (for a,b,c holds (a+b)+c = a+(b+c)) implies (a+b = 0.L implies b+a = 0.L);

theorem :: ALGSTR_1:2
  (for a holds a + 0.L = a) & (for a ex x st a+x = 0.L)
  & (for a,b,c holds (a+b)+c = a+(b+c)) implies 0.L+a = a+0.L;

theorem :: ALGSTR_1:3
  (for a holds a + 0.L = a) & (for a ex x st a+x = 0.L)
  & (for a,b,c holds (a+b)+c = a+(b+c)) implies for a ex x st x+a = 0.L;

definition
  let x be set;
  canceled 2;
  func Extract x -> Element of {x} equals
:: ALGSTR_1:def 3

  x;
end;

canceled;

theorem :: ALGSTR_1:5
  for a,b being Element of Trivial-addLoopStr holds a = b;

theorem :: ALGSTR_1:6
  for a,b be Element of Trivial-addLoopStr holds a+b = 0. Trivial-addLoopStr;

definition
  let IT be non empty addLoopStr;
  canceled;
  attr IT is left_zeroed means
:: ALGSTR_1:def 5

  for a being Element of IT holds 0.IT + a = a;
end;

definition
  let L be non empty addLoopStr;
  canceled 2;
  attr L is add-left-invertible means
:: ALGSTR_1:def 8

  for a,b be Element of L
  ex x being Element of L st x + a = b;
  attr L is add-right-invertible means
:: ALGSTR_1:def 9

  for a,b be Element of L
  ex x being Element of L st a + x = b;
end;

definition
  let IT be non empty addLoopStr;
  canceled 2;
  attr IT is Loop-like means
:: ALGSTR_1:def 12

  IT is left_add-cancelable right_add-cancelable
  add-left-invertible add-right-invertible;
end;

registration
  cluster Loop-like -> left_add-cancelable right_add-cancelable
    add-left-invertible add-right-invertible (non empty addLoopStr);
  cluster left_add-cancelable right_add-cancelable
    add-left-invertible add-right-invertible ->
    Loop-like (non empty addLoopStr);
end;

theorem :: ALGSTR_1:7
  for L being non empty addLoopStr holds L is Loop-like iff
  (for a,b be Element of L ex x being Element of L st a+x=b)
  & (for a,b be Element of L ex x being Element of L st x+a=b)
  & (for a,x,y be Element of L holds a+x=a+y implies x=y)
  & (for a,x,y be Element of L holds x+a=y+a implies x=y);

registration
  cluster Trivial-addLoopStr
    -> add-associative Loop-like right_zeroed left_zeroed;
end;

registration
  cluster strict left_zeroed right_zeroed Loop-like (non empty addLoopStr);
end;

definition
  mode Loop is left_zeroed right_zeroed Loop-like (non empty addLoopStr);
end;

registration
  cluster strict add-associative Loop;
end;

definition
  mode AddGroup is add-associative Loop;
end;

registration
  cluster Loop-like -> add-left-invertible (non empty addLoopStr);
  cluster add-associative right_zeroed right_complementable
    -> left_zeroed Loop-like (non empty addLoopStr);
end;

canceled;

theorem :: ALGSTR_1:9
  L is AddGroup iff (for a holds a + 0.L = a) & (for a ex x st a+x = 0.L)
  & (for a,b,c holds (a+b)+c = a+(b+c));

registration
  cluster Trivial-addLoopStr -> Abelian;
end;

registration
  cluster strict Abelian AddGroup;
end;

canceled;

theorem :: ALGSTR_1:11
  L is Abelian AddGroup iff (for a holds a + 0.L = a)
  & (for a ex x st a+x = 0.L) & (for a,b,c holds (a+b)+c = a+(b+c))
  & (for a,b holds a+b = b+a);

registration
  cluster Trivial-multLoopStr -> non empty;
end;

canceled 6;

theorem :: ALGSTR_1:18
  for a,b being Element of Trivial-multLoopStr holds a = b;

theorem :: ALGSTR_1:19
  for a,b be Element of Trivial-multLoopStr
  holds a*b = 1.Trivial-multLoopStr;

definition
  let IT be non empty multLoopStr;
  canceled;
  attr IT is invertible means
:: ALGSTR_1:def 14

  (for a,b be Element of IT
  ex x being Element of IT st a*x=b) & (for a,b be Element of IT
  ex x being Element of IT st x*a=b);
  canceled;
end;

notation
  let L be non empty multLoopStr;
  synonym L is cancelable for L is mult-cancelable;
end;

registration
  cluster strict well-unital invertible cancelable (non empty multLoopStr);
end;

definition
  mode multLoop is well-unital invertible cancelable (non empty multLoopStr);
end;

registration
  cluster Trivial-multLoopStr -> well-unital invertible cancelable;
end;

registration
  cluster strict associative multLoop;
end;

definition
  mode multGroup is associative multLoop;
end;

reserve L for non empty multLoopStr;
reserve a,b,c,x,y,z for Element of L;

canceled 2;

theorem :: ALGSTR_1:22
  L is multGroup iff (for a holds a * 1.L = a) & (for a ex x st a*x = 1.L)
  & (for a,b,c holds (a*b)*c = a*(b*c));

registration
  cluster Trivial-multLoopStr -> associative;
end;

registration
  cluster strict commutative multGroup;
end;

canceled;

theorem :: ALGSTR_1:24
  L is commutative multGroup iff (for a holds a * 1.L = a)
  & (for a ex x st a*x = 1.L) & (for a,b,c holds (a*b)*c = a*(b*c))
  & (for a,b holds a*b = b*a);

notation
  let L be invertible cancelable (non empty multLoopStr);
  let x be Element of L;
  synonym x" for /x;
end;

registration
  let L be invertible cancelable (non empty multLoopStr);
  cluster -> left_invertible Element of L;
end;

reserve G for multGroup;
reserve a,b,c,x for Element of G;

canceled;

theorem :: ALGSTR_1:26
  a"*a=1.G & a*(a") = 1.G;

definition
  canceled 3;
  let L be invertible cancelable (non empty multLoopStr);
  let a, b be Element of L;
  func a/b -> Element of L equals
:: ALGSTR_1:def 19

  a*(b");
end;

definition
  canceled 3;
  func multEX_0 -> strict multLoopStr_0 equals
:: ALGSTR_1:def 23
  multLoopStr_0 (# REAL, multreal, 0, 1 #);
end;

registration
  cluster multEX_0 -> non empty;
end;

registration
  cluster multEX_0 -> well-unital;
end;

canceled 5;

theorem :: ALGSTR_1:32
  for q,p be Real st q<>0 ex y be Real st p=q*y;

theorem :: ALGSTR_1:33
  for q,p be Real st q<>0 ex y be Real st p=y*q;

definition
  let IT be non empty multLoopStr_0;
  attr IT is almost_invertible means
:: ALGSTR_1:def 24

  (for a,b be Element of IT st a<>0.IT ex x be Element of IT st a*x=b) &
  (for a,b be Element of IT st a<>0.IT ex x be Element of IT st x*a=b);
end;

definition
  let IT be non empty multLoopStr_0;
  canceled;
  attr IT is multLoop_0-like means
:: ALGSTR_1:def 26

  IT is almost_invertible almost_cancelable
  & (for a be Element of IT holds a*0.IT = 0.IT)
  & (for a be Element of IT holds 0.IT*a = 0.IT);
end;

theorem :: ALGSTR_1:34
  for L being non empty multLoopStr_0 holds L is multLoop_0-like iff
  (for a,b be Element of L st a<>0.L ex x be Element of L st a*x=b) &
  (for a,b be Element of L st a<>0.L ex x be Element of L st x*a=b) &
  (for a,x,y be Element of L st a<>0.L holds a*x=a*y implies x=y) &
  (for a,x,y be Element of L st a<>0.L holds x*a=y*a implies x=y) &
  (for a be Element of L holds a*0.L = 0.L) &
  (for a be Element of L holds 0.L*a = 0.L);

registration
  cluster multLoop_0-like -> almost_invertible almost_cancelable
    (non empty multLoopStr_0);
end;

registration
  cluster strict well-unital multLoop_0-like non degenerated
    (non empty multLoopStr_0);
end;

definition
  mode multLoop_0 is well-unital non degenerated multLoop_0-like
    (non empty multLoopStr_0);
end;

registration
  cluster multEX_0 -> well-unital multLoop_0-like;
end;

registration
  cluster strict associative non degenerated multLoop_0;
end;

definition
  mode multGroup_0 is associative non degenerated multLoop_0;
end;

reserve L for non empty multLoopStr_0;
reserve a,b,c,x,y,z for Element of L;

canceled 2;

registration
  cluster multEX_0 -> associative;
end;

registration
  cluster strict commutative multGroup_0;
end;

canceled 2;

definition
  let L be almost_invertible almost_cancelable (non empty multLoopStr_0);
  let x be Element of L;
  assume
 x<>0.L;
  redefine func x" means
:: ALGSTR_1:def 27

  it*x = 1.L;
end;

reserve G for associative almost_invertible almost_cancelable well-unital
  (non empty multLoopStr_0);

reserve a,x for Element of G;

canceled;

theorem :: ALGSTR_1:40
  a<>0.G implies a"*a=1.G & a*(a") = 1.G;

definition
  let L be almost_invertible almost_cancelable (non empty multLoopStr_0);
  let a, b be Element of L;
  func a/b -> Element of L equals
:: ALGSTR_1:def 28

  a*(b");
end;