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

begin

definition

let f be Function;
let a, b be set ;
func f . (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 func f . (a,b) -> Element of C;
coherence
f . (a,b) is Element of C

proof end;

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

proof end;

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

proof end;

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;

scheme :: BINOP_1:sch 1
FuncEx2{ F₁() -> set , F₂() -> set , F₃() -> set , P₁[ set , set , set ] } :

ex f being Function of [:F₁(),F₂():],F₃() st
for x, y being set st x in F₁() & y in F₂() holds
P₁[x,y,f . (x,y)]

provided

A1: for x, y being set st x in F₁() & y in F₂() holds
ex z being set st
( z in F₃() & P₁[x,y,z] )

proof end;

scheme :: BINOP_1:sch 2
Lambda2{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( set , set ) -> set } :

ex f being Function of [:F₁(),F₂():],F₃() st
for x, y being set st x in F₁() & y in F₂() holds
f . (x,y) = F₄(x,y)

provided

A1: for x, y being set st x in F₁() & y in F₂() holds
F₄(x,y) in F₃()

proof end;

scheme :: BINOP_1:sch 3
FuncEx2D{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , P₁[ set , set , set ] } :

ex f being Function of [:F₁(),F₂():],F₃() st
for x being Element of F₁()
for y being Element of F₂() holds P₁[x,y,f . (x,y)]

provided

A1: for x being Element of F₁()
for y being Element of F₂() ex z being Element of F₃() st P₁[x,y,z]

proof end;

scheme :: BINOP_1:sch 4
Lambda2D{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( Element of F₁(), Element of F₂()) -> Element of F₃() } :

ex f being Function of [:F₁(),F₂():],F₃() st
for x being Element of F₁()
for y being Element of F₂() holds f . (x,y) = F₄(x,y)

proof end;

definition

let A be set ;
let o be BinOp of A;
attr o is commutative means :Def2: :: BINOP_1:def 2
for a, b being Element of A holds o . (a,b) = o . (b,a);
attr o is associative means :Def3: :: BINOP_1:def 3
for a, b, c being Element of A holds o . (a,(o . (b,c))) = o . ((o . (a,b)),c);
attr o is idempotent means :Def4: :: 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 Def3 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 Def4 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 V15([:{},{}:], {} ) -> empty commutative associative Element of bool [:[:{},{}:],{}:];
coherence
for b₁ being BinOp of {} holds
( b₁ is empty & b₁ is associative & b₁ is commutative )

proof end;

end;

definition

let A be set ;
let e be Element of A;
let o be BinOp of A;
pred e is_a_left_unity_wrt o means :Def5: :: BINOP_1:def 5
for a being Element of A holds o . (e,a) = a;
pred e 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;
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;

:: 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 :: BINOP_1:3

canceled;

theorem :: BINOP_1:4

canceled;

theorem :: BINOP_1:5

canceled;

theorem :: BINOP_1:6

canceled;

theorem :: BINOP_1:7

canceled;

theorem :: BINOP_1:8

canceled;

theorem :: BINOP_1:9

canceled;

theorem :: BINOP_1:10

canceled;

theorem Th11: :: BINOP_1:11

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 ) )

proof end;

theorem Th12: :: BINOP_1:12

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 )

proof end;

theorem Th13: :: BINOP_1:13

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 )

proof end;

theorem Th14: :: BINOP_1:14

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 )

proof end;

theorem Th15: :: BINOP_1:15

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 )

proof end;

theorem :: BINOP_1:16

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 )

proof end;

theorem Th17: :: BINOP_1:17

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

proof end;

theorem Th18: :: BINOP_1:18

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

proof end;

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 b₁ being Element of A st b₁ is_a_unity_wrt o by A1;
uniqueness
for b₁, b₂ being Element of A st b₁ is_a_unity_wrt o & b₂ is_a_unity_wrt o holds
b₁ = b₂ by Th18;

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 b₃ being Element of A holds
( b₃ = the_unity_wrt o iff b₃ is_a_unity_wrt o );

definition

let A be set ;
let o9, o be BinOp of A;
pred o9 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)));
pred o9 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;
pred o9 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 :: BINOP_1:19

canceled;

theorem :: BINOP_1:20

canceled;

theorem :: BINOP_1:21

canceled;

theorem :: BINOP_1:22

canceled;

theorem Th23: :: BINOP_1:23

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))) ) )

proof end;

theorem Th24: :: BINOP_1:24

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))) )

proof end;

