:: Binary Operations
::  by Czes{\l}aw Byli\'nski
::
:: Received April 14, 1989
:: Copyright (c) 1990 Association of Mizar Users

environ

 vocabularies FUNCT_1, XBOOLE_0, ZFMISC_1, SUBSET_1, TARSKI, RELAT_1, PARTFUN1,
      BINOP_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, FUNCT_2;
 constructors FUNCT_2, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_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;

reserve X,Y,Z,x,x1,x2,y,y1,y2,z,z1,z2 for set;

theorem :: BINOP_1:1
  for X,Y,Z being set for f1,f2 being Function of [:X,Y:],Z st for
  x,y being set st x in X & y in Y holds f1.(x,y) = f2.(x,y) holds f1 = f2;

theorem :: BINOP_1:2
  for f1,f2 being Function of [:X,Y:],Z st for a being Element of X for
  b being Element of Y 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,o9 for BinOp of A,
  a,b,c,e,e1,e2 for Element of A;

scheme :: BINOP_1:sch 1

  FuncEx2{X, Y, Z() -> set, P[set,set,set]}: ex f being Function of [:X(),Y()
  :],Z() st for x,y st x in X() & y in Y() holds P[x,y,f.(x,y)]
provided
 for x,y st x in X() & y in Y() ex z st z in Z() & P[x,y,z];

scheme :: BINOP_1:sch 2

  Lambda2{X, Y, Z() -> set, F(set,set)->set}: ex f being Function of [:X(),Y()
  :],Z() st for x,y st x in X() & y in Y() holds f.(x,y) = F(x,y)
provided
 for x,y st x in X() & y in Y() holds F(x,y) in Z();

scheme :: BINOP_1:sch 3

  FuncEx2D{X, Y, Z() -> non empty set, P[set,set,set]}: ex f being Function of
[:X(),Y():],Z() st for x being Element of X() for y being Element of Y() holds
  P[x,y,f.(x,y)]
provided
 for x being Element of X() for y being Element of Y() ex z being
Element of Z() st P[x,y,z];

scheme :: BINOP_1:sch 4

  Lambda2D{X, Y, Z() -> non empty set, F(Element of X(),Element of Y()) ->
Element of Z()}: ex f being Function of [:X(),Y():],Z() st for x being Element
  of X() for y being Element of Y() holds f.(x,y)=F(x,y);

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;

registration
  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,o9,o;
  pred o9 is_left_distributive_wrt o means
:: BINOP_1:def 9

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

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

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

canceled 4;

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

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

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

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

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

theorem :: BINOP_1:28
  for A being non empty set, o,o9 being BinOp of A holds o9 is
  commutative implies (o9 is_right_distributive_wrt o iff o9
  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, o9,o be BinOp of A;
  redefine pred o9 is_left_distributive_wrt o means
:: BINOP_1:def 18
  for a,b,c being Element of
  A holds o9.(a,o.(b,c)) = o.(o9.(a,b),o9.(a,c));
  pred o9 is_right_distributive_wrt o means
:: BINOP_1:def 19
  for a,b,c being Element of A holds
  o9.(o.(a,b),c) = o.(o9.(a,c),o9.(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;

:: FUNCT_2, 2005.12.13, A.T.

theorem :: BINOP_1:29
  for f being Function of [:X,Y:],Z st x in X & y in Y & Z <> {} holds f
  .(x,y) in Z;

:: from TOPALG_3, 2005.12.14, A.T.

theorem :: BINOP_1:30
  for x, y, X, Y, Z being set, f being Function of [:X,Y:],Z, g being
  Function st Z <> {} & x in X & y in Y holds (g*f).(x,y) = g.(f.(x,y));

:: missing, 2005.12.17, A.T.

theorem :: BINOP_1:31
  for f being Function st dom f = [:X,Y:] holds f is constant iff for x1
  ,x2,y1,y2 st x1 in X & x2 in X & y1 in Y & y2 in Y holds f.(x1,y1)=f.(x2,y2);

:: from PARTFUN1, 2006.12.05, AT

theorem :: BINOP_1:32
  for f1,f2 being PartFunc of [:X,Y:],Z st dom f1 = dom f2 & for x,y st
  [x,y] in dom f1 holds f1.(x,y)=f2.(x,y) holds f1 = f2;

scheme :: BINOP_1:sch 5

  PartFuncEx2{X,Y,Z()->set,P[set,set,set]}: ex f being PartFunc of [:X(),Y():]
,Z() st (for x,y holds [x,y] in dom f iff x in X() & y in Y() & ex z st P[x,y,z
  ]) & for x,y st [x,y] in dom f holds P[x,y,f.(x,y)]
provided
 for x,y,z st x in X() & y in Y() & P[x,y,z] holds z in Z() and
 for x,y,z1,z2 st x in X() & y in Y() & P[x,y,z1] & P[x,y,z2] holds
z1 = z2;

scheme :: BINOP_1:sch 6

  LambdaR2{X,Y,Z()->set,F(set,set)->set,P[set,set]}: ex f being PartFunc of [:
X(),Y():],Z() st (for x,y holds [x,y] in dom f iff x in X() & y in Y() & P[x,y]
  ) & for x,y st [x,y] in dom f holds f.(x,y) = F(x,y)
provided
 for x,y st P[x,y] holds F(x,y) in Z();

:: from GRCAT_1, 2006.12.05, AT

scheme :: BINOP_1:sch 7

  PartLambda2{X,Y,Z()->set,F(set,set)->set,P[set,set]}: ex f being PartFunc of
[:X(),Y():],Z() st (for x,y holds [x,y] in dom f iff x in X() & y in Y() & P[x,
  y]) & for x,y st [x,y] in dom f holds f.(x,y) = F(x,y)
provided
 for x,y st x in X() & y in Y() & P[x,y] holds F(x,y) in Z();

scheme :: BINOP_1:sch 8

  {X,Y()->non empty set,Z()->set,F(set,set)->set, P[set,set]}: ex f being
PartFunc of [:X(),Y():],Z() st (for x being Element of X(), y being Element of
  Y() holds [x,y] in dom f iff P[x,y]) & for x being Element of X(), y being
  Element of Y() st [x,y] in dom f holds f.(x,y) = F(x,y)
provided
 for x being Element of X(), y being Element of Y() st P[x,y] holds F
(x,y) in Z();

:: 2007.11.22, A.T.

definition
  let A be set, f be BinOp of A, x,y be Element of A;
  redefine func f.(x,y) -> Element of A;
end;