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


begin

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

:: deftheorem  defines . BINOP_1:def_1_:_
 for f being Function
for a, b being set holds f . (a,b) = f . [a,b];

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

theorem Th1: :: 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
proofend;

theorem :: BINOP_1:2
for X, Y, Z being set
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
proofend;

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;

definition
let A be set ;
let f be BinOp of A;
let a, b be Element of A;
:: original:.
redefine funcf . (a,b) ->  Element of A;
coherence
 f . (a,b) is Element of A
proofend;
end;

scheme :: BINOP_1:sch 1
FuncEx2{ F1() ->  set , F2() ->  set , F3() ->  set , P1[ set , set , set ] } :
 ex f being Function of [:F1(),F2():],F3() st
for x, y being set st x in F1() & y in F2() holds
P1[x,y,f . (x,y)]
provided
A1: for x, y being set st x in F1() & y in F2() holds
ex z being set st
( z in F3() & P1[x,y,z] )
proofend;

scheme :: BINOP_1:sch 2
Lambda2{ F1() ->  set , F2() ->  set , F3() ->  set , F4( set , set ) ->  set } :
 ex f being Function of [:F1(),F2():],F3() st
for x, y being set st x in F1() & y in F2() holds
f . (x,y) = F4(x,y)
provided
A1: for x, y being set st x in F1() & y in F2() holds
F4(x,y) in F3()
proofend;

scheme :: BINOP_1:sch 3
FuncEx2D{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  non empty set , P1[ set , set , set ] } :
 ex f being Function of [:F1(),F2():],F3() st
for x being Element of F1()
for y being Element of F2() holds P1[x,y,f . (x,y)]
provided
A1: for x being Element of F1()
for y being Element of F2() ex z being Element of F3() st P1[x,y,z]
proofend;

scheme :: BINOP_1:sch 4
Lambda2D{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  non empty set , F4( Element of F1(), Element of F2()) ->  Element of F3() } :
 ex f being Function of [:F1(),F2():],F3() st
for x being Element of F1()
for y being Element of F2() holds f . (x,y) = F4(x,y)
proofend;

definition
let A be set ;
let o be BinOp of A;
attro is commutative  means :Def2: :: BINOP_1:def 2
 for a, b being Element of A holds o . (a,b) = o . (b,a);
attro is associative  means :: BINOP_1:def 3
 for a, b, c being Element of A holds o . (a,(o . (b,c))) = o . ((o . (a,b)),c);
attro is idempotent  means :: BINOP_1:def 4
 for a being Element of A holds o . (a,a) = a;
end;

:: deftheorem Def2 defines commutative BINOP_1:def_2_:_
 for A being set
for o being BinOp of A holds
( o is commutative iff for a, b being Element of A holds o . (a,b) = o . (b,a) );

:: deftheorem  defines associative BINOP_1:def_3_:_
 for A being set
for o being BinOp of A holds
( o is associative iff for a, b, c being Element of A holds o . (a,(o . (b,c))) = o . ((o . (a,b)),c) );

:: deftheorem  defines idempotent BINOP_1:def_4_:_
 for A being set
for o being BinOp of A holds
( o is idempotent iff for a being Element of A holds o . (a,a) = a );

registration
cluster Function-like V18([:{},{}:], {} )  ->  empty commutative associative for Element of bool [:[:{},{}:],{}:];
coherence
 for b1 being BinOp of {} holds
( b1 is empty & b1 is associative & b1 is commutative )
proofend;
end;

definition
let A be set ;
let e be Element of A;
let o be BinOp of A;
prede is_a_left_unity_wrt o means :Def5: :: BINOP_1:def 5
 for a being Element of A holds o . (e,a) = a;
prede is_a_right_unity_wrt o means :Def6: :: BINOP_1:def 6
 for a being Element of A holds o . (a,e) = a;
end;

:: deftheorem Def5 defines is_a_left_unity_wrt BINOP_1:def_5_:_
 for A being set
for e being Element of A
for o being BinOp of A holds
( e is_a_left_unity_wrt o iff for a being Element of A holds o . (e,a) = a );

:: deftheorem Def6 defines is_a_right_unity_wrt BINOP_1:def_6_:_
 for A being set
for e being Element of A
for o being BinOp of A holds
( e is_a_right_unity_wrt o iff for a being Element of A holds o . (a,e) = a );

