:: Semigroup operations on finite subsets
:: by Czes{\l}aw Byli\'nski
::
:: Received May 4, 1990
:: Copyright (c) 1990 Association of Mizar Users
Lm1:
for i being Nat holds Seg i is Element of Fin NAT
by FINSUB_1:def 5;
theorem :: SETWOP_2:1
canceled;
theorem :: SETWOP_2:2
canceled;
theorem Th3: :: SETWOP_2:3
theorem Th4: :: SETWOP_2:4
theorem :: SETWOP_2:5
theorem :: SETWOP_2:6
theorem Th7: :: SETWOP_2:7
theorem :: SETWOP_2:8
theorem :: SETWOP_2:9
theorem :: SETWOP_2:10
theorem Th11: :: SETWOP_2:11
for
C,
D being non
empty set for
B being
Element of
Fin C for
e being
Element of
D for
F,
G being
BinOp of
D for
f,
f' being
Function of
C,
D st
F is
commutative &
F is
associative &
F is
having_a_unity &
e = the_unity_wrt F &
G . e,
e = e & ( for
d1,
d2,
d3,
d4 being
Element of
D holds
F . (G . d1,d2),
(G . d3,d4) = G . (F . d1,d3),
(F . d2,d4) ) holds
G . (F $$ B,f),
(F $$ B,f') = F $$ B,
(G .: f,f')
Lm3:
for D being non empty set
for F being BinOp of D st F is commutative & F is associative holds
for d1, d2, d3, d4 being Element of D holds F . (F . d1,d2),(F . d3,d4) = F . (F . d1,d3),(F . d2,d4)
theorem :: SETWOP_2:12
theorem :: SETWOP_2:13
for
C,
D being non
empty set for
B being
Element of
Fin C for
F,
G being
BinOp of
D for
f,
f' being
Function of
C,
D st
F is
commutative &
F is
associative &
F is
having_a_unity &
F is
having_an_inverseOp &
G = F * (id D),
(the_inverseOp_wrt F) holds
G . (F $$ B,f),
(F $$ B,f') = F $$ B,
(G .: f,f')
theorem Th14: :: SETWOP_2:14
theorem Th15: :: SETWOP_2:15
theorem :: SETWOP_2:16
theorem :: SETWOP_2:17
theorem Th18: :: SETWOP_2:18
theorem :: SETWOP_2:19
theorem :: SETWOP_2:20
theorem :: SETWOP_2:21
:: deftheorem defines [#] SETWOP_2:def 1 :
theorem Th22: :: SETWOP_2:22
theorem :: SETWOP_2:23
theorem :: SETWOP_2:24
theorem :: SETWOP_2:25
theorem :: SETWOP_2:26
Lm4:
for D being non empty set
for e being Element of D
for F being BinOp of D
for p, q being FinSequence of D st len p = len q & F . e,e = e holds
F .: ([#] p,e),([#] q,e) = [#] (F .: p,q),e
Lm5:
for D being non empty set
for e, d being Element of D
for F being BinOp of D
for p being FinSequence of D st F . e,d = e holds
F [:] ([#] p,e),d = [#] (F [:] p,d),e
Lm6:
for D being non empty set
for d, e being Element of D
for F being BinOp of D
for p being FinSequence of D st F . d,e = e holds
F [;] d,([#] p,e) = [#] (F [;] d,p),e
:: deftheorem Def2 defines $$ SETWOP_2:def 2 :
theorem :: SETWOP_2:27
canceled;
theorem :: SETWOP_2:28
canceled;
theorem :: SETWOP_2:29
canceled;
theorem :: SETWOP_2:30
canceled;
theorem :: SETWOP_2:31
canceled;
theorem :: SETWOP_2:32
canceled;
theorem :: SETWOP_2:33
canceled;
theorem :: SETWOP_2:34
canceled;
theorem Th35: :: SETWOP_2:35
theorem :: SETWOP_2:36
canceled;
theorem Th37: :: SETWOP_2:37
theorem :: SETWOP_2:38
theorem Th39: :: SETWOP_2:39
theorem :: SETWOP_2:40
theorem :: SETWOP_2:41
theorem :: SETWOP_2:42
theorem Th43: :: SETWOP_2:43
for
D being non
empty set for
e being
Element of
D for
F,
G being
BinOp of
D for
p,
q being
FinSequence of
D st
F is
commutative &
F is
associative &
F is
having_a_unity &
e = the_unity_wrt F &
G . e,
e = e & ( for
d1,
d2,
d3,
d4 being
Element of
D holds
F . (G . d1,d2),
(G . d3,d4) = G . (F . d1,d3),
(F . d2,d4) ) &
len p = len q holds
G . (F "**" p),
(F "**" q) = F "**" (G .: p,q)
theorem Th44: :: SETWOP_2:44
for
D being non
empty set for
e being
Element of
D for
F,
G being
BinOp of
D for
i being
Nat for
T1,
T2 being
Element of
i -tuples_on D st
F is
commutative &
F is
associative &
F is
having_a_unity &
e = the_unity_wrt F &
G . e,
e = e & ( for
d1,
d2,
d3,
d4 being
Element of
D holds
F . (G . d1,d2),
(G . d3,d4) = G . (F . d1,d3),
(F . d2,d4) ) holds
G . (F "**" T1),
(F "**" T2) = F "**" (G .: T1,T2)
theorem Th45: :: SETWOP_2:45
theorem Th46: :: SETWOP_2:46
theorem :: SETWOP_2:47
theorem :: SETWOP_2:48
theorem Th49: :: SETWOP_2:49
theorem Th50: :: SETWOP_2:50
theorem :: SETWOP_2:51
theorem :: SETWOP_2:52