:: Binary Operations :: by Czes{\l}aw Byli\'nski :: :: Received April 14, 1989 :: Copyright (c) 1990-2016 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];