The abstract of the Mizar article:

Binary Operations

by

Czeslaw Bylinski

Received April 14, 1989

MML identifier: BINOP_1

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, BOOLE, RELAT_1, BINOP_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2;
 constructors TARSKI, FUNCT_2, XBOOLE_0;
 clusters RELSET_1, SUBSET_1, XBOOLE_0, ZFMISC_1;
 requirements SUBSET, BOOLE;


begin

definition let f be Function; let a,b be set;
  func f.(a,b) -> set equals
:: BINOP_1:def 1
  f.[a,b];
end;

reserve A for set;

definition let A,B be non empty set, C be set, f be Function of [:A,B:],C;
  let a be Element of A; let b be Element of B;
redefine func f.(a,b) -> Element of C;
end;

canceled;

theorem :: BINOP_1:2
   for A,B,C be non empty set
  for f1,f2 being Function of [:A,B:],C st
    for a being Element of A for b being Element of B holds f1.(a,b) = f2.(a,b)
   holds f1 = f2;

definition let A be set;
 mode UnOp of A is Function of A,A;
 mode BinOp of A is Function of [:A,A:],A;
end;

reserve u for UnOp of A,
        o,o' for BinOp of A,
        a,b,c,e,e1,e2 for Element of A;

scheme BinOpEx{A()->non empty set,
               P[Element of A(),Element of A(),Element of A()]}:
 ex o being BinOp of A() st
    for a,b being Element of A() holds P[a,b,o.(a,b)]
provided
 for x,y being Element of A() ex z being Element of A() st P[x,y,z];

scheme BinOpLambda{A()->non empty set,
                   O(Element of A(),Element of A())->Element of A()}:
 ex o being BinOp of A() st
    for a,b being Element of A() holds o.(a,b) = O(a,b);

definition let A,o;
  attr o is commutative means
:: BINOP_1:def 2

   for a,b holds o.(a,b) = o.(b,a);
  attr o is associative means
:: BINOP_1:def 3

   for a,b,c holds o.(a,o.(b,c)) = o.(o.(a,b),c);
  attr o is idempotent means
:: BINOP_1:def 4

   for a holds o.(a,a) = a;
end;

definition
 cluster -> empty associative commutative BinOp of {};
end;

definition let A,e,o;
  pred e is_a_left_unity_wrt o means
:: BINOP_1:def 5

   for a holds o.(e,a) = a;
  pred e is_a_right_unity_wrt o means
:: BINOP_1:def 6

   for a holds o.(a,e) = a;
end;

definition let A,e,o;
  pred e is_a_unity_wrt o means
:: BINOP_1:def 7
     e is_a_left_unity_wrt o & e is_a_right_unity_wrt o;
end;

canceled 8;

theorem :: BINOP_1:11
   e is_a_unity_wrt o iff for a holds o.(e,a) = a & o.(a,e) = a;

theorem :: BINOP_1:12
   o is commutative implies
    (e is_a_unity_wrt o iff for a holds o.(e,a) = a);

theorem :: BINOP_1:13
   o is commutative implies
    (e is_a_unity_wrt o iff for a holds o.(a,e) = a);

theorem :: BINOP_1:14
   o is commutative implies
    (e is_a_unity_wrt o iff e is_a_left_unity_wrt o);

theorem :: BINOP_1:15
   o is commutative implies
    (e is_a_unity_wrt o iff e is_a_right_unity_wrt o);

theorem :: BINOP_1:16
     o is commutative implies
    (e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o);

theorem :: BINOP_1:17
   e1 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o implies e1 = e2;

theorem :: BINOP_1:18
   e1 is_a_unity_wrt o & e2 is_a_unity_wrt o implies e1 = e2;

definition let A,o;
 assume
  ex e st e is_a_unity_wrt o;
  func the_unity_wrt o -> Element of A means
:: BINOP_1:def 8
   it is_a_unity_wrt o;
end;

definition let A,o',o;
  pred o' is_left_distributive_wrt o means
:: BINOP_1:def 9

    for a,b,c holds o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c));
  pred o' is_right_distributive_wrt o means
:: BINOP_1:def 10

    for a,b,c holds o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c));
end;

definition
  let A,o',o;
  pred o' is_distributive_wrt o means
:: BINOP_1:def 11
      o' is_left_distributive_wrt o & o' is_right_distributive_wrt o;
end;

canceled 4;

theorem :: BINOP_1:23
   o' is_distributive_wrt o iff
    for a,b,c holds
     o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c)) &
       o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c));

theorem :: BINOP_1:24
 for A being non empty set, o,o' being BinOp of A holds
   o' is commutative implies
    (o' is_distributive_wrt o iff
     for a,b,c being Element of A holds o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c)))
;

theorem :: BINOP_1:25
 for A being non empty set, o,o' being BinOp of A holds
   o' is commutative implies
    (o' is_distributive_wrt o iff
     for a,b,c being Element of A holds o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c)))
;

theorem :: BINOP_1:26
 for A being non empty set, o,o' being BinOp of A holds
   o' is commutative implies
    (o' is_distributive_wrt o iff o' is_left_distributive_wrt o);

theorem :: BINOP_1:27
 for A being non empty set, o,o' being BinOp of A holds
   o' is commutative implies
    (o' is_distributive_wrt o iff o' is_right_distributive_wrt o);

theorem :: BINOP_1:28
   for A being non empty set, o,o' being BinOp of A holds
   o' is commutative implies
    (o' is_right_distributive_wrt o iff o' is_left_distributive_wrt o);

definition let A,u,o;
  pred u is_distributive_wrt o means
:: BINOP_1:def 12

    for a,b holds u.(o.(a,b)) = o.((u.a),(u.b));
end;

definition let A be non empty set, o be BinOp of A;
 redefine
  attr o is commutative means
:: BINOP_1:def 13
     for a,b being Element of A holds o.(a,b) = o.(b,a);
  attr o is associative means
:: BINOP_1:def 14
     for a,b,c being Element of A holds o.(a,o.(b,c)) = o.(o.(a,b),c);
  attr o is idempotent means
:: BINOP_1:def 15
     for a being Element of A holds o.(a,a) = a;
end;

definition let A be non empty set, e be Element of A, o be BinOp of A;
 redefine
  pred e is_a_left_unity_wrt o means
:: BINOP_1:def 16
     for a being Element of A holds o.(e,a) = a;
  pred e is_a_right_unity_wrt o means
:: BINOP_1:def 17
     for a being Element of A holds o.(a,e) = a;
end;

definition let A be non empty set, o',o be BinOp of A;
 redefine
  pred o' is_left_distributive_wrt o means
:: BINOP_1:def 18
      for a,b,c being Element of A holds o'.(a,o.(b,c)) = o.(o'.(a,b),o'.(a,c))
;
  pred o' is_right_distributive_wrt o means
:: BINOP_1:def 19
      for a,b,c being Element of A holds o'.(o.(a,b),c) = o.(o'.(a,c),o'.(b,c))
;
end;

definition let A be non empty set, u be UnOp of A, o be BinOp of A;
 redefine
  pred u is_distributive_wrt o means
:: BINOP_1:def 20
      for a,b being Element of A holds u.(o.(a,b)) = o.((u.a),(u.b));
end;