definition
let A be set ;
let e be Element of A;
let o be BinOp of A;
prede 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;

:: deftheorem  defines is_a_unity_wrt BINOP_1:def_7_:_
 for A being set
for e being Element of A
for o being BinOp of A holds
( e is_a_unity_wrt o iff ( e is_a_left_unity_wrt o & e is_a_right_unity_wrt o ) );

theorem Th3: :: BINOP_1:3
for A being set
for o being BinOp of A
for e being Element of A holds
( e is_a_unity_wrt o iff for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a ) )
proofend;

theorem Th4: :: BINOP_1:4
for A being set
for o being BinOp of A
for e being Element of A st o is commutative holds
( e is_a_unity_wrt o iff for a being Element of A holds o . (e,a) = a )
proofend;

theorem Th5: :: BINOP_1:5
for A being set
for o being BinOp of A
for e being Element of A st o is commutative holds
( e is_a_unity_wrt o iff for a being Element of A holds o . (a,e) = a )
proofend;

theorem Th6: :: BINOP_1:6
for A being set
for o being BinOp of A
for e being Element of A st o is commutative holds
( e is_a_unity_wrt o iff e is_a_left_unity_wrt o )
proofend;

theorem Th7: :: BINOP_1:7
for A being set
for o being BinOp of A
for e being Element of A st o is commutative holds
( e is_a_unity_wrt o iff e is_a_right_unity_wrt o )
proofend;

theorem :: BINOP_1:8
for A being set
for o being BinOp of A
for e being Element of A st o is commutative holds
( e is_a_left_unity_wrt o iff e is_a_right_unity_wrt o )
proofend;

theorem Th9: :: BINOP_1:9
for A being set
for o being BinOp of A
for e1, e2 being Element of A st e1 is_a_left_unity_wrt o & e2 is_a_right_unity_wrt o holds
e1 = e2
proofend;

theorem Th10: :: BINOP_1:10
for A being set
for o being BinOp of A
for e1, e2 being Element of A st e1 is_a_unity_wrt o & e2 is_a_unity_wrt o holds
e1 = e2
proofend;

definition
let A be set ;
let o be BinOp of A;
assume A1: ex e being Element of A 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;
existence
 ex b1 being Element of A st b1 is_a_unity_wrt o by A1;
uniqueness
 for b1, b2 being Element of A st b1 is_a_unity_wrt o & b2 is_a_unity_wrt o holds
b1 = b2 by Th10;
end;

:: deftheorem  defines the_unity_wrt BINOP_1:def_8_:_
 for A being set
for o being BinOp of A st ex e being Element of A st e is_a_unity_wrt o holds
for b3 being Element of A holds
( b3 = the_unity_wrt o iff b3 is_a_unity_wrt o );

definition
let A be set ;
let o9, o be BinOp of A;
predo9 is_left_distributive_wrt o means :Def9: :: BINOP_1:def 9
 for a, b, c being Element of A holds o9 . (a,(o . (b,c))) = o . ((o9 . (a,b)),(o9 . (a,c)));
predo9 is_right_distributive_wrt o means :Def10: :: BINOP_1:def 10
 for a, b, c being Element of A holds o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c)));
end;

:: deftheorem Def9 defines is_left_distributive_wrt BINOP_1:def_9_:_
 for A being set
for o9, o being BinOp of A holds
( o9 is_left_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))) );

:: deftheorem Def10 defines is_right_distributive_wrt BINOP_1:def_10_:_
 for A being set
for o9, o being BinOp of A holds
( o9 is_right_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))) );

definition
let A be set ;
let o9, o be BinOp of A;
predo9 is_distributive_wrt o means :: BINOP_1:def 11
( o9 is_left_distributive_wrt o & o9 is_right_distributive_wrt o );
end;

:: deftheorem  defines is_distributive_wrt BINOP_1:def_11_:_
 for A being set
for o9, o being BinOp of A holds
( o9 is_distributive_wrt o iff ( o9 is_left_distributive_wrt o & o9 is_right_distributive_wrt o ) );

theorem Th11: :: BINOP_1:11
for A being set
for o9, o being BinOp of A holds
( 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))) & o9 . ((o . (a,b)),c) = o . ((o9 . (a,c)),(o9 . (b,c))) ) )
proofend;

theorem Th12: :: BINOP_1:12
for A being non empty set
for o, o9 being BinOp of A st o9 is commutative holds
( 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))) )
proofend;

