:: Binary Operations
:: by Czes{\l}aw Byli\'nski
::
:: Received April 14, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
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 object;
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 for set,x,x1,x2,y,y1,y2,z,z1,z2 for object;
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[object,object,object]}:
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(object,object)->object}:
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[object,object,object]}:
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 for BinOp of {};
end;
definition
let A; let e be object; let 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; let e be object; let 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;
theorem :: BINOP_1:3
e is_a_unity_wrt o iff for a holds o.(e,a) = a & o.(a,e) = a;
theorem :: BINOP_1:4
o is commutative implies (e is_a_unity_wrt o iff for a holds o.( e,a) = a);
theorem :: BINOP_1:5
o is commutative implies (e is_a_unity_wrt o iff for a holds o.( a,e) = a);
theorem :: BINOP_1:6
o is commutative implies (e is_a_unity_wrt o iff e is_a_left_unity_wrt o);
theorem :: BINOP_1:7
o is commutative implies (e is_a_unity_wrt o iff e is_a_right_unity_wrt o);
theorem :: BINOP_1:8
o is commutative implies (e is_a_left_unity_wrt o iff e
is_a_right_unity_wrt o);
theorem :: BINOP_1:9
e1 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o implies e1 = e2;
theorem :: BINOP_1:10
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;
theorem :: BINOP_1:11
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:12
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:13
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:14
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:15
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:16
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
::$CD 3
let A be non empty set, e be object, 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;
redefine 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));
redefine 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:17
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:18
for x, y being object, 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:19
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:20
for f1,f2 being PartFunc of [:X,Y:],Z st dom f1 = dom f2 &
for x,y being object 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[object,object,object]}:
ex f being PartFunc of [:X(),Y():],Z() st
(for x,y being object holds [x,y] in dom f iff x in X() & y in Y() &
ex z being object st P[x,y,z]) &
for x,y being object st [x,y] in dom f holds P[x,y,f.(x,y)]
provided
for x,y,z being object st x in X() & y in Y() & P[x,y,z]
holds z in Z() and
for x,y,z1,z2 being object 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(object,object)->object, P[object,object]}:
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(object,object)->object, P[object,object]}:
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(object,object)->object, P[object,object]}:
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();
definition
let A be set, f be BinOp of A;
let a,b be Element of A;
redefine func f.(a,b) -> Element of A;
end;
definition
let X,Y,Z be set; let f1,f2 being Function of [:X,Y:],Z;
redefine pred f1 = f2 means
:: BINOP_1:def 21
for x,y being set st x in X & y in Y holds f1.(x,y) = f2.(x,y);
end;
scheme :: BINOP_1:sch 9
{X, Y, Z() -> set, P[object,object,object]}:
ex f being Function of [:X(),Y():],Z() st
for x,y being set st x in X() & y in Y() holds P[x,y,f.(x,y)]
provided
for x,y being set st x in X() & y in Y()
ex z being set st z in Z() & P[x,y,z];