theorem Th25: :: BINOP_1:25

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))) )

proof end;

theorem Th26: :: BINOP_1:26

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 )

proof end;

theorem Th27: :: BINOP_1:27

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 )

proof end;

theorem :: BINOP_1:28

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 )

proof end;

definition

let A be set ;
let u be UnOp of A;
let o be BinOp of A;
pred u 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 ;
let 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);
correctness
compatibility
( o is commutative iff for a, b being Element of A holds o . (a,b) = o . (b,a) );
by Def2;
redefine 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);
correctness
compatibility
( o is associative iff for a, b, c being Element of A holds o . (a,(o . (b,c))) = o . ((o . (a,b)),c) );
by Def3;
redefine attr o is idempotent means :: BINOP_1:def 15
for a being Element of A holds o . (a,a) = a;
correctness
compatibility
( o is idempotent iff for a being Element of A holds o . (a,a) = a );
by Def4;

end;

:: deftheorem defines commutative BINOP_1:def 13 :
for A being non empty 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 14 :
for A being non empty 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 15 :
for A being non empty set
for o being BinOp of A holds
( o is idempotent iff for a being Element of A holds o . (a,a) = a );

definition

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 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)) );

theorem :: BINOP_1:29

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

proof end;

theorem :: BINOP_1:30

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

proof end;

theorem :: BINOP_1:31

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 & x2 in X & y1 in Y & y2 in Y holds
f . (x1,y1) = f . (x2,y2) )

proof end;

theorem :: BINOP_1:32

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

proof end;

scheme :: BINOP_1:sch 5
PartFuncEx2{ F₁() -> set , F₂() -> set , F₃() -> set , P₁[ set , set , set ] } :

ex f being PartFunc of [:F₁(),F₂():],F₃() st
( ( for x, y being set holds
( [x,y] in dom f iff ( x in F₁() & y in F₂() & ex z being set st P₁[x,y,z] ) ) ) & ( for x, y being set st [x,y] in dom f holds
P₁[x,y,f . (x,y)] ) )

provided

A1: for x, y, z being set st x in F₁() & y in F₂() & P₁[x,y,z] holds
z in F₃() and
A2: for x, y, z1, z2 being set st x in F₁() & y in F₂() & P₁[x,y,z1] & P₁[x,y,z2] holds
z1 = z2

proof end;

scheme :: BINOP_1:sch 6
LambdaR2{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( set , set ) -> set , P₁[ set , set ] } :

ex f being PartFunc of [:F₁(),F₂():],F₃() st
( ( for x, y being set holds
( [x,y] in dom f iff ( x in F₁() & y in F₂() & P₁[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds
f . (x,y) = F₄(x,y) ) )

provided

A1: for x, y being set st P₁[x,y] holds
F₄(x,y) in F₃()

proof end;

scheme :: BINOP_1:sch 7
PartLambda2{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( set , set ) -> set , P₁[ set , set ] } :

ex f being PartFunc of [:F₁(),F₂():],F₃() st
( ( for x, y being set holds
( [x,y] in dom f iff ( x in F₁() & y in F₂() & P₁[x,y] ) ) ) & ( for x, y being set st [x,y] in dom f holds
f . (x,y) = F₄(x,y) ) )

provided

A1: for x, y being set st x in F₁() & y in F₂() & P₁[x,y] holds
F₄(x,y) in F₃()

proof end;

scheme :: BINOP_1:sch 8
Sch8{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> set , F₄( set , set ) -> set , P₁[ set , set ] } :

ex f being PartFunc of [:F₁(),F₂():],F₃() st
( ( for x being Element of F₁()
for y being Element of F₂() holds
( [x,y] in dom f iff P₁[x,y] ) ) & ( for x being Element of F₁()
for y being Element of F₂() st [x,y] in dom f holds
f . (x,y) = F₄(x,y) ) )

provided

A1: for x being Element of F₁()
for y being Element of F₂() st P₁[x,y] holds
F₄(x,y) in F₃()

proof end;

definition

let A be set ;
let f be BinOp of A;
let x, y be Element of A;
:: original: .
redefine func f . (x,y) -> Element of A;
coherence
f . (x,y) is Element of A

proof end;

end;

definition

let X, Y, Z be set ;
let f1, f2 be Function of [:X,Y:],Z;
:: original: =
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);
compatibility
( f1 = f2 iff for x, y being set st x in X & 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 & y in Y holds
f1 . (x,y) = f2 . (x,y) );