theorem Th13: :: BINOP_1:13
for A being non empty set
for o, o9 being BinOp of A st o9 is commutative holds
( 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))) )
proofend;

theorem Th14: :: BINOP_1:14
for A being non empty set
for o, o9 being BinOp of A st o9 is commutative holds
( o9 is_distributive_wrt o iff o9 is_left_distributive_wrt o )
proofend;

theorem Th15: :: BINOP_1:15
for A being non empty set
for o, o9 being BinOp of A st o9 is commutative holds
( o9 is_distributive_wrt o iff o9 is_right_distributive_wrt o )
proofend;

theorem :: BINOP_1:16
for A being non empty set
for o, o9 being BinOp of A st o9 is commutative holds
( o9 is_right_distributive_wrt o iff o9 is_left_distributive_wrt o )
proofend;

definition
let A be set ;
let u be UnOp of A;
let o be BinOp of A;
predu is_distributive_wrt o means :Def12: :: BINOP_1:def 12
 for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b));
end;

:: deftheorem Def12 defines is_distributive_wrt BINOP_1:def_12_:_
 for A being set
for u being UnOp of A
for o being BinOp of A holds
( u is_distributive_wrt o iff for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b)) );

:: definition
:: let A be non empty set, o be BinOp of A;
:: redefine attr o is commutative means
:: for a,b being Element of A holds o.(a,b ) = o.(b,a);
:: correctness by Def2;
:: redefine attr o is associative means
:: for a,b,c being Element of A holds o.(a,o.(b,c)) = o.(o.(a,b),c);
:: correctness by Def3;
:: redefine attr o is idempotent means
:: for a being Element of A holds o.(a,a) = a;
:: correctness by Def4;
:: end;
definition
canceled;
canceled;
canceled;
let A be non empty set ;
let e be Element of A;
let 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;
correctness
compatibility
( e is_a_left_unity_wrt o iff for a being Element of A holds o . (e,a) = a );
by Def5;
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;
correctness
compatibility
( e is_a_right_unity_wrt o iff for a being Element of A holds o . (a,e) = a );
by Def6;
end;

:: deftheorem  BINOP_1:def_13_:_
canceled;

:: deftheorem  BINOP_1:def_14_:_
canceled;

:: deftheorem  BINOP_1:def_15_:_
canceled;

:: deftheorem  defines is_a_left_unity_wrt BINOP_1:def_16_:_
 for A being non empty set
for e being Element of A
for o being BinOp of A holds
( e is_a_left_unity_wrt o iff for a being Element of A holds o . (e,a) = a );

:: deftheorem  defines is_a_right_unity_wrt BINOP_1:def_17_:_
 for A being non empty set
for e being Element of A
for o being BinOp of A holds
( e is_a_right_unity_wrt o iff for a being Element of A holds o . (a,e) = a );

definition
let A be non empty set ;
let 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)));
correctness
compatibility
( o9 is_left_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))) );
by Def9;
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)));
correctness
compatibility
( o9 is_right_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))) );
by Def10;
end;

:: deftheorem  defines is_left_distributive_wrt BINOP_1:def_18_:_
 for A being non empty set
for o9, o being BinOp of A holds
( o9 is_left_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))) );

:: deftheorem  defines is_right_distributive_wrt BINOP_1:def_19_:_
 for A being non empty set
for o9, o being BinOp of A holds
( o9 is_right_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))) );

definition
let A be non empty set ;
let u be UnOp of A;
let 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));
correctness
compatibility
( u is_distributive_wrt o iff for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b)) );
by Def12;
end;

:: deftheorem  defines is_distributive_wrt BINOP_1:def_20_:_
 for A being non empty set
for u being UnOp of A
for o being BinOp of A holds
( u is_distributive_wrt o iff for a, b being Element of A holds u . (o . (a,b)) = o . ((u . a),(u . b)) );

:: FUNCT_2, 2005.12.13, A.T.
theorem :: BINOP_1:17
for X, Y, Z, x, y being set
for f being Function of [:X,Y:],Z st x in X &amp; y in Y &amp; Z <> {} holds
f . (x,y) in Z
proofend;

:: from TOPALG_3, 2005.12.14, A.T.
theorem :: BINOP_1:18
for x, y, X, Y, Z being set
for f being Function of [:X,Y:],Z
for g being Function st Z <> {} &amp; x in X &amp; y in Y holds
(g * f) . (x,y) = g . (f . (x,y))
proofend;

