:: BINOP_1 semantic presentation
:: deftheorem Def1 defines . BINOP_1:def 1 :
theorem Th1: :: BINOP_1:1
for b
1, b
2, b
3 being
set for b
4, b
5 being
Function of
[:b1,b2:],b
3 holds
( ( for b
6, b
7 being
set holds
( b
6 in b
1 & b
7 in b
2 implies b
4 . b
6,b
7 = b
5 . b
6,b
7 ) ) implies b
4 = b
5 )
proof
let c
1, c
2, c
3 be
set ;
let c
4, c
5 be
Function of
[:c1,c2:],c
3;
assume E2:
for b
1, b
2 being
set holds
( b
1 in c
1 & b
2 in c
2 implies c
4 . b
1,b
2 = c
5 . b
1,b
2 )
;
for b
1 being
set holds
( b
1 in [:c1,c2:] implies c
4 . b
1 = c
5 . b
1 )
hence
c
4 = c
5
by FUNCT_2:18;
end;
theorem Th2: :: BINOP_1:2
for b
1, b
2, b
3 being
set for b
4, b
5 being
Function of
[:b1,b2:],b
3 holds
( ( for b
6 being
Element of b
1for b
7 being
Element of b
2 holds b
4 . b
6,b
7 = b
5 . b
6,b
7 ) implies b
4 = b
5 )
proof
let c
1, c
2, c
3 be
set ;
let c
4, c
5 be
Function of
[:c1,c2:],c
3;
assume
for b
1 being
Element of c
1for b
2 being
Element of c
2 holds c
4 . b
1,b
2 = c
5 . b
1,b
2
;
then
for b
1, b
2 being
set holds
( b
1 in c
1 & b
2 in c
2 implies c
4 . b
1,b
2 = c
5 . b
1,b
2 )
;
hence
c
4 = c
5
by Th1;
end;
scheme :: BINOP_1:sch 1
s1{ F
1()
-> set , F
2()
-> set , F
3()
-> set , P
1[
set ,
set ,
set ] } :
ex b
1 being
Function of
[:F1(),F2():],F
3() st
for b
2, b
3 being
set holds
( b
2 in F
1() & b
3 in F
2() implies P
1[b
2,b
3,b
1 . b
2,b
3] )
provided
E2:
for b
1, b
2 being
set holds
not ( b
1 in F
1() & b
2 in F
2() & ( for b
3 being
set holds
not ( b
3 in F
3() & P
1[b
1,b
2,b
3] ) ) )
proof
defpred S
1[
set ,
set ] means for b
1, b
2 being
set holds
( a
1 = [b1,b2] implies P
1[b
1,b
2,a
2] );
E3:
for b
1 being
set holds
not ( b
1 in [:F1(),F2():] & ( for b
2 being
set holds
not ( b
2 in F
3() & S
1[b
1,b
2] ) ) )
proof
let c
1 be
set ;
assume
c
1 in [:F1(),F2():]
;
then consider c
2, c
3 being
set such that E4:
( c
2 in F
1() & c
3 in F
2() )
and E5:
c
1 = [c2,c3]
by ZFMISC_1:def 2;
consider c
4 being
set such that E6:
c
4 in F
3()
and E7:
P
1[c
2,c
3,c
4]
by E2, E4;
take
c
4
;
thus
c
4 in F
3()
by E6;
let c
5, c
6 be
set ;
assume
c
1 = [c5,c6]
;
then
( c
2 = c
5 & c
3 = c
6 )
by E5, ZFMISC_1:33;
hence
P
1[c
5,c
6,c
4]
by E7;
end;
consider c
1 being
Function of
[:F1(),F2():],F
3()
such that E4:
for b
1 being
set holds
( b
1 in [:F1(),F2():] implies S
1[b
1,c
1 . b
1] )
from FUNCT_2:sch 1(E3);
take
c
1
;
let c
2, c
3 be
set ;
assume
( c
2 in F
1() & c
3 in F
2() )
;
then
[c2,c3] in [:F1(),F2():]
by ZFMISC_1:def 2;
hence
P
1[c
2,c
3,c
1 . c
2,c
3]
by E4;
end;
scheme :: BINOP_1:sch 2
s2{ F
1()
-> set , F
2()
-> set , F
3()
-> set , F
4(
set ,
set )
-> set } :
ex b
1 being
Function of
[:F1(),F2():],F
3() st
for b
2, b
3 being
set holds
( b
2 in F
1() & b
3 in F
2() implies b
1 . b
2,b
3 = F
4(b
2,b
3) )
provided
E2:
for b
1, b
2 being
set holds
( b
1 in F
1() & b
2 in F
2() implies F
4(b
1,b
2)
in F
3() )
proof
defpred S
1[
set ,
set ,
set ] means a
3 = F
4(a
1,a
2);
E3:
for b
1, b
2 being
set holds
not ( b
1 in F
1() & b
2 in F
2() & ( for b
3 being
set holds
not ( b
3 in F
3() & S
1[b
1,b
2,b
3] ) ) )
proof
let c
1, c
2 be
set ;
assume E4:
( c
1 in F
1() & c
2 in F
2() )
;
take
F
4(c
1,c
2)
;
thus
( F
4(c
1,c
2)
in F
3() & S
1[c
1,c
2,F
4(c
1,c
2)] )
by E2, E4;
end;
thus
ex b
1 being
Function of
[:F1(),F2():],F
3() st
for b
2, b
3 being
set holds
( b
2 in F
1() & b
3 in F
2() implies S
1[b
2,b
3,b
1 . b
2,b
3] )
from BINOP_1:sch 1(E3);
end;
scheme :: BINOP_1:sch 3
s3{ F
1()
-> non
empty set , F
2()
-> non
empty set , F
3()
-> non
empty set , P
1[
set ,
set ,
set ] } :
provided
E2:
for b
1 being
Element of F
1()
for b
2 being
Element of F
2() holds
ex b
3 being
Element of F
3() st P
1[b
1,b
2,b
3]
proof
defpred S
1[
set ,
set ] means for b
1 being
Element of F
1()
for b
2 being
Element of F
2() holds
( a
1 = [b1,b2] implies P
1[b
1,b
2,a
2] );
E3:
for b
1 being
Element of
[:F1(),F2():] holds
ex b
2 being
Element of F
3() st
S
1[b
1,b
2]
consider c
1 being
Function of
[:F1(),F2():],F
3()
such that E4:
for b
1 being
Element of
[:F1(),F2():] holds
S
1[b
1,c
1 . b
1]
from FUNCT_2:sch 3(E3);
take
c
1
;
let c
2 be
Element of F
1();
let c
3 be
Element of F
2();
reconsider c
4 =
[c2,c3] as
Element of
[:F1(),F2():] by ZFMISC_1:def 2;
P
1[c
2,c
3,c
1 . c
4]
by E4;
hence
P
1[c
2,c
3,c
1 . c
2,c
3]
;
end;
scheme :: BINOP_1:sch 4
s4{ F
1()
-> non
empty set , F
2()
-> non
empty set , F
3()
-> non
empty set , F
4(
Element of F
1(),
Element of F
2())
-> Element of F
3() } :
proof
defpred S
1[
Element of F
1(),
Element of F
2(),
set ] means a
3 = F
4(a
1,a
2);
E2:
for b
1 being
Element of F
1()
for b
2 being
Element of F
2() holds
ex b
3 being
Element of F
3() st
S
1[b
1,b
2,b
3]
;
thus
ex b
1 being
Function of
[:F1(),F2():],F
3() st
for b
2 being
Element of F
1()
for b
3 being
Element of F
2() holds
S
1[b
2,b
3,b
1 . b
2,b
3]
from BINOP_1:sch 3(E2);
end;
definition
let c
1 be
set ;
let c
2 be
BinOp of c
1;
attr a
2 is
commutative means :
Def2:
:: BINOP_1:def 2
for b
1, b
2 being
Element of a
1 holds a
2 . b
1,b
2 = a
2 . b
2,b
1;
attr a
2 is
associative means :
Def3:
:: BINOP_1:def 3
for b
1, b
2, b
3 being
Element of a
1 holds a
2 . b
1,
(a2 . b2,b3) = a
2 . (a2 . b1,b2),b
3;
attr a
2 is
idempotent means :
Def4:
:: BINOP_1:def 4
for b
1 being
Element of a
1 holds a
2 . b
1,b
1 = b
1;
end;
:: deftheorem Def2 defines commutative BINOP_1:def 2 :
:: deftheorem Def3 defines associative BINOP_1:def 3 :
for b
1 being
set for b
2 being
BinOp of b
1 holds
( b
2 is
associative iff for b
3, b
4, b
5 being
Element of b
1 holds b
2 . b
3,
(b2 . b4,b5) = b
2 . (b2 . b3,b4),b
5 );
:: deftheorem Def4 defines idempotent BINOP_1:def 4 :
registration
cluster -> empty commutative associative M4(
[:{} ,{} :],
{} );
coherence
for b1 being BinOp of {} holds
( b1 is empty & b1 is associative & b1 is commutative )
proof
let c
1 be
BinOp of
{} ;
E5:
[:{} ,{} :] = {}
by ZFMISC_1:113;
then E6:
( c
1 c= [:(dom c1),(rng c1):] &
dom c
1 = {} &
rng c
1 c= {} )
by FUNCT_2:def 1, RELAT_1:21, RELSET_1:12;
thus
c
1 is
empty
by E5, XBOOLE_1:3;
let c
2, c
3 be
Element of
{} ;
:: according to BINOP_1:def 2
thus c
1 . c
2,c
3 =
{}
by E6, FUNCT_1:def 4
.=
c
1 . c
3,c
2
by E6, FUNCT_1:def 4
;
end;
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 :
:: deftheorem Def7 defines is_a_unity_wrt BINOP_1:def 7 :
theorem Th3: :: BINOP_1:3
canceled;
theorem Th4: :: BINOP_1:4
canceled;
theorem Th5: :: BINOP_1:5
canceled;
theorem Th6: :: BINOP_1:6
canceled;
theorem Th7: :: BINOP_1:7
canceled;
theorem Th8: :: BINOP_1:8
canceled;
theorem Th9: :: BINOP_1:9
canceled;
theorem Th10: :: BINOP_1:10
canceled;
theorem Th11: :: BINOP_1:11
theorem Th12: :: BINOP_1:12
theorem Th13: :: BINOP_1:13
theorem Th14: :: BINOP_1:14
theorem Th15: :: BINOP_1:15
theorem Th16: :: BINOP_1:16
theorem Th17: :: BINOP_1:17
theorem Th18: :: BINOP_1:18
:: deftheorem Def8 defines the_unity_wrt BINOP_1:def 8 :
definition
let c
1 be
set ;
let c
2, c
3 be
BinOp of c
1;
pred c
2 is_left_distributive_wrt c
3 means :
Def9:
:: BINOP_1:def 9
for b
1, b
2, b
3 being
Element of a
1 holds a
2 . b
1,
(a3 . b2,b3) = a
3 . (a2 . b1,b2),
(a2 . b1,b3);
pred c
2 is_right_distributive_wrt c
3 means :
Def10:
:: BINOP_1:def 10
for b
1, b
2, b
3 being
Element of a
1 holds a
2 . (a3 . b1,b2),b
3 = a
3 . (a2 . b1,b3),
(a2 . b2,b3);
end;
:: deftheorem Def9 defines is_left_distributive_wrt BINOP_1:def 9 :
:: deftheorem Def10 defines is_right_distributive_wrt BINOP_1:def 10 :
:: deftheorem Def11 defines is_distributive_wrt BINOP_1:def 11 :
theorem Th19: :: BINOP_1:19
canceled;
theorem Th20: :: BINOP_1:20
canceled;
theorem Th21: :: BINOP_1:21
canceled;
theorem Th22: :: BINOP_1:22
canceled;
theorem Th23: :: BINOP_1:23
for b
1 being
set for b
2, b
3 being
BinOp of b
1 holds
( b
2 is_distributive_wrt b
3 iff for b
4, b
5, b
6 being
Element of b
1 holds
( b
2 . b
4,
(b3 . b5,b6) = b
3 . (b2 . b4,b5),
(b2 . b4,b6) & b
2 . (b3 . b4,b5),b
6 = b
3 . (b2 . b4,b6),
(b2 . b5,b6) ) )
proof
let c
1 be
set ;
let c
2, c
3 be
BinOp of c
1;
thus
( c
2 is_distributive_wrt c
3 implies for b
1, b
2, b
3 being
Element of c
1 holds
( c
2 . b
1,
(c3 . b2,b3) = c
3 . (c2 . b1,b2),
(c2 . b1,b3) & c
2 . (c3 . b1,b2),b
3 = c
3 . (c2 . b1,b3),
(c2 . b2,b3) ) )
proof
assume
( c
2 is_left_distributive_wrt c
3 & c
2 is_right_distributive_wrt c
3 )
;
:: according to BINOP_1:def 11
hence
for b
1, b
2, b
3 being
Element of c
1 holds
( c
2 . b
1,
(c3 . b2,b3) = c
3 . (c2 . b1,b2),
(c2 . b1,b3) & c
2 . (c3 . b1,b2),b
3 = c
3 . (c2 . b1,b3),
(c2 . b2,b3) )
by Def9, Def10;
end;
assume
for b
1, b
2, b
3 being
Element of c
1 holds
( c
2 . b
1,
(c3 . b2,b3) = c
3 . (c2 . b1,b2),
(c2 . b1,b3) & c
2 . (c3 . b1,b2),b
3 = c
3 . (c2 . b1,b3),
(c2 . b2,b3) )
;
hence
( ( for b
1, b
2, b
3 being
Element of c
1 holds c
2 . b
1,
(c3 . b2,b3) = c
3 . (c2 . b1,b2),
(c2 . b1,b3) ) & ( for b
1, b
2, b
3 being
Element of c
1 holds c
2 . (c3 . b1,b2),b
3 = c
3 . (c2 . b1,b3),
(c2 . b2,b3) ) )
;
:: according to BINOP_1:def 9,
BINOP_1:def 10,
BINOP_1:def 11
end;
theorem Th24: :: BINOP_1:24
proof
let c
1 be non
empty set ;
let c
2, c
3 be
BinOp of c
1;
assume E18:
c
3 is
commutative
;
( ( for b
1, b
2, b
3 being
Element of c
1 holds
( c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3) & c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3) ) ) iff for b
1, b
2, b
3 being
Element of c
1 holds c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3) )
proof
thus
( ( for b
1, b
2, b
3 being
Element of c
1 holds
( c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3) & c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3) ) ) implies for b
1, b
2, b
3 being
Element of c
1 holds c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3) )
;
assume E19:
for b
1, b
2, b
3 being
Element of c
1 holds c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3)
;
let c
4, c
5, c
6 be
Element of c
1;
thus
c
3 . c
4,
(c2 . c5,c6) = c
2 . (c3 . c4,c5),
(c3 . c4,c6)
by E19;
thus c
3 . (c2 . c4,c5),c
6 =
c
3 . c
6,
(c2 . c4,c5)
by E18, Def2
.=
c
2 . (c3 . c6,c4),
(c3 . c6,c5)
by E19
.=
c
2 . (c3 . c4,c6),
(c3 . c6,c5)
by E18, Def2
.=
c
2 . (c3 . c4,c6),
(c3 . c5,c6)
by E18, Def2
;
end;
hence
( c
3 is_distributive_wrt c
2 iff for b
1, b
2, b
3 being
Element of c
1 holds c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3) )
by Th23;
end;
theorem Th25: :: BINOP_1:25
proof
let c
1 be non
empty set ;
let c
2, c
3 be
BinOp of c
1;
assume E19:
c
3 is
commutative
;
( ( for b
1, b
2, b
3 being
Element of c
1 holds
( c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3) & c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3) ) ) iff for b
1, b
2, b
3 being
Element of c
1 holds c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3) )
proof
thus
( ( for b
1, b
2, b
3 being
Element of c
1 holds
( c
3 . b
1,
(c2 . b2,b3) = c
2 . (c3 . b1,b2),
(c3 . b1,b3) & c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3) ) ) implies for b
1, b
2, b
3 being
Element of c
1 holds c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3) )
;
assume E20:
for b
1, b
2, b
3 being
Element of c
1 holds c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3)
;
let c
4, c
5, c
6 be
Element of c
1;
thus c
3 . c
4,
(c2 . c5,c6) =
c
3 . (c2 . c5,c6),c
4
by E19, Def2
.=
c
2 . (c3 . c5,c4),
(c3 . c6,c4)
by E20
.=
c
2 . (c3 . c4,c5),
(c3 . c6,c4)
by E19, Def2
.=
c
2 . (c3 . c4,c5),
(c3 . c4,c6)
by E19, Def2
;
thus
c
3 . (c2 . c4,c5),c
6 = c
2 . (c3 . c4,c6),
(c3 . c5,c6)
by E20;
end;
hence
( c
3 is_distributive_wrt c
2 iff for b
1, b
2, b
3 being
Element of c
1 holds c
3 . (c2 . b1,b2),b
3 = c
2 . (c3 . b1,b3),
(c3 . b2,b3) )
by Th23;
end;
theorem Th26: :: BINOP_1:26
theorem Th27: :: BINOP_1:27
theorem Th28: :: BINOP_1:28
:: deftheorem Def12 defines is_distributive_wrt BINOP_1:def 12 :
definition
let c
1 be non
empty set ;
let c
2 be
BinOp of c
1;
redefine attr a
2 is
commutative means :: BINOP_1:def 13
for b
1, b
2 being
Element of a
1 holds a
2 . b
1,b
2 = a
2 . b
2,b
1;
correctness
compatibility
( c2 is commutative iff for b1, b2 being Element of c1 holds c2 . b1,b2 = c2 . b2,b1 );
by Def2;
redefine attr a
2 is
associative means :: BINOP_1:def 14
for b
1, b
2, b
3 being
Element of a
1 holds a
2 . b
1,
(a2 . b2,b3) = a
2 . (a2 . b1,b2),b
3;
correctness
compatibility
( c2 is associative iff for b1, b2, b3 being Element of c1 holds c2 . b1,(c2 . b2,b3) = c2 . (c2 . b1,b2),b3 );
by Def3;
redefine attr a
2 is
idempotent means :: BINOP_1:def 15
for b
1 being
Element of a
1 holds a
2 . b
1,b
1 = b
1;
correctness
compatibility
( c2 is idempotent iff for b1 being Element of c1 holds c2 . b1,b1 = b1 );
by Def4;
end;
:: deftheorem Def13 defines commutative BINOP_1:def 13 :
:: deftheorem Def14 defines associative BINOP_1:def 14 :
:: deftheorem Def15 defines idempotent BINOP_1:def 15 :
:: deftheorem Def16 defines is_a_left_unity_wrt BINOP_1:def 16 :
:: deftheorem Def17 defines is_a_right_unity_wrt BINOP_1:def 17 :
definition
let c
1 be non
empty set ;
let c
2, c
3 be
BinOp of c
1;
redefine pred c
2 is_left_distributive_wrt c
3 means :: BINOP_1:def 18
for b
1, b
2, b
3 being
Element of a
1 holds a
2 . b
1,
(a3 . b2,b3) = a
3 . (a2 . b1,b2),
(a2 . b1,b3);
correctness
compatibility
( c2 is_left_distributive_wrt c3 iff for b1, b2, b3 being Element of c1 holds c2 . b1,(c3 . b2,b3) = c3 . (c2 . b1,b2),(c2 . b1,b3) );
by Def9;
redefine pred c
2 is_right_distributive_wrt c
3 means :: BINOP_1:def 19
for b
1, b
2, b
3 being
Element of a
1 holds a
2 . (a3 . b1,b2),b
3 = a
3 . (a2 . b1,b3),
(a2 . b2,b3);