Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Binary Operations

by
Czeslaw Bylinski

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;

```