:: missing, 2005.12.17, A.T.
theorem :: BINOP_1:19
for X, Y being set
for f being Function st dom f = [:X,Y:] holds
( f is constant iff for x1, x2, y1, y2 being set st x1 in X &amp; x2 in X &amp; y1 in Y &amp; y2 in Y holds
f . (x1,y1) = f . (x2,y2) )
proofend;

:: from PARTFUN1, 2006.12.05, AT
theorem :: BINOP_1:20
for X, Y, Z being set
for f1, f2 being PartFunc of [:X,Y:],Z st dom f1 = dom f2 &amp; ( for x, y being set st [x,y] in dom f1 holds
f1 . (x,y) = f2 . (x,y) ) holds
f1 = f2
proofend;

scheme :: BINOP_1:sch 5
PartFuncEx2{ F1() ->  set , F2() ->  set , F3() ->  set , P1[ set , set , set ] } :
 ex f being PartFunc of [:F1(),F2():],F3() st
( ( for x, y being set holds
( [x,y] in dom f iff ( x in F1() &amp; y in F2() &amp; ex z being set st P1[x,y,z] ) ) ) &amp; ( for x, y being set st [x,y] in dom f holds
P1[x,y,f . (x,y)] ) )
provided
A1: for x, y, z being set st x in F1() &amp; y in F2() &amp; P1[x,y,z] holds
z in F3() and
A2: for x, y, z1, z2 being set st x in F1() &amp; y in F2() &amp; P1[x,y,z1] &amp; P1[x,y,z2] holds
z1 = z2
proofend;

scheme :: BINOP_1:sch 6
LambdaR2{ F1() ->  set , F2() ->  set , F3() ->  set , F4( set , set ) ->  set , P1[ set , set ] } :
 ex f being PartFunc of [:F1(),F2():],F3() st
( ( for x, y being set holds
( [x,y] in dom f iff ( x in F1() &amp; y in F2() &amp; P1[x,y] ) ) ) &amp; ( for x, y being set st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) )
provided
A1: for x, y being set st P1[x,y] holds
F4(x,y) in F3()
proofend;

scheme :: BINOP_1:sch 7
PartLambda2{ F1() ->  set , F2() ->  set , F3() ->  set , F4( set , set ) ->  set , P1[ set , set ] } :
 ex f being PartFunc of [:F1(),F2():],F3() st
( ( for x, y being set holds
( [x,y] in dom f iff ( x in F1() &amp; y in F2() &amp; P1[x,y] ) ) ) &amp; ( for x, y being set st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) )
provided
A1: for x, y being set st x in F1() &amp; y in F2() &amp; P1[x,y] holds
F4(x,y) in F3()
proofend;

scheme :: BINOP_1:sch 8
Sch8{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  set , F4( set , set ) ->  set , P1[ set , set ] } :
 ex f being PartFunc of [:F1(),F2():],F3() st
( ( for x being Element of F1()
for y being Element of F2() holds
( [x,y] in dom f iff P1[x,y] ) ) &amp; ( for x being Element of F1()
for y being Element of F2() st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) )
provided
A1: for x being Element of F1()
for y being Element of F2() st P1[x,y] holds
F4(x,y) in F3()
proofend;

:: 2007.11.22, A.T.
definition
let A be set ;
let f be BinOp of A;
let x, y be Element of A;
:: original:.
redefine funcf . (x,y) ->  Element of A;
coherence
 f . (x,y) is Element of A
proofend;
end;

definition
let X, Y, Z be set ;
let f1, f2 be Function of [:X,Y:],Z;
:: original:=
redefine predf1 = f2 means :: BINOP_1:def 21
 for x, y being set st x in X &amp; y in Y holds
f1 . (x,y) = f2 . (x,y);
compatibility
 ( f1 = f2 iff for x, y being set st x in X &amp; y in Y holds
f1 . (x,y) = f2 . (x,y) ) by Th1;
end;

:: deftheorem  defines = BINOP_1:def_21_:_
 for X, Y, Z being set
for f1, f2 being Function of [:X,Y:],Z holds
( f1 = f2 iff for x, y being set st x in X &amp; y in Y holds
f1 . (x,y) = f2 . (x,y) );