:: Basic Algebraic Structures
::  by Library Committee
::
:: Received December 8, 2007
:: Copyright (c) 2007 Association of Mizar Users

environ

 vocabularies STRUCT_0, BINOP_1, FUNCT_1, RLVECT_1, CAT_1, ARYTM_1, VECTSP_1,
      MIDSP_1, REALSET1, ALGSTR_1, GROUP_1, ARYTM_3, BINOM, RELAT_1, ALGSTR_0,
      VECTSP_2;
 notations XBOOLE_0, SUBSET_1, REALSET1, FUNCT_5, STRUCT_0, BINOP_1;
 constructors BINOP_1, STRUCT_0, REALSET1, FUNCT_5;
 registrations REALSET1;
 requirements BOOLE;
 theorems CARD_1, STRUCT_0;

begin :: Additive structures

reserve D for non empty set,
  d,e for Element of D,
  o,o1 for BinOp of D;

reserve T for trivial set,
  s,t for Element of T,
  f,f1 for BinOp of T;

reserve N for non trivial set,
  n,m for Element of N,
  b,b1 for BinOp of N;

definition
  struct (1-sorted) addMagma (# carrier -> set,
    addF -> BinOp of the carrier #);
end;

registration
  let D,o;
  cluster addMagma(#D,o#) -> non empty;
  coherence by STRUCT_0:def 1;
end;

registration
  let T,f;
  cluster addMagma(#T,f#) -> trivial;
  coherence by STRUCT_0:def 9;
end;

registration
  let N,b;
  cluster addMagma(#N,b#) -> non trivial;
  coherence by STRUCT_0:def 9;
end;

definition
  let M be addMagma;
  let x,y be Element of M;
  func x+y -> Element of M equals

  (the addF of M).(x,y);
  coherence;
end;

definition
  func Trivial-addMagma -> addMagma equals

  addMagma(#1, op2 #);
  coherence;
end;

registration
  cluster Trivial-addMagma -> strict non empty trivial;
  coherence by CARD_1:87,STRUCT_0:def 9;
end;

registration
  cluster strict non empty trivial addMagma;
  existence
  proof
    take Trivial-addMagma;
    thus thesis;
  end;
end;

definition
  let M be addMagma, x be Element of M;
  attr x is left_add-cancelable means
  for y,z being Element of M st x+y = x+z holds y = z;
  attr x is right_add-cancelable means
  :Def4:
  for y,z being Element of M st y+x = z+x holds y = z;
end;

definition
  let M be addMagma, x be Element of M;
  attr x is add-cancelable means
  :Def5:
  x is right_add-cancelable left_add-cancelable;
end;

registration
  let M be addMagma;
  cluster right_add-cancelable left_add-cancelable
    -> add-cancelable Element of M;
  coherence by Def5;
  cluster add-cancelable
    -> right_add-cancelable left_add-cancelable Element of M;
  coherence by Def5;
end;

definition
  let M be addMagma;
  attr M is left_add-cancelable means
  :Def6:
  for x being Element of M holds x is left_add-cancelable;
  attr M is right_add-cancelable means
  :Def7:
  for x being Element of M holds x is right_add-cancelable;
end;

definition
  let M be addMagma;
  attr M is add-cancelable means
  :Def8:
  M is right_add-cancelable left_add-cancelable;
end;

registration
  cluster right_add-cancelable left_add-cancelable -> add-cancelable addMagma;
  coherence by Def8;
  cluster add-cancelable -> right_add-cancelable left_add-cancelable addMagma;
  coherence by Def8;
end;

registration
  cluster Trivial-addMagma -> add-cancelable;
  coherence
  proof
    set M = Trivial-addMagma;
    thus M is right_add-cancelable
    proof
      let x,y,z be Element of M;
      assume y+x = z+x;
      thus y = z by STRUCT_0:def 10;
    end;
    let x,y,z being Element of M;
    assume x+y = x+z;
    thus y = z by STRUCT_0:def 10;
  end;
end;

registration
  cluster add-cancelable strict non empty trivial addMagma;
  existence
  proof
    take Trivial-addMagma;
    thus thesis;
  end;
end;

registration
  let M be left_add-cancelable addMagma;
  cluster -> left_add-cancelable Element of M;
  coherence by Def6;
end;

registration
  let M be right_add-cancelable addMagma;
  cluster -> right_add-cancelable Element of M;
  coherence by Def7;
end;

definition
  struct (ZeroStr,addMagma) addLoopStr (# carrier -> set,
    addF -> BinOp of the carrier, ZeroF -> Element of the carrier #);
end;

registration
  let D,o,d;
  cluster addLoopStr(#D,o,d#) -> non empty;
  coherence by STRUCT_0:def 1;
end;

registration
  let T,f,t;
  cluster addLoopStr(#T,f,t#) -> trivial;
  coherence by STRUCT_0:def 9;
end;

registration
  let N,b,m;
  cluster addLoopStr(#N,b,m#) -> non trivial;
  coherence by STRUCT_0:def 9;
end;

definition
  func Trivial-addLoopStr -> addLoopStr equals

  addLoopStr(#1, op2, op0 #);
  coherence;
end;

registration
  cluster Trivial-addLoopStr -> strict non empty trivial;
  coherence by CARD_1:87,STRUCT_0:def 9;
end;

registration
  cluster strict non empty trivial addLoopStr;
  existence
  proof
    take Trivial-addLoopStr;
    thus thesis;
  end;
end;

definition
  let M be addLoopStr, x be Element of M;
  attr x is left_complementable means
  :Def10:
  ex y being Element of M st y+x = 0.M;
  attr x is right_complementable means

  ex y being Element of M st x+y = 0.M;
end;

definition
  let M be addLoopStr, x be Element of M;
  attr x is complementable means
  :Def12:
  x is right_complementable left_complementable;
end;

registration
  let M be addLoopStr;
  cluster right_complementable left_complementable
    -> complementable Element of M;
  coherence by Def12;
  cluster complementable
    -> right_complementable left_complementable Element of M;
  coherence by Def12;
end;

definition
  let M be addLoopStr, x be Element of M;
  assume
A1: x is left_complementable right_add-cancelable;
  func -x -> Element of M means

  it + x = 0.M;
  existence by A1,Def10;
  uniqueness by A1,Def4;
end;

definition
  let V be addLoopStr;
  let v,w be Element of V;
  func v - w -> Element of V equals

  v + -w;
  correctness;
end;

registration
  cluster Trivial-addLoopStr -> add-cancelable;
  coherence
  proof
    set M = Trivial-addLoopStr;
    thus M is right_add-cancelable
    proof
      let x,y,z be Element of M;
      assume y+x = z+x;
      thus y = z by STRUCT_0:def 10;
    end;
    let x,y,z being Element of M;
    assume x+y = x+z;
    thus y = z by STRUCT_0:def 10;
  end;
end;

definition
  let M be addLoopStr;
  attr M is left_complementable means
  :Def15:
  for x being Element of M holds x is left_complementable;
  attr M is right_complementable means
  :Def16:
  for x being Element of M holds x is right_complementable;
end;

definition
  let M be addLoopStr;
  attr M is complementable means
  :Def17:
  M is right_complementable left_complementable;
end;

registration
  cluster right_complementable left_complementable
    -> complementable addLoopStr;
  coherence by Def17;
  cluster complementable
    -> right_complementable left_complementable addLoopStr;
  coherence by Def17;
end;

registration
  cluster Trivial-addLoopStr -> complementable;
  coherence
  proof
    set M = Trivial-addLoopStr;
    thus M is right_complementable
    proof
      let x be Element of M;
      take x;
      thus thesis by STRUCT_0:def 10;
    end;
    let x being Element of M;
    take x;
    thus thesis by STRUCT_0:def 10;
  end;
end;

registration
  cluster complementable add-cancelable strict non empty trivial addLoopStr;
  existence
  proof
    take Trivial-addLoopStr;
    thus thesis;
  end;
end;

registration
  let M be left_complementable addLoopStr;
  cluster -> left_complementable Element of M;
  coherence by Def15;
end;

registration
  let M be right_complementable addLoopStr;
  cluster -> right_complementable Element of M;
  coherence by Def16;
end;

begin :: Multiplicative structures

definition
  struct (1-sorted) multMagma (# carrier -> set,
    multF -> BinOp of the carrier #);
end;

registration
  let D,o;
  cluster multMagma(#D,o#) -> non empty;
  coherence by STRUCT_0:def 1;
end;

registration
  let T,f;
  cluster multMagma(#T,f#) -> trivial;
  coherence by STRUCT_0:def 9;
end;

registration
  let N,b;
  cluster multMagma(#N,b#) -> non trivial;
  coherence by STRUCT_0:def 9;
end;

definition
  let M be multMagma;
  let x,y be Element of M;
  func x*y -> Element of M equals

  (the multF of M).(x,y);
  coherence;
end;

definition
  func Trivial-multMagma -> multMagma equals

  multMagma(#1, op2 #);
  coherence;
end;

registration
  cluster Trivial-multMagma -> strict non empty trivial;
  coherence by CARD_1:87,STRUCT_0:def 9;
end;

registration
  cluster strict non empty trivial multMagma;
  existence
  proof
    take Trivial-multMagma;
    thus thesis;
  end;
end;

definition
  let M be multMagma, x be Element of M;
  attr x is left_mult-cancelable means
  for y,z being Element of M st x*y = x*z holds y = z;
  attr x is right_mult-cancelable means
  :Def21:
  for y,z being Element of M st y*x = z*x holds y = z;
end;

definition
  let M be multMagma, x be Element of M;
  attr x is mult-cancelable means
  :Def22:
  x is right_mult-cancelable left_mult-cancelable;
end;

registration
  let M be multMagma;
  cluster right_mult-cancelable left_mult-cancelable
    -> mult-cancelable Element of M;
  coherence by Def22;
  cluster mult-cancelable
    -> right_mult-cancelable left_mult-cancelable Element of M;
  coherence by Def22;
end;

definition
  let M be multMagma;
  attr M is left_mult-cancelable means
  :Def23:
  for x being Element of M holds x is left_mult-cancelable;
  attr M is right_mult-cancelable means
  :Def24:
  for x being Element of M holds x is right_mult-cancelable;
end;

definition
  let M be multMagma;
  attr M is mult-cancelable means
  :Def25:
  M is left_mult-cancelable right_mult-cancelable;
end;

registration
  cluster right_mult-cancelable left_mult-cancelable
    -> mult-cancelable multMagma;
  coherence by Def25;
  cluster mult-cancelable
    -> right_mult-cancelable left_mult-cancelable multMagma;
  coherence by Def25;
end;

registration
  cluster Trivial-multMagma -> mult-cancelable;
  coherence
  proof
    set M = Trivial-multMagma;
    thus M is left_mult-cancelable
    proof
      let x,y,z be Element of M;
      assume x*y = x*z;
      thus y = z by STRUCT_0:def 10;
    end;
    let x,y,z being Element of M;
    assume y*x = z*x;
    thus y = z by STRUCT_0:def 10;
  end;
end;

registration
  cluster mult-cancelable strict non empty trivial multMagma;
  existence
  proof
    take Trivial-multMagma;
    thus thesis;
  end;
end;

registration
  let M be left_mult-cancelable multMagma;
  cluster -> left_mult-cancelable Element of M;
  coherence by Def23;
end;

registration
  let M be right_mult-cancelable multMagma;
  cluster -> right_mult-cancelable Element of M;
  coherence by Def24;
end;

definition
  struct (OneStr,multMagma) multLoopStr (# carrier -> set,
    multF -> BinOp of the carrier, OneF -> Element of the carrier #);
end;

registration
  let D,o,d;
  cluster multLoopStr(#D,o,d#) -> non empty;
  coherence by STRUCT_0:def 1;
end;

registration
  let T,f,t;
  cluster multLoopStr(#T,f,t#) -> trivial;
  coherence by STRUCT_0:def 9;
end;

registration
  let N,b,m;
  cluster multLoopStr(#N,b,m#) -> non trivial;
  coherence by STRUCT_0:def 9;
end;

definition
  func Trivial-multLoopStr -> multLoopStr equals

  multLoopStr(#1, op2, op0 #);
  coherence;
end;

registration
  cluster Trivial-multLoopStr -> strict non empty trivial;
  coherence by CARD_1:87,STRUCT_0:def 9;
end;

registration
  cluster strict non empty trivial multLoopStr;
  existence
  proof
    take Trivial-multLoopStr;
    thus thesis;
  end;
end;

registration
  cluster Trivial-multLoopStr -> mult-cancelable;
  coherence
  proof
    set M = Trivial-multLoopStr;
    thus M is left_mult-cancelable
    proof
      let x,y,z be Element of M;
      assume x*y = x*z;
      thus y = z by STRUCT_0:def 10;
    end;
    let x,y,z being Element of M;
    assume y*x = z*x;
    thus y = z by STRUCT_0:def 10;
  end;
end;

definition
  let M be multLoopStr, x be Element of M;
  attr x is left_invertible means
  :Def27:
  ex y being Element of M st y*x = 1.M;
  attr x is right_invertible means

  ex y being Element of M st x*y = 1.M;
end;

definition
  let M be multLoopStr, x be Element of M;
  attr x is invertible means
  :Def29:
  x is right_invertible left_invertible;
end;

registration
  let M be multLoopStr;
  cluster right_invertible left_invertible -> invertible Element of M;
  coherence by Def29;
  cluster invertible -> right_invertible left_invertible Element of M;
  coherence by Def29;
end;

definition
  let M be multLoopStr, x be Element of M;
  assume
A1: x is left_invertible right_mult-cancelable;
  func /x -> Element of M means

  it * x = 1.M;
  existence by A1,Def27;
  uniqueness by A1,Def21;
end;

definition
  let M be multLoopStr;
  attr M is left_invertible means
  :Def31:
  for x being Element of M holds x is left_invertible;
  attr M is right_invertible means
  :Def32:
  for x being Element of M holds x is right_invertible;
end;

definition
  let M be multLoopStr;
  attr M is invertible means
  :Def33:
  M is right_invertible left_invertible;
end;

registration
  cluster right_invertible left_invertible -> invertible multLoopStr;
  coherence by Def33;
  cluster invertible -> right_invertible left_invertible multLoopStr;
  coherence by Def33;
end;

registration
  cluster Trivial-multLoopStr -> invertible;
  coherence
  proof
    set M = Trivial-multLoopStr;
    thus M is right_invertible
    proof
      let x be Element of M;
      take x;
      thus thesis by STRUCT_0:def 10;
    end;
    let x being Element of M;
    take x;
    thus thesis by STRUCT_0:def 10;
  end;
end;

registration
  cluster invertible mult-cancelable strict non empty trivial multLoopStr;
  existence
  proof
    take T = Trivial-multLoopStr;
    thus thesis;
  end;
end;

registration
  let M be left_invertible multLoopStr;
  cluster -> left_invertible Element of M;
  coherence by Def31;
end;

registration
  let M be right_invertible multLoopStr;
  cluster -> right_invertible Element of M;
  coherence by Def32;
end;

begin :: Almost

definition
  struct (multLoopStr,ZeroOneStr) multLoopStr_0 (# carrier -> set,
    multF -> BinOp of the carrier, ZeroF, OneF -> Element of the carrier #);
end;

registration
  let D,o,d,e;
  cluster multLoopStr_0(#D,o,d,e#) -> non empty;
  coherence by STRUCT_0:def 1;
end;

registration
  let T,f,s,t;
  cluster multLoopStr_0(#T,f,s,t#) -> trivial;
  coherence by STRUCT_0:def 9;
end;

registration
  let N,b,m,n;
  cluster multLoopStr_0(#N,b,m,n#) -> non trivial;
  coherence by STRUCT_0:def 9;
end;

definition
  func Trivial-multLoopStr_0 -> multLoopStr_0 equals
  multLoopStr_0(#1, op2, op0, op0 #);
  coherence;
end;

registration
  cluster Trivial-multLoopStr_0 -> strict non empty trivial;
  coherence by CARD_1:87,STRUCT_0:def 9;
end;

registration
  cluster strict non empty trivial multLoopStr_0;
  existence
  proof
    take Trivial-multLoopStr_0;
    thus thesis;
  end;
end;

definition
  let M be multLoopStr_0, x be Element of M;
  func x" -> Element of M means
  it * x = 1.M if x is left_invertible right_mult-cancelable
  otherwise it = 0.M;
  existence by Def27;
  uniqueness by Def21;
  consistency;
end;

definition
  let M be multLoopStr_0;
  attr M is almost_left_cancelable means

  for x being Element of M st x <> 0.M
  holds x is left_mult-cancelable;
  attr M is almost_right_cancelable means

  for x being Element of M st x <> 0.M
  holds x is right_mult-cancelable;
end;

definition
  let M be multLoopStr_0;
  attr M is almost_cancelable means
  :Def38:
  M is almost_left_cancelable almost_right_cancelable;
end;

registration
  cluster almost_right_cancelable almost_left_cancelable
    -> almost_cancelable multLoopStr_0;
  coherence by Def38;
  cluster almost_cancelable
    -> almost_right_cancelable almost_left_cancelable multLoopStr_0;
  coherence by Def38;
end;

registration
  cluster Trivial-multLoopStr_0 -> almost_cancelable;
  coherence
  proof
    set M = Trivial-multLoopStr_0;
    thus M is almost_left_cancelable
    proof
      let x be Element of M;
      assume x <> 0.M;
      let y,z be Element of M;
      assume x*y = x*z;
      thus y = z by STRUCT_0:def 10;
    end;
    let x be Element of M;
    assume x <> 0.M;
    let y,z being Element of M;
    assume y*x = z*x;
    thus y = z by STRUCT_0:def 10;
  end;
end;

registration
  cluster almost_cancelable strict non empty trivial multLoopStr_0;
  existence
  proof
    take Trivial-multLoopStr_0;
    thus thesis;
  end;
end;

definition
  let M be multLoopStr_0;
  attr M is almost_left_invertible means
  for x being Element of M st x <> 0.M holds x is left_invertible;
  attr M is almost_right_invertible means
  for x being Element of M st x <> 0.M holds x is right_invertible;
end;

definition
  let M be multLoopStr_0;
  attr M is almost_invertible means
  :Def41:
  M is almost_right_invertible almost_left_invertible;
end;

registration
  cluster almost_right_invertible almost_left_invertible
    -> almost_invertible multLoopStr_0;
  coherence by Def41;
  cluster almost_invertible
    -> almost_right_invertible almost_left_invertible multLoopStr_0;
  coherence by Def41;
end;

registration
  cluster Trivial-multLoopStr_0 -> almost_invertible;
  coherence
  proof
    set M = Trivial-multLoopStr_0;
    thus M is almost_right_invertible
    proof
      let x be Element of M;
      assume x <> 0.M;
      take x;
      thus thesis by STRUCT_0:def 10;
    end;
    let x being Element of M;
    assume x <> 0.M;
    take x;
    thus thesis by STRUCT_0:def 10;
  end;
end;

registration
  cluster almost_invertible almost_cancelable
    strict non empty trivial multLoopStr_0;
  existence
  proof
    take T = Trivial-multLoopStr_0;
    thus thesis;
  end;
end;

begin :: Double

definition
  struct(addLoopStr,multLoopStr_0) doubleLoopStr (# carrier -> set,
    addF, multF -> BinOp of the carrier,
    OneF, ZeroF -> Element of the carrier #);
end;

registration
  let D,o,o1,d,e;
  cluster doubleLoopStr(#D,o,o1,d,e#) -> non empty;
  coherence by STRUCT_0:def 1;
end;

registration
  let T,f,f1,s,t;
  cluster doubleLoopStr(#T,f,f1,s,t#) -> trivial;
  coherence by STRUCT_0:def 9;
end;

registration
  let N,b,b1,m,n;
  cluster doubleLoopStr(#N,b,b1,m,n#) -> non trivial;
  coherence by STRUCT_0:def 9;
end;

definition
  func Trivial-doubleLoopStr -> doubleLoopStr equals
  doubleLoopStr(#1, op2, op2, op0, op0 #);
  coherence;
end;

registration
  cluster Trivial-doubleLoopStr -> strict non empty trivial;
  coherence by CARD_1:87,STRUCT_0:def 9;
end;

registration
  cluster strict non empty trivial doubleLoopStr;
  existence
  proof
    take Trivial-doubleLoopStr;
    thus thesis;
  end;
end;