:: BINOP_1 semantic presentation

definition

let f be Function;
let a, b be set ;
func f . a,b -> set equals :: BINOP_1:def 1
f . [a,b];
correctness ;

end;

:: deftheorem defines . BINOP_1:def 1 :

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

proof end;

end;

theorem :: BINOP_1:1

canceled;

theorem :: BINOP_1:2

for A, B, C being 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

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
BinOpEx{ F₁() -> non empty set , P₁[ Element of F₁(), Element of F₁(), Element of F₁()] } :

ex o being BinOp of F₁() st
for a, b being Element of F₁() holds P₁[a,b,o . a,b]

provided

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

proof end;

scheme :: BINOP_1:sch 2
BinOpLambda{ F₁() -> non empty set , F₂( Element of F₁(), Element of F₁()) -> Element of F₁() } :

ex o being BinOp of F₁() st
for a, b being Element of F₁() holds o . a,b = F₂(a,b)

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 :

:: deftheorem Def3 defines associative BINOP_1:def 3 :

:: deftheorem Def4 defines idempotent BINOP_1:def 4 :

registration

cluster -> empty commutative associative M4([:{} ,{} :], {} );
coherence

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 :

:: deftheorem Def6 defines is_a_right_unity_wrt BINOP_1:def 6 :

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 :

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 by A1;
uniqueness by Th18;

end;

:: deftheorem defines the_unity_wrt BINOP_1:def 8 :

definition

let A be set ;
let o', o be BinOp of A;
pred o' is_left_distributive_wrt o means :Def9: :: BINOP_1:def 9
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 :Def10: :: BINOP_1:def 10
for a, b, c being Element of A holds o' . (o . a,b),c = o . (o' . a,c),(o' . b,c);

end;

:: deftheorem Def9 defines is_left_distributive_wrt BINOP_1:def 9 :

:: deftheorem Def10 defines is_right_distributive_wrt BINOP_1:def 10 :

definition

let A be set ;
let o', o be BinOp of A;
pred o' is_distributive_wrt o means :: BINOP_1:def 11
( o' is_left_distributive_wrt o & o' is_right_distributive_wrt o );

end;

:: deftheorem defines is_distributive_wrt BINOP_1:def 11 :

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 o', o being BinOp of A holds
( 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) & o' . (o . a,b),c = o . (o' . a,c),(o' . b,c) ) )

proof end;

theorem Th24: :: BINOP_1:24

for A being non empty set
for o, o' being BinOp of A st o' is commutative holds
( 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) )

proof end;

theorem Th25: :: BINOP_1:25

for A being non empty set
for o, o' being BinOp of A st o' is commutative holds
( 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) )

proof end;

theorem Th26: :: BINOP_1:26

for A being non empty set
for o, o' being BinOp of A st o' is commutative holds
( o' is_distributive_wrt o iff o' is_left_distributive_wrt o )

proof end;

theorem Th27: :: BINOP_1:27

for A being non empty set
for o, o' being BinOp of A st o' is commutative holds
( o' is_distributive_wrt o iff o' is_right_distributive_wrt o )

proof end;

theorem :: BINOP_1:28

for A being non empty set
for o, o' being BinOp of A st o' is commutative holds
( o' is_right_distributive_wrt o iff o' 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 :

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 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 by Def3;
redefine attr o is idempotent means :: BINOP_1:def 15
for a being Element of A holds o . a,a = a;
correctness by Def4;

end;

:: deftheorem defines commutative BINOP_1:def 13 :

:: deftheorem defines associative BINOP_1:def 14 :

:: deftheorem defines idempotent BINOP_1:def 15 :

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 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 by Def6;

end;

:: deftheorem defines is_a_left_unity_wrt BINOP_1:def 16 :

:: deftheorem defines is_a_right_unity_wrt BINOP_1:def 17 :

definition

let A be non empty set ;
let 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);
correctness by Def9;
redefine 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);
correctness by Def10;

end;

:: deftheorem defines is_left_distributive_wrt BINOP_1:def 18 :

:: deftheorem defines is_right_distributive_wrt BINOP_1:def 19 :

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 by Def12;

end;

:: deftheorem defines is_distributive_wrt BINOP_1:def 20 :