:: Monoid of Multisets and Subsets
:: by Grzegorz Bancerek
::
:: Received December 29, 1992
:: Copyright (c) 1992-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, NUMBERS, ALGSTR_0, MESFUNC1, XBOOLE_0, FUNCT_1,
ZFMISC_1, FINSEQ_4, FUNCT_2, RELAT_1, PARTFUN1, TARSKI, FUNCOP_1,
FINSEQ_2, FINSEQ_1, BINOP_1, SETWISEO, ALGSTR_1, MONOID_0, LATTICE2,
MCART_1, STRUCT_0, GROUP_1, VECTSP_1, BINOP_2, CARD_1, ARYTM_3, FUNCT_3,
FINSET_1, ORDINAL4, COMPLEX1, ARYTM_1, MONOID_1, NAT_1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XXREAL_0, XCMPLX_0, REAL_1, NAT_1, RELAT_1, STRUCT_0, FUNCT_1, FINSEQ_1,
MONOID_0, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, RECDEF_1,
SETWISEO, FINSET_1, FUNCT_3, FINSEQ_2, LATTICE2, FUNCT_6, DOMAIN_1,
ALGSTR_0;
constructors BINOP_1, DOMAIN_1, FUNCT_3, SETWISEO, REAL_1, BINOP_2, RECDEF_1,
FUNCT_5, FUNCT_6, LATTICE2, MONOID_0, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FUNCOP_1, FINSET_1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, MONOID_0, CARD_1,
RELSET_1, XTUPLE_0, VALUED_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, BINOP_1, LATTICE2, SETWISEO, MONOID_0, STRUCT_0, XBOOLE_0;
equalities BINOP_1, STRUCT_0, FUNCT_6, ALGSTR_0;
expansions TARSKI, BINOP_1, SETWISEO, MONOID_0, XBOOLE_0, RELAT_1;
theorems TARSKI, NAT_1, FINSEQ_1, BINOP_1, MCART_1, FUNCOP_1, ZFMISC_1,
FUNCT_1, FUNCT_2, FUNCT_3, CARD_1, CARD_2, FINSEQ_2, FINSEQ_3, FUNCT_5,
MONOID_0, GRFUNC_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, GROUP_1;
schemes NAT_1, FUNCT_2, MONOID_0, PARTFUN1, FUNCT_1, BINOP_1;
begin :: Updating
reserve x,y,z, X,Y,Z for set,
n for Element of NAT;
deffunc op(multMagma) = the multF of $1;
deffunc un(multLoopStr) = 1.$1;
definition
let f be Function, x1,x2,y be set;
func f..(x1,x2,y) -> set equals
f..([x1,x2],y);
correctness;
end;
definition
let A,D1,D2,D be non empty set;
let f be Function of [:D1, D2:], Funcs(A,D);
let x1 be Element of D1;
let x2 be Element of D2;
let x be Element of A;
redefine func f..(x1,x2,x) -> Element of D; :: redefines .. (MONOID_1, definition)
coherence
proof
reconsider g = f.(x1,x2) as Element of Funcs(A,D);
A1: [x1,x2] in [:D1,D2:];
dom f = [:D1,D2:] & dom g = A by FUNCT_2:def 1;
then f..(x1,x2,x) = g.x by A1,FUNCT_5:38;
hence thesis;
end;
end;
definition
let A be set;
let D1,D2,D be non empty set, f be Function of [:D1,D2:],D;
let g1 be Function of A,D1;
let g2 be Function of A,D2;
redefine func f.:(g1,g2) -> Element of Funcs(A,D); :: redefines .: (FUNCOP_1, definition)
coherence
proof
f.:(g1,g2) = f*<:g1,g2:> by FUNCOP_1:def 3;
then dom (f.:(g1,g2)) = A & rng (f.:(g1,g2)) c= D by FUNCT_2:def 1
,RELAT_1:def 19;
hence thesis by FUNCT_2:def 2;
end;
end;
notation
let A be non empty set;
let n be Element of NAT, x be Element of A;
synonym n .--> x for n |-> x;
end;
definition
let A be non empty set;
let n be Element of NAT, x be Element of A;
redefine func n .--> x -> FinSequence of A; :: redefines .--> (MONOID_1, synonym) → |-> (FINSEQ_2, definition)
coherence by FINSEQ_2:63;
end;
definition
let D be non empty set, A be set, d be Element of D;
redefine func A --> d -> Element of Funcs(A,D); :: redefines --> (FUNCOP_1, definition)
coherence
proof
dom (A --> d) = A & rng (A --> d) c= {d} by FUNCOP_1:13;
hence thesis by FUNCT_2:def 2;
end;
end;
definition
let A be set;
let D1,D2,D be non empty set, f be Function of [:D1,D2:],D;
let d be Element of D1;
let g be Function of A,D2;
redefine func f[;](d,g) -> Element of Funcs(A,D); :: redefines [;] (FUNCOP_1, definition)
coherence
proof
dom g = A by FUNCT_2:def 1;
then f[;](d,g) = f*<:A --> d, g:> by FUNCOP_1:def 5;
then dom (f[;](d,g)) = A & rng (f[;](d,g)) c= D by FUNCT_2:def 1
,RELAT_1:def 19;
hence thesis by FUNCT_2:def 2;
end;
end;
definition
let A be set;
let D1,D2,D be non empty set, f be Function of [:D1,D2:],D;
let g be Function of A,D1;
let d be Element of D2;
redefine func f[:](g,d) -> Element of Funcs(A,D); :: redefines [:] (FUNCOP_1, definition)
coherence
proof
dom g = A by FUNCT_2:def 1;
then f[:](g,d) = f*<:g, A --> d:> by FUNCOP_1:def 4;
then dom (f[:](g,d)) = A & rng (f[:](g,d)) c= D by FUNCT_2:def 1
,RELAT_1:def 19;
hence thesis by FUNCT_2:def 2;
end;
end;
theorem
for f,g being Function, X being set holds (f|X)*g = f*(X|`g)
proof
let f,g be Function, X be set;
A1: dom (f|X) = dom f /\ X by RELAT_1:61;
A2: dom ((f|X)*g) = dom (f*(X|`g))
proof
thus dom ((f|X)*g) c= dom (f*(X|`g))
proof
let x be object;
assume
A3: x in dom ((f|X)*g);
then
A4: x in dom g by FUNCT_1:11;
A5: g.x in dom (f|X) by A3,FUNCT_1:11;
then
A6: g.x in dom f by A1,XBOOLE_0:def 4;
g.x in X by A1,A5,XBOOLE_0:def 4;
then
A7: x in dom (X|`g) by A4,FUNCT_1:53;
then g.x = (X|`g).x by FUNCT_1:53;
hence thesis by A6,A7,FUNCT_1:11;
end;
let x be object;
assume
A8: x in dom (f*(X|`g));
then
A9: x in dom (X|`g) by FUNCT_1:11;
then
A10: x in dom g by FUNCT_1:53;
(X|`g).x in dom f by A8,FUNCT_1:11;
then
A11: g.x in dom f by A9,FUNCT_1:53;
g.x in X by A9,FUNCT_1:53;
then g.x in dom (f|X) by A1,A11,XBOOLE_0:def 4;
hence thesis by A10,FUNCT_1:11;
end;
now
let x be object;
assume
A12: x in dom ((f|X)*g);
then ((f|X)*g).x = (f|X).(g.x) & g.x in dom (f|X) by FUNCT_1:11,12;
then
A13: ((f|X)*g).x = f.(g.x) by FUNCT_1:47;
(f*(X|`g)).x = f.((X|`g).x) & x in dom (X|`g) by A2,A12,FUNCT_1:11,12;
hence ((f|X)*g).x = (f*(X|`g)).x by A13,FUNCT_1:53;
end;
hence thesis by A2,FUNCT_1:2;
end;
scheme
NonUniqFuncDEx { X() -> set, Y() -> non empty set, P[object,object] }:
ex f being
Function of X(), Y() st for x being object st x in X() holds P[x,f.x]
provided
A1: for x being object st x in X() ex y being Element of Y() st P[x,y]
proof
A2: for x being object st x in X() ex y being object st y in Y() & P[x,y]
proof
let x be object;
assume x in X();
then consider y being Element of Y() such that
A3: P[x,y] by A1;
take y;
thus thesis by A3;
end;
consider f being Function such that
A4: dom f = X() & rng f c= Y() &
for x being object st x in X() holds P[x,f.x] from
FUNCT_1:sch 6(A2);
reconsider f as Function of X(), Y() by A4,FUNCT_2:def 1,RELSET_1:4;
take f;
thus thesis by A4;
end;
begin :: Monoid of functions into a semigroup
definition
let D1,D2,D be non empty set;
let f be Function of [:D1,D2:],D;
let A be set;
func (f,D).:A -> Function of [:Funcs(A,D1), Funcs(A,D2):], Funcs(A,D)
means
:
Def2: for f1 being Element of Funcs(A,D1) for f2 being Element of Funcs(A,D2)
holds it.(f1,f2) = f.:(f1,f2);
existence
proof
deffunc G(Element of Funcs(A,D1),Element of Funcs(A,D2)) = f.:($1,$2);
consider b being Function of [:Funcs(A,D1), Funcs(A,D2):],
Funcs(A,D) such that
A1: for f1 being Element of Funcs(A,D1) for f2 being Element of Funcs(
A,D2) holds b.(f1,f2) = G(f1,f2) from BINOP_1:sch 4;
take b;
let f1 be Element of Funcs(A,D1), f2 be Element of Funcs(A,D2);
thus thesis by A1;
end;
uniqueness
proof
let o1,o2 be Function of [:Funcs(A,D1), Funcs(A,D2):], Funcs(A,D)
such that
A2: for f1 being Element of Funcs(A,D1) for f2 being Element of Funcs(
A,D2) holds o1.(f1,f2) = f.:(f1,f2) and
A3: for f1 being Element of Funcs(A,D1) for f2 being Element of Funcs(
A,D2) holds o2.(f1,f2) = f.:(f1,f2);
now
let f1 be Element of Funcs(A,D1), f2 be Element of Funcs(A,D2);
thus o1.(f1,f2) = f.:(f1,f2) by A2
.= o2.(f1,f2) by A3;
end;
hence thesis;
end;
end;
theorem
for D1,D2,D being non empty set for f being Function of [:D1,D2:],D for A
being set, f1 being (Function of A,D1), f2 being Function of A,D2 for x st x in
A holds ((f,D).:A)..(f1,f2,x) = f.(f1.x,f2.x)
proof
let D1,D2,D be non empty set;
let f be Function of [:D1,D2:],D;
let A be set, f1 be (Function of A,D1), f2 be Function of A,D2;
dom f2 = A & rng f2 c= D2 by FUNCT_2:def 1;
then reconsider f2 as Element of Funcs(A,D2) by FUNCT_2:def 2;
dom f1 = A & rng f1 c= D1 by FUNCT_2:def 1;
then reconsider f1 as Element of Funcs(A,D1) by FUNCT_2:def 2;
A1: dom (f.: (f1,f2)) = A by FUNCT_2:def 1;
A2: ((f,D).:A).(f1,f2) = f.:(f1,f2) & [f1,f2] = [f1,f2] by Def2;
let x such that
A3: x in A;
dom ((f,D).:A) = [:Funcs(A,D1), Funcs(A,D2):] & (f.:(f1,f2)).x = f.(f1.x
,f2. x) by A3,A1,FUNCOP_1:22,FUNCT_2:def 1;
hence thesis by A3,A1,A2,FUNCT_5:38;
end;
reserve A for set,
D for non empty set,
a,b,c,l,r for Element of D,
o,o9 for BinOp of D,
f,g,h for Function of A,D;
theorem Th3:
o is commutative implies o.:(f,g) = o.:(g,f)
proof
A1: dom (o.:(f,g)) = A by FUNCT_2:def 1;
A2: dom f = A & dom g = A by FUNCT_2:def 1;
A3: dom (o.:(g,f)) = A by FUNCT_2:def 1;
assume
A4: o.(a,b) = o.(b,a);
now
let x be object;
assume
A5: x in A;
then f.x in rng f & g.x in rng g by A2,FUNCT_1:def 3;
then reconsider a = f.x, b = g.x as Element of D;
thus (o.:(f,g)).x = o.(a,b) by A1,A5,FUNCOP_1:22
.= o.(b,a) by A4
.= (o.:(g,f)).x by A3,A5,FUNCOP_1:22;
end;
hence thesis by A1,A3,FUNCT_1:2;
end;
theorem Th4:
o is associative implies o.:(o.:(f,g),h) = o.:(f,o.:(g,h))
proof
A1: dom (o.:(f,g)) = A by FUNCT_2:def 1;
A2: dom (o.:(g,h)) = A by FUNCT_2:def 1;
A3: dom f = A & dom g = A by FUNCT_2:def 1;
A4: dom (o.:(o.:(f,g),h)) = A by FUNCT_2:def 1;
A5: dom h = A by FUNCT_2:def 1;
A6: dom (o.:(f,o.:(g,h))) = A by FUNCT_2:def 1;
assume
A7: o.(o.(a,b),c) = o.(a,o.(b,c));
now
let x be object;
assume
A8: x in A;
then
A9: h.x in rng h by A5,FUNCT_1:def 3;
f.x in rng f & g.x in rng g by A3,A8,FUNCT_1:def 3;
then reconsider a = f.x, b = g.x, c = h.x as Element of D by A9;
thus (o.:(o.:(f,g),h)).x = o.((o.:(f,g)).x,c) by A4,A8,FUNCOP_1:22
.= o.(o.(a,b),c) by A1,A8,FUNCOP_1:22
.= o.(a,o.(b,c)) by A7
.= o.(a,(o.:(g,h)).x) by A2,A8,FUNCOP_1:22
.= (o.:(f,o.:(g,h))).x by A6,A8,FUNCOP_1:22;
end;
hence thesis by A4,A6,FUNCT_1:2;
end;
theorem Th5:
a is_a_unity_wrt o implies o[;](a,f) = f & o[:](f,a) = f
proof
assume
A1: a is_a_unity_wrt o;
A2: dom f = A by FUNCT_2:def 1;
A3: dom (o[;](a,f)) = A by FUNCT_2:def 1;
now
let x be object;
assume
A4: x in A;
then f.x in rng f by A2,FUNCT_1:def 3;
then reconsider b = f.x as Element of D;
thus (o[;](a,f)).x = o.(a,b) by A3,A4,FUNCOP_1:32
.= f.x by A1,BINOP_1:3;
end;
hence o[;](a,f) = f by A3,A2,FUNCT_1:2;
A5: dom (o[:](f,a)) = A by FUNCT_2:def 1;
now
let x be object;
assume
A6: x in A;
then f.x in rng f by A2,FUNCT_1:def 3;
then reconsider b = f.x as Element of D;
thus (o[:](f,a)).x = o.(b,a) by A5,A6,FUNCOP_1:27
.= f.x by A1,BINOP_1:3;
end;
hence thesis by A5,A2,FUNCT_1:2;
end;
theorem Th6:
o is idempotent implies o.:(f,f) = f
proof
A1: dom (o.:(f,f)) = A by FUNCT_2:def 1;
assume
A2: o.(a,a) = a;
A3: now
let x be object;
assume
A4: x in A;
then reconsider a = f.x as Element of D by FUNCT_2:5;
thus o.:(f,f).x = o.(a,a) by A1,A4,FUNCOP_1:22
.= f.x by A2;
end;
dom f = A by FUNCT_2:def 1;
hence thesis by A1,A3,FUNCT_1:2;
end;
theorem Th7:
o is commutative implies (o,D).:A is commutative
proof
assume
A1: o is commutative;
set h = (o,D).:A;
let f,g be Element of Funcs(A,D);
thus h.(f,g) = o.:(f, g) by Def2
.= o.:(g, f) by A1,Th3
.= h.(g,f) by Def2;
end;
theorem Th8:
o is associative implies (o,D).:A is associative
proof
assume
A1: o is associative;
set F = (o,D).:A;
let f,g,h be Element of Funcs(A,D);
thus F.(F.(f,g),h) = F.(o.:(f,g),h) by Def2
.= o.:(o.:(f,g),h) by Def2
.= o.:(f,o.:(g,h)) by A1,Th4
.= F.(f,o.:(g,h)) by Def2
.= F.(f,F.(g,h)) by Def2;
end;
theorem Th9:
a is_a_unity_wrt o implies A --> a is_a_unity_wrt (o,D).:A
proof
set e = A --> a;
set F = (o,D).:A;
assume
A1: a is_a_unity_wrt o;
now
let f be Element of Funcs(A,D);
A2: dom f = A by FUNCT_2:def 1;
thus F.(e,f) = o.:(e,f) by Def2
.= o[;](a,f) by A2,FUNCOP_1:31
.= f by A1,Th5;
thus F.(f,e) = o.:(f,e) by Def2
.= o[:](f,a) by A2,FUNCOP_1:26
.= f by A1,Th5;
end;
hence thesis by BINOP_1:3;
end;
theorem Th10:
o is having_a_unity implies the_unity_wrt (o,D).:A = A -->
the_unity_wrt o & (o,D).:A is having_a_unity
proof
given a such that
A1: a is_a_unity_wrt o;
a = the_unity_wrt o & A --> a is_a_unity_wrt (o,D).:A by A1,Th9,BINOP_1:def 8
;
hence the_unity_wrt (o,D).:A = A --> the_unity_wrt o by BINOP_1:def 8;
take A --> a;
thus thesis by A1,Th9;
end;
theorem Th11:
o is idempotent implies (o,D).:A is idempotent
proof
assume
A1: o is idempotent;
let f be Element of Funcs(A,D);
thus ((o,D).:A).(f,f) = o.:(f,f) by Def2
.= f by A1,Th6;
end;
theorem Th12:
o is invertible implies (o,D).:A is invertible
proof
assume
A1: for a,b ex r,l st o.(a,r) = b & o.(l,a) = b;
let f,g be Element of Funcs(A,D);
defpred P[object,object] means o.(f.$1,$2) = g.$1;
A2: for x being object st x in A ex c st P[x,c]
proof
let x be object;
assume x in A;
then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:5;
consider r,l such that
A3: o.(a,r) = b and
o.(l,a) = b by A1;
take r;
thus thesis by A3;
end;
consider h1 being Function of A,D such that
A4: for x being object st x in A holds P[x,h1.x] from NonUniqFuncDEx(A2);
defpred Q[object,object] means o.($2,f.$1) = g.$1;
A5: for x being object st x in A ex c st Q[x,c]
proof
let x be object;
assume x in A;
then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:5;
consider r,l such that
o.(a,r) = b and
A6: o.(l,a) = b by A1;
take l;
thus thesis by A6;
end;
consider h2 being Function of A,D such that
A7: for x being object st x in A holds Q[x,h2.x] from NonUniqFuncDEx(A5);
A8: dom h1 = A & dom h2 = A by FUNCT_2:def 1;
rng h1 c= D & rng h2 c= D;
then reconsider h1, h2 as Element of Funcs(A,D) by A8,FUNCT_2:def 2;
take h1, h2;
A9: dom g = A by FUNCT_2:def 1;
A10: dom (o.:(f,h1)) = A by FUNCT_2:def 1;
A11: now
let x be object;
assume
A12: x in A;
hence o.:(f,h1).x = o.(f.x,h1.x) by A10,FUNCOP_1:22
.= g.x by A4,A12;
end;
o.:(f,h1) = ((o,D).:A).(f,h1) by Def2;
hence ((o,D).:A).(f,h1) = g by A10,A9,A11,FUNCT_1:2;
A13: dom (o.:(h2,f)) = A by FUNCT_2:def 1;
A14: now
let x be object;
assume
A15: x in A;
hence o.:(h2,f).x = o.(h2.x,f.x) by A13,FUNCOP_1:22
.= g.x by A7,A15;
end;
o.:(h2,f) = ((o,D).:A).(h2,f) by Def2;
hence thesis by A13,A9,A14,FUNCT_1:2;
end;
theorem Th13:
o is cancelable implies (o,D).:A is cancelable
proof
assume
A1: o.(a,b) = o.(a,c) or o.(b,a) = o.(c,a) implies b = c;
let f,g,h be Element of Funcs(A,D) such that
A2: (o,D).:A.(f,g) = (o,D).:A.(f,h) or (o,D).:A.(g,f) = (o,D).:A.(h,f);
A3: A = dom (o.:(g,f)) & A = dom (o.:(h,f)) by FUNCT_2:def 1;
A4: (o,D).:A.(f,h) = o.:(f,h) & (o,D).:A.(h,f) = o.:(h,f) by Def2;
A5: A = dom (o.:(f,g)) & A = dom (o.:(f,h)) by FUNCT_2:def 1;
A6: (o,D).:A.(f,g) = o.:(f,g) & (o,D).:A.(g,f) = o.:(g,f) by Def2;
A7: now
let x be object;
assume
A8: x in A;
then reconsider a = f.x, b = g.x, c = h.x as Element of D by FUNCT_2:5;
A9: o.:(g,f).x = o.(b,a) & o.:(h,f).x = o.(c,a) by A3,A8,FUNCOP_1:22;
o.:(f,g).x = o.(a,b) & o.:(f,h).x = o.(a,c) by A5,A8,FUNCOP_1:22;
hence g.x = h.x by A1,A2,A6,A4,A9;
end;
dom g = A & dom h = A by FUNCT_2:def 1;
hence thesis by A7,FUNCT_1:2;
end;
theorem Th14:
o is uniquely-decomposable implies (o,D).:A is uniquely-decomposable
proof
assume that
A1: o is having_a_unity and
A2: for a,b st o.(a,b) = the_unity_wrt o holds a = b & b = the_unity_wrt o;
A3: the_unity_wrt (o,D).:A = A --> the_unity_wrt o by A1,Th10;
thus (o,D).:A is having_a_unity by A1,Th10;
let f,g be Element of Funcs(A,D) such that
A4: (o,D).:A.(f,g) = the_unity_wrt (o,D).:A;
A5: dom (o.:(f,g)) = A by FUNCT_2:def 1;
A6: (o,D).:A.(f,g) = o.:(f,g) by Def2;
A7: now
let x be object;
assume
A8: x in A;
then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:5;
(o.:(f,g)).x = o.(a,b) & (A --> the_unity_wrt o).x = the_unity_wrt o
by A5,A8,FUNCOP_1:7,22;
hence f.x = g.x by A2,A4,A6,A3;
end;
A9: now
let x be object;
assume
A10: x in A;
then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:5;
(o.:(f,g)).x = o.(a,b) & (A --> the_unity_wrt o).x = the_unity_wrt o
by A5,A10,FUNCOP_1:7,22;
hence g.x = (A --> the_unity_wrt o).x by A2,A4,A6,A3;
end;
A11: dom g = A by FUNCT_2:def 1;
dom f = A by FUNCT_2:def 1;
hence f = g by A11,A7,FUNCT_1:2;
dom (A --> the_unity_wrt o) = A;
hence thesis by A3,A11,A9,FUNCT_1:2;
end;
theorem
o absorbs o9 implies (o,D).:A absorbs (o9,D).:A
proof
assume
A1: o.(a,o9.(a,b)) = a;
let f,g be Element of Funcs(A,D);
A2: dom (o.:(f,o9.:(f,g))) = A by FUNCT_2:def 1;
A3: dom (o9.:(f,g)) = A by FUNCT_2:def 1;
A4: now
let x be object;
assume
A5: x in A;
then reconsider a = f.x, b = g.x as Element of D by FUNCT_2:5;
(o.:(f,o9.:(f,g))).x = o.(a,(o9.:(f,g)).x) & (o9.:(f,g)).x = o9.(a,b )
by A3,A2,A5,FUNCOP_1:22;
hence f.x = (o.:(f,o9.:(f,g))).x by A1;
end;
A6: dom f = A by FUNCT_2:def 1;
((o9,D).:A).(f,g) = o9.:(f,g) & ((o,D).:A).(f,o9.:(f,g)) = o.:(f,o9.: (f
,g)) by Def2;
hence thesis by A6,A2,A4,FUNCT_1:2;
end;
theorem Th16:
for D1, D2, D, E1, E2, E being non empty set, o1 being Function
of [:D1, D2:], D, o2 being Function of [:E1, E2:], E st o1 c= o2
holds (o1,D).:A c= (o2,E).:A
proof
let D1, D2, D, E1, E2, E be non empty set, o1 be Function of [:D1, D2:], D,
o2 be Function of [:E1, E2:], E;
A1: dom o1 = [:D1,D2:] by FUNCT_2:def 1;
assume
A2: o1 c= o2;
then
A3: dom o1 c= dom o2 by GRFUNC_1:2;
A4: dom o2 = [:E1,E2:] by FUNCT_2:def 1;
then D2 c= E2 by A3,A1,ZFMISC_1:114;
then
A5: Funcs(A,D2) c= Funcs(A,E2) by FUNCT_5:56;
D1 c= E1 by A3,A1,A4,ZFMISC_1:114;
then
A6: Funcs(A,D1) c= Funcs(A,E1) by FUNCT_5:56;
A7: now
let x be object;
assume x in dom (o1,D).:A;
then reconsider y = x as Element of [:Funcs(A,D1),Funcs(A,D2):];
reconsider g2 = y`2 as Element of Funcs(A,E2) by A5;
reconsider f2 = y`2 as Element of Funcs(A,D2);
reconsider g1 = y`1 as Element of Funcs(A,E1) by A6;
reconsider f1 = y`1 as Element of Funcs(A,D1);
A8: dom (o2.:(g1,g2)) = A & dom (o1.:(f1,f2)) = A by FUNCT_2:def 1;
A9: dom f1 = A & dom f2 = A by FUNCT_2:def 1;
A10: now
let z be object;
assume
A11: z in A;
then f1.z in rng f1 & f2.z in rng f2 by A9,FUNCT_1:def 3;
then
A12: [f1.z,f2.z] in dom o1 by A1,ZFMISC_1:87;
(o2.:(g1,g2)).z = o2.(g1.z,g2.z) & (o1.:(f1,f2)).z = o1.(f1.z, f2.
z) by A8,A11,FUNCOP_1:22;
hence (o2.:(g1,g2)).z = (o1.:(f1,f2)).z by A2,A12,GRFUNC_1:2;
end;
A13: [f1,f2] = x by MCART_1:21;
((o1,D).:A).(f1,f2) = o1.:(f1,f2) & ((o2,E).:A).(g1,g2) = o2.:(g1,g2)
by Def2;
hence ((o1,D).:A).x = ((o2,E).:A).x by A8,A10,A13,FUNCT_1:2;
end;
dom (o1,D).:A = [:Funcs(A,D1),Funcs(A,D2):] & dom (o2,E).:A = [:Funcs(A,
E1), Funcs(A,E2):] by FUNCT_2:def 1;
then dom (o1,D).:A c= dom (o2,E).:A by A6,A5,ZFMISC_1:96;
hence thesis by A7,GRFUNC_1:2;
end;
definition
let G be non empty multMagma;
let A be set;
func .:(G,A) -> multMagma equals
: Def3:
multLoopStr (# Funcs(A, the carrier
of G), (the multF of G,the carrier of G).:A, A --> the_unity_wrt the multF of G
#) if G is unital otherwise multMagma (# Funcs(A, the carrier of G), (the multF
of G,the carrier of G).:A #);
correctness;
end;
registration
let G be non empty multMagma;
let A be set;
cluster .:(G,A) -> non empty;
coherence
proof
per cases;
suppose
G is unital;
then
.:(G,A) = multLoopStr (# Funcs(A, the carrier of G), (the multF of G
,the carrier of G).:A, (A --> the_unity_wrt the multF of G)#) by Def3;
hence the carrier of .:(G,A) is non empty;
end;
suppose
G is not unital;
then
.:(G,A) = multMagma (# Funcs(A, the carrier of G), (the multF of G,
the carrier of G).:A #) by Def3;
hence the carrier of .:(G,A) is non empty;
end;
end;
end;
reserve G for non empty multMagma;
deffunc carr(non empty multMagma) = the carrier of $1;
theorem Th17:
the carrier of .:(G,X) = Funcs(X, the carrier of G) & the multF
of .:(G,X) = (the multF of G, the carrier of G).:X
proof
A1: not G is unital implies .:(G,X) = multMagma(#Funcs(X, carr(G)), (op(G),
carr(G)).:X#) by Def3;
G is unital implies .:(G,X) = multLoopStr(#Funcs(X, carr(G)), (op(G),
carr(G)).:X, (X --> the_unity_wrt op(G))#) by Def3;
hence thesis by A1;
end;
theorem
x is Element of .: (G,X) iff x is Function of X, the carrier of G
proof
x is Element of .:(G,X) implies x is Element of Funcs(X, carr(G)) by Th17;
hence x is Element of .:(G,X) implies x is Function of X, carr(G);
assume x is Function of X, carr(G);
then reconsider f = x as Function of X, carr(G);
A1: rng f c= carr(G);
carr(.:(G,X)) = Funcs(X, carr(G)) & dom f = X by Th17,FUNCT_2:def 1;
hence thesis by A1,FUNCT_2:def 2;
end;
Lm1: .:(G,X) is constituted-Functions
proof
let a be Element of .:(G,X);
a is Element of Funcs(X,carr(G)) by Th17;
hence thesis;
end;
registration
let G be non empty multMagma, A be set;
cluster .:(G,A) -> constituted-Functions;
coherence by Lm1;
end;
theorem Th19:
for f being Element of .:(G,X) holds dom f = X & rng f c= the carrier of G
proof
let f be Element of .:(G,X);
reconsider f as Element of Funcs(X, carr(G)) by Th17;
f = f;
hence thesis by FUNCT_2:def 1,RELAT_1:def 19;
end;
theorem Th20:
for f,g being Element of .:(G,X) st
for x being object st x in X holds f.x = g.x holds f = g
proof
let f,g be Element of .:(G,X);
dom f = X & dom g = X by Th19;
hence thesis by FUNCT_1:2;
end;
definition
let G be non empty multMagma, A be non empty set;
let f be Element of .:(G,A);
let a be Element of A;
redefine func f.a -> Element of G; :: redefines . (FUNCT_1, definition)
coherence
proof
dom f = A by Th19;
then
A1: f.a in rng f by FUNCT_1:def 3;
rng f c= carr(G) by Th19;
hence thesis by A1;
end;
end;
registration
let G be non empty multMagma, A be non empty set;
let f be Element of .:(G,A);
cluster rng f -> non empty;
coherence
proof
set a = the Element of A;
dom f = A by Th19;
then f.a in rng f by FUNCT_1:def 3;
hence thesis;
end;
end;
theorem Th21:
for f1,f2 being Element of .:(G,D), a being Element of D holds (
f1*f2).a = (f1.a)*(f2.a)
proof
let f1,f2 be Element of .:(G,D), a be Element of D;
reconsider g1 = f1, g2 = f2 as Element of Funcs(D, carr(G)) by Th17;
op(.:(G,D)) = (op(G),carr(G)).:D by Th17;
then dom (op(G).:(g1,g2)) = D & f1*f2 = op(G).:(g1,g2) by Def2,FUNCT_2:def 1;
hence thesis by FUNCOP_1:22;
end;
definition
let G be unital non empty multMagma;
let A be set;
redefine func .:(G,A) -> well-unital constituted-Functions strict non empty :: redefines .: (MONOID_1, definition)
multLoopStr;
coherence
proof
set M = multLoopStr(#Funcs(A, carr(G)), (op(G),carr(G)).:A, (A -->
the_unity_wrt op(G))#);
op(G) is having_a_unity by MONOID_0:def 10;
then consider a being Element of G such that
A1: a is_a_unity_wrt op(G);
A2: 1.M = A --> the_unity_wrt the multF of G & .:(G,A) = M by Def3;
a = the_unity_wrt op(G) & A --> a is_a_unity_wrt (op(G),carr(G)).:A by A1
,Th9,BINOP_1:def 8;
hence thesis by A2,MONOID_0:def 21;
end;
end;
theorem Th22:
for G being unital non empty multMagma holds 1..:(G,X) = X -->
the_unity_wrt the multF of G
proof
let G be unital non empty multMagma;
.:(G,X) = multLoopStr(#Funcs(X, carr(G)), (op(G), carr(G)).:X, (X -->
the_unity_wrt op(G))#) by Def3;
hence thesis;
end;
theorem Th23:
for G being non empty multMagma, A being set holds (G is
commutative implies .:(G,A) is commutative) & (G is associative implies .:(G,A)
is associative) & (G is idempotent implies .:(G,A) is idempotent) & (G is
invertible implies .:(G,A) is invertible) & (G is cancelable implies .:(G,A) is
cancelable) & (G is uniquely-decomposable implies .:(G,A) is
uniquely-decomposable)
proof
let G;
let A be set;
A1: op(.:(G,A)) = (op(G), carr(G)).:A & carr(.:(G,A)) = Funcs(A, carr(G)) by
Th17;
thus G is commutative implies .:(G,A) is commutative
by A1,Th7;
thus G is associative implies .:(G,A) is associative
by A1,Th8;
thus G is idempotent implies .:(G,A) is idempotent
by A1,Th11;
thus G is invertible implies .:(G,A) is invertible
by A1,Th12;
thus G is cancelable implies .:(G,A) is cancelable
by A1,Th13;
assume op(G) is uniquely-decomposable;
hence op(.:(G,A)) is uniquely-decomposable by A1,Th14;
end;
theorem
for H being non empty SubStr of G holds .:(H,X) is SubStr of .:(G,X)
proof
let H be non empty SubStr of G;
A1: op(.:(H,X)) = (op(H), carr(H)).:X by Th17;
op(H) c= op(G) & op(.:(G,X)) = (op(G), carr(G)).:X by Th17,MONOID_0:def 23;
hence op(.:(H,X)) c= op(.:(G,X)) by A1,Th16;
end;
theorem
for G being unital non empty multMagma, H being non empty SubStr of
G st the_unity_wrt the multF of G in the carrier of H holds .:(H,X) is
MonoidalSubStr of .:(G,X)
proof
let G be unital non empty multMagma, H be non empty SubStr of G;
assume
A1: the_unity_wrt the multF of G in carr(H);
then reconsider G9 = G, H9 = H as unital non empty multMagma by MONOID_0:30;
A2: the_unity_wrt op(H9) = the_unity_wrt op(G9) by A1,MONOID_0:30;
A3: op(.:(H,X)) = (op(H), carr(H)).:X by Th17;
op(H) c= op(G) & op(.:(G,X)) = (op(G), carr(G)).:X by Th17,MONOID_0:def 23;
then
A4: op(.:(H,X)) c= op(.:(G,X)) by A3,Th16;
1..:(G9,X) = X --> the_unity_wrt op(G) & 1..:(H9,X) = X -->
the_unity_wrt op (H) by Th22;
hence thesis by A2,A4,MONOID_0:def 25;
end;
definition
let G be unital associative commutative cancelable uniquely-decomposable
non empty multMagma;
let A be set;
redefine func .:(G,A) -> commutative cancelable uniquely-decomposable :: redefines .: (MONOID_1, definition)
constituted-Functions strict Monoid;
coherence
proof
.:(G,A) is commutative cancelable by Th23;
hence thesis by Th23;
end;
end;
begin :: Monoid of multisets over a set
definition
let A be set;
func MultiSet_over A -> commutative cancelable uniquely-decomposable
constituted-Functions strict Monoid equals
.:(<NAT,+,0>, A);
correctness;
end;
theorem Th26:
the carrier of MultiSet_over X = Funcs(X,NAT) & the multF of
MultiSet_over X = (addnat,NAT).:X & 1.MultiSet_over X = X --> 0
proof
the multMagma of <NAT,+,0> = <NAT,+> & the_unity_wrt op(<NAT,+>) = 0 by
MONOID_0:40,def 22;
hence thesis by Th17,Th22,MONOID_0:46;
end;
definition
let A be set;
mode Multiset of A is Element of MultiSet_over A;
end;
theorem Th27:
x is Multiset of X iff x is Function of X,NAT
proof
A1: now
let x be Function of X,NAT;
dom x = X & rng x c= NAT by FUNCT_2:def 1;
hence x is Element of Funcs(X,NAT) by FUNCT_2:def 2;
end;
x is Multiset of X iff x is Element of Funcs(X,NAT) by Th26;
hence thesis by A1;
end;
theorem Th28:
for m being Multiset of X holds dom m = X & rng m c= NAT
proof
let m be Multiset of X;
m is Function of X,NAT by Th27;
hence thesis by FUNCT_2:def 1,RELAT_1:def 19;
end;
registration
let X;
cluster -> NAT-valued for Multiset of X;
coherence by Th28;
end;
theorem Th29:
for m1,m2 being Multiset of D, a being Element of D holds
(m1 [*] m2).a = (m1.a)+(m2.a)
proof
reconsider N = <NAT,+,0> as non empty multMagma;
let m1,m2 be Multiset of D, a be Element of D;
reconsider f1 = m1, f2 = m2 as Element of .:(N,D);
thus (m1 [*] m2).a = (f1.a)*(f2.a) by Th21
.= (m1.a)+(m2.a) by MONOID_0:45;
end;
theorem Th30:
chi(Y,X) is Multiset of X
proof
rng chi(Y,X) c= {0,1};
then
A1: rng chi(Y,X) c= NAT by XBOOLE_1:1;
dom chi(Y,X) = X & carr(MultiSet_over X) = Funcs(X,NAT)
by Th26,FUNCT_3:def 3;
hence thesis by A1,FUNCT_2:def 2;
end;
definition
let Y,X;
redefine func chi(Y,X) -> Multiset of X; :: redefines chi (FUNCT_3, definition)
coherence by Th30;
end;
definition
let X;
let n be Element of NAT;
redefine func X --> n -> Multiset of X; :: redefines --> (FUNCOP_1, definition)
coherence
proof
thus X --> n is Multiset of X by Th27;
end;
end;
definition
let A be non empty set, a be Element of A;
func chi a -> Multiset of A equals
chi({a},A);
coherence;
end;
theorem Th31:
for A being non empty set, a,b being Element of A holds
(chi a).a = 1 & (b <> a implies (chi a).b = 0)
proof
let A be non empty set, a,b be Element of A;
A1: b <> a implies not b in {a} by TARSKI:def 1;
a in {a} by TARSKI:def 1;
hence thesis by A1,FUNCT_3:def 3;
end;
reserve A for non empty set,
a for Element of A,
p for FinSequence of A,
m1,m2 for Multiset of A;
theorem Th32:
(for a holds m1.a = m2.a) implies m1 = m2
proof
assume for a holds m1.a = m2.a;
then for x being object st x in A holds m1.x = m2.x;
hence thesis by Th20;
end;
definition
let A be set;
func finite-MultiSet_over A -> strict non empty MonoidalSubStr of
MultiSet_over A means
: Def6:
for f being Multiset of A holds f in the carrier
of it iff f"(NAT\{0}) is finite;
existence
proof
reconsider e = A --> 0 as Function of A,NAT by Th27;
defpred P[set] means ex f being Function of A,NAT st $1 = f & f"(NAT\{0})
is finite;
A1: for a,b being Multiset of A holds P[a] & P[b] implies P[a [*] b]
proof
let a,b be Multiset of A;
reconsider h = a [*] b as Function of A,NAT by Th27;
given f being Function of A,NAT such that
A2: a = f and
A3: f"(NAT\{0}) is finite;
given g being Function of A,NAT such that
A4: b = g and
A5: g"(NAT\{0}) is finite;
take h;
A6: dom f = A & dom g = A by FUNCT_2:def 1;
h"(NAT\{0}) c= (f"(NAT\{0})) \/ (g"(NAT\{0}))
proof
let x be object;
assume
A7: x in h"(NAT\{0});
then h.x in NAT\{0} by FUNCT_1:def 7;
then
A8: not h.x in {0} by XBOOLE_0:def 5;
f.x in rng f & g.x in rng g by A6,A7,FUNCT_1:def 3;
then reconsider n = f.x, m = g.x as Element of NAT;
h.x = n+m by A2,A4,A7,Th29;
then n <> 0 or m <> 0 by A8,TARSKI:def 1;
then not n in {0} or not m in {0} by TARSKI:def 1;
then n in NAT\{0} or m in NAT\{0} by XBOOLE_0:def 5;
then x in f"(NAT\{0}) or x in g"(NAT\{0}) by A6,A7,FUNCT_1:def 7;
hence thesis by XBOOLE_0:def 3;
end;
hence thesis by A3,A5;
end;
A9: dom e = A;
now
set x = the Element of e"(NAT\{0});
assume
A10: e"(NAT\{0}) <> {};
then e.x in NAT\{0} by FUNCT_1:def 7;
then
A11: not e.x in {0} by XBOOLE_0:def 5;
x in A by A9,A10,FUNCT_1:def 7;
then e.x = 0 by FUNCOP_1:7;
hence contradiction by A11,TARSKI:def 1;
end;
then
A12: P[1.MultiSet_over A] by Th26;
consider M being strict non empty MonoidalSubStr of MultiSet_over A such
that
A13: for a being Multiset of A holds a in the carrier of M iff P[a]
from MONOID_0:sch 2(A1,A12);
reconsider M as strict non empty MonoidalSubStr of MultiSet_over A;
take M;
let f be Multiset of A;
thus f in carr(M) implies f"(NAT\{0}) is finite
proof
assume f in carr(M);
then ex g being Function of A,NAT st f = g & g"(NAT\{0}) is finite by A13
;
hence thesis;
end;
reconsider g = f as Function of A,NAT by Th27;
assume f"(NAT\{0}) is finite;
then g"(NAT\{0}) is finite;
hence thesis by A13;
end;
uniqueness
proof
set M = MultiSet_over A;
let M1,M2 be strict non empty MonoidalSubStr of MultiSet_over A such that
A14: for f being Multiset of A holds f in carr(M1) iff f"(NAT\{0}) is
finite and
A15: for f being Multiset of A holds f in carr(M2) iff f"(NAT\{0}) is finite;
A16: carr(M2) c= carr(M) by MONOID_0:23;
A17: carr(M1) c= carr(M) by MONOID_0:23;
carr(M1) = carr(M2)
proof
thus carr(M1) c= carr(M2)
proof
let x be object;
assume
A18: x in carr(M1);
then reconsider f = x as Multiset of A by A17;
f"(NAT\{0}) is finite by A14,A18;
hence thesis by A15;
end;
let x be object;
assume
A19: x in carr(M2);
then reconsider f = x as Multiset of A by A16;
f"(NAT\{0}) is finite by A15,A19;
hence thesis by A14;
end;
hence thesis by MONOID_0:27;
end;
end;
theorem Th33:
chi a is Element of finite-MultiSet_over A
proof
(chi a)"(NAT\{0}) c= {a}
proof
let x be object;
assume
A1: x in (chi a)"(NAT\{0});
then x in dom chi a by FUNCT_1:def 7;
then reconsider y = x as Element of A by Th28;
(chi a).x in NAT\{0} by A1,FUNCT_1:def 7;
then not (chi a).y in {0} by XBOOLE_0:def 5;
then (chi a).y <> 0 by TARSKI:def 1;
then y = a by Th31;
hence thesis by TARSKI:def 1;
end;
hence thesis by Def6;
end;
theorem Th34:
dom ({x}|`(p^<*x*>)) = dom ({x}|`p) \/ {len p+1}
proof
thus dom ({x}|`(p^<*x*>)) c= dom ({x}|`p) \/ {len p+1}
proof
let a be object;
A1: len <*x*> = 1 by FINSEQ_1:40;
A2: Seg len p = dom p by FINSEQ_1:def 3;
assume
A3: a in dom ({x}|`(p^<*x*>));
then
A4: a in dom (p^<*x*>) by FUNCT_1:54;
then a in Seg (len p+len <*x*>) by FINSEQ_1:def 7;
then a in Seg len p \/ {len p+1} by A1,FINSEQ_1:9;
then
A5: a in dom p or a in {len p+1} by A2,XBOOLE_0:def 3;
A6: (p^<*x*>).a in {x} by A3,FUNCT_1:54;
reconsider a as Element of NAT by A4;
a in dom p implies (p^<*x*>).a = p.a by FINSEQ_1:def 7;
then a in dom p implies a in dom ({x}|`p) by A6,FUNCT_1:54;
hence thesis by A5,XBOOLE_0:def 3;
end;
let a be object;
len <*x*> = 1 by FINSEQ_1:40;
then
A7: dom (p^<*x*>) = Seg (len p+1) by FINSEQ_1:def 7;
assume
A8: a in dom ({x}|`p) \/ {len p+1};
then a in dom ({x}|`p) or a in {len p+1} by XBOOLE_0:def 3;
then
A9: a in dom p & p.a in {x} or a in {len p+1} & a = len p+1 & x in {x} by
FUNCT_1:54,TARSKI:def 1;
Seg len p = dom p & Seg (len p+1) = Seg len p \/ {len p+1} by FINSEQ_1:9
,def 3;
then
A10: (p^<*x*>).(len p+1) = x & a in dom (p^<*x*>) by A9,A7,FINSEQ_1:42
,XBOOLE_0:def 3;
reconsider a as Element of NAT by A8;
a in dom p implies (p^<*x*>).a = p.a by FINSEQ_1:def 7;
hence thesis by A9,A10,FUNCT_1:54;
end;
theorem Th35:
x <> y implies dom ({x}|`(p^<*y*>)) = dom ({x}|`p)
proof
assume
A1: x <> y;
thus dom ({x}|`(p^<*y*>)) c= dom ({x}|`p)
proof
let a be object;
A2: len <*y*> = 1 by FINSEQ_1:40;
A3: Seg len p = dom p by FINSEQ_1:def 3;
assume
A4: a in dom ({x}|`(p^<*y*>));
then
A5: a in dom (p^<*y*>) by FUNCT_1:54;
then a in Seg (len p+len <*y*>) by FINSEQ_1:def 7;
then a in Seg len p \/ {len p+1} by A2,FINSEQ_1:9;
then
A6: a in dom p or a in {len p+1} by A3,XBOOLE_0:def 3;
A7: (p^<*y*>).a in {x} by A4,FUNCT_1:54;
reconsider a as Element of NAT by A5;
A8: (p^<*y*>).(len p+1) = y & not y in {x} by A1,FINSEQ_1:42,TARSKI:def 1;
then (p^<*y*>).a = p.a by A7,A6,FINSEQ_1:def 7,TARSKI:def 1;
hence thesis by A7,A6,A8,FUNCT_1:54,TARSKI:def 1;
end;
let a be object;
assume
A9: a in dom ({x}|`p);
then
A10: a in dom p by FUNCT_1:54;
len <*y*> = 1 by FINSEQ_1:40;
then
A11: dom (p^<*y*>) = Seg (len p+1) by FINSEQ_1:def 7;
Seg len p = dom p & Seg (len p+1) = Seg len p \/ {len p+1} by FINSEQ_1:9
,def 3;
then
A12: a in dom (p^<*y*>) by A10,A11,XBOOLE_0:def 3;
A13: p.a in {x} by A9,FUNCT_1:54;
reconsider a as Element of NAT by A9;
(p^<*y*>).a = p.a by A10,FINSEQ_1:def 7;
hence thesis by A13,A12,FUNCT_1:54;
end;
definition
let A be non empty set, p be FinSequence of A;
func |.p.| -> Multiset of A means
: Def7:
for a being Element of A holds it. a = card dom ({a}|`p);
existence
proof
deffunc F(Element of A)=card dom ({$1}|`p);
consider m being Function of A,NAT such that
A1: for a being Element of A holds m.a = F(a) from FUNCT_2:sch 4;
m is Multiset of A by Th27;
hence thesis by A1;
end;
uniqueness
proof
let m1, m2 be Multiset of A such that
A2: for a being Element of A holds m1.a = card dom ({a}|`p) and
A3: for a being Element of A holds m2.a = card dom ({a}|`p);
now
let a be Element of A;
thus m1.a = card dom ({a}|`p) by A2
.= m2.a by A3;
end;
hence thesis by Th32;
end;
end;
theorem
|.<*> A.|.a = 0
proof
dom ({a}|`{}) c= dom {} by FUNCT_1:56;
then dom ({a}|`<*> A) = {};
hence thesis by Def7,CARD_1:27;
end;
theorem Th37:
|.<*> A.| = A --> 0
proof
A1: now
let x be object;
assume x in A;
then reconsider a = x as Element of A;
thus |.<*>A.|.x = card dom ({a}|`{}) by Def7
.= 0 by CARD_1:27,RELAT_1:38,107;
end;
dom |.<*>A.| = A by Th28;
hence thesis by A1,FUNCOP_1:11;
end;
theorem
|.<*a*>.| = chi a
proof
A1: rng <*a*> = {a} by FINSEQ_1:39;
now
let b be Element of A;
set x = b;
A2: dom <*a*> = Seg 1 & card Seg 1 = 1 by FINSEQ_1:38,57;
a <> x implies {x} misses {a} by ZFMISC_1:11;
then
A3: a <> x implies {x}/\{a} = {};
A4: (chi a).a = 1 & {a}|`<*a*> = <*a*> by A1,Th31;
<*a*> = (rng<*a*>)|`<*a*>;
then {x}|`<*a*> = ({x}/\rng<*a*>)|`<*a*> by RELAT_1:96;
then x <> a implies {x}|`<*a*> = {} & (chi a).b = 0 by A1,A3,Th31;
hence |.<*a*>.|.x = (chi a).x by A2,A4,Def7,CARD_1:27,RELAT_1:38;
end;
hence thesis by Th32;
end;
reserve p,q for FinSequence of A;
theorem Th39:
|.p^<*a*>.| = |.p.| [*] chi a
proof
now
reconsider pa = p^<*a*> as FinSequence of A;
let b be Element of A;
len p < len p+1 & dom ({b}|`p) c= dom p by FUNCT_1:56,NAT_1:13;
then
A1: not len p+1 in dom ({b}|`p) by FINSEQ_3:25;
A2: |.p^<*a*>.|.b = card dom ({b}|`pa) & |.p.|.b = card dom ({b}|`p) by Def7;
A3: a <> b implies dom ({b}|`(p^<*a*>)) = dom ({b}|`p) & (chi a).b = 0 by Th31
,Th35;
A4: (|.p.| [*] chi a).b = (|.p.|.b) + ((chi a).b) by Th29;
dom ({a}|`(p^<*a*>)) = dom ({a}|`p) \/ {len p+1} & (chi a).a = 1
by Th31,Th34;
hence |.p^<*a*>.|.b = (|.p.| [*] chi a).b by A1,A2,A3,A4,CARD_2:41;
end;
hence thesis by Th32;
end;
theorem Th40:
|.p^q.| = |.p.|[*]|.q.|
proof
defpred P[Nat] means for q st len q = $1 holds |.p^q.| = |.p.|[*]
|.q.|;
A1: len q = len q;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A3: for q st len q = n holds |.p^q.| = |.p.|[*]|.q.|;
let q;
assume
A4: len q = n+1;
then q <> {};
then consider r being FinSequence, x being object such that
A5: q = r^<*x*> by FINSEQ_1:46;
rng <*x*> = {x} by FINSEQ_1:39;
then {x} c= rng q by A5,FINSEQ_1:30;
then
A6: {x} c= A by XBOOLE_1:1;
reconsider r as FinSequence of A by A5,FINSEQ_1:36;
len <*x*> = 1 by FINSEQ_1:40;
then
A7: n+1 = len r+1 by A4,A5,FINSEQ_1:22;
reconsider x as Element of A by A6,ZFMISC_1:31;
thus |.p^q.| = |.p^r^<*x*>.| by A5,FINSEQ_1:32
.= |.p^r.|[*] chi x by Th39
.= |.p.|[*]|.r.|[*] chi x by A3,A7
.= |.p.|[*](|.r.|[*] chi x) by GROUP_1:def 3
.= |.p.|[*]|.q.| by A5,Th39;
end;
A8: P[0]
proof
let q;
A9: |.<*>A.| = A-->0 & A-->0 = un(MultiSet_over A) by Th26,Th37;
assume len q = 0;
then
A10: q = {};
then p^q = p by FINSEQ_1:34;
hence thesis by A10,A9,MONOID_0:16;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A8,A2);
hence thesis by A1;
end;
theorem Th41:
|.n .--> a.|.a = n & for b being Element of A st b <> a holds |.
n .--> a.|.b = 0
proof
defpred P[Nat] means |.In($1,NAT) .--> a.|.a = $1;
A1: 0.-->a = {} & {} = <*>A by FINSEQ_2:58;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A3: |.In(n,NAT) .--> a.|.a = n;
thus |.In(n+1,NAT) .--> a.|.a
= |.(In(n,NAT) .--> a)^<*a*>.|.a by FINSEQ_2:60
.= (|.In(n,NAT) .--> a.|[*]chi a).a by Th39
.= n+(chi a).a by A3,Th29
.= n+1 by Th31;
end;
(A-->0).a = 0;
then
A4: P[0] by A1,Th37;
for n being Nat holds P[n] from NAT_1:sch 2(A4,A2);
then |.In(n,NAT) .--> a.|.a = n;
hence |.n .--> a.|.a = n;
let b be Element of A such that
A5: b <> a;
defpred P[Nat] means |.In($1,NAT) .--> a.|.b = 0;
A6: for n being Nat st P[n] holds P[(n+1)]
proof
let n be Nat such that
A7: |.In(n,NAT) .--> a.|.b = 0;
thus |.In(n+1,NAT) .--> a.|.b
= |.(In(n,NAT) .--> a)^<*a*>.|.b by FINSEQ_2:60
.= (|.In(n,NAT) .--> a.|[*]chi a).b by Th39
.= 0+(chi a).b by A7,Th29
.= 0 by A5,Th31;
end;
(A-->0).b = 0;
then
A8: P[0] by A1,Th37;
for n being Nat holds P[n] from NAT_1:sch 2(A8,A6);
then P[n];
hence thesis;
end;
reserve fm for Element of finite-MultiSet_over A;
theorem
|.p.| is Element of finite-MultiSet_over A
proof
defpred P[FinSequence of A] means |.$1.| is Element of finite-MultiSet_over
A;
defpred Q[Nat] means for p st len p = $1 holds P[p];
A1: len p = len p;
A2: for n being Nat st Q[n] holds Q[n+1]
proof
set M = finite-MultiSet_over A;
let n be Nat such that
A3: for p st len p = n holds P[p];
let p;
assume
A4: len p = n+1;
then p <> {};
then consider r being FinSequence, x being object such that
A5: p = r^<*x*> by FINSEQ_1:46;
rng <*x*> = {x} by FINSEQ_1:39;
then {x} c= rng p by A5,FINSEQ_1:30;
then
A6: {x} c= A by XBOOLE_1:1;
reconsider r as FinSequence of A by A5,FINSEQ_1:36;
A7: len <*x*> = 1 by FINSEQ_1:40;
reconsider x as Element of A by A6,ZFMISC_1:31;
n+1 = len r+1 by A4,A5,A7,FINSEQ_1:22;
then reconsider r9 = |.r.|, a = chi x as Element of M by A3,Th33;
M is SubStr of MultiSet_over A by MONOID_0:21;
then r9[*]a = |.r.|[*]chi x by MONOID_0:25
.= |.p.| by A5,Th39;
hence thesis;
end;
A8: Q[0]
proof
let p;
assume len p = 0;
then p = <*> A;
then |.p.| = A --> 0 by Th37
.= un(MultiSet_over A) by Th26
.= un(finite-MultiSet_over A) by MONOID_0:def 24;
hence thesis;
end;
for n being Nat holds Q[n] from NAT_1:sch 2(A8,A2);
hence thesis by A1;
end;
theorem
x is Element of finite-MultiSet_over A implies ex p st x = |.p.|
proof
defpred Z[Nat] means for fm st for V being finite set st V = fm"(
NAT\{0}) holds card V = $1 ex p st fm = |.p.|;
assume x is Element of finite-MultiSet_over A;
then reconsider m = x as Element of finite-MultiSet_over A;
carr(finite-MultiSet_over A) c= carr(MultiSet_over A) by MONOID_0:23;
then m is Multiset of A;
then reconsider V = m"(NAT\{0}) as finite set by Def6;
A1: for V9 being finite set st V9 = m"(NAT\{0}) holds card V9 = card V;
A2: for n being Nat st Z[n] holds Z[n+1]
proof
deffunc F(object) = 0;
let n be Nat such that
A3: for fm st for V being finite set st V = fm"(NAT\{0}) holds card V
= n ex p st fm = |.p.|;
let fm such that
A4: for V being finite set st V = fm"(NAT\{0}) holds card V = n+1;
deffunc G(object) = fm.$1;
set x = the Element of fm"(NAT\{0});
carr(finite-MultiSet_over A) c= carr(MultiSet_over A) by MONOID_0:23;
then reconsider m = fm as Multiset of A;
reconsider V = m"(NAT\{0}) as finite set by Def6;
A5: card V = n+1 by A4;
A6: dom m = A by Th28;
then reconsider x as Element of A by A5,CARD_1:27,FUNCT_1:def 7;
defpred C[object] means x = $1;
consider f being Function such that
A7: dom f = A & for a being object st a in A holds (C[a] implies f.a = F
(a)) & (not C[a] implies f.a = G(a)) from PARTFUN1:sch 1;
rng f c= NAT
proof
let y be object;
assume y in rng f;
then consider z being object such that
A8: z in dom f and
A9: y = f.z by FUNCT_1:def 3;
reconsider z as Element of A by A7,A8;
y = 0 or y = m.z by A7,A9;
hence thesis;
end;
then reconsider f as Function of A,NAT by A7,FUNCT_2:def 1,RELSET_1:4;
reconsider f as Multiset of A by Th27;
A10: f"(NAT\{0}) = (fm"(NAT\{0}))\{x}
proof
thus f"(NAT\{0}) c= (fm"(NAT\{0}))\{x}
proof
let y be object;
assume
A11: y in f"(NAT\{0});
then reconsider a = y as Element of A by A7,FUNCT_1:def 7;
A12: f.y in NAT\{0} by A11,FUNCT_1:def 7;
then not f.a in {0} by XBOOLE_0:def 5;
then
A13: f.a <> 0 by TARSKI:def 1;
then a <> x by A7;
then
A14: not a in {x} by TARSKI:def 1;
f.a = fm.a by A7,A13;
then a in fm"(NAT\{0}) by A6,A12,FUNCT_1:def 7;
hence thesis by A14,XBOOLE_0:def 5;
end;
let y be object;
assume
A15: y in (fm"(NAT\{0}))\{x};
then
A16: y in dom fm by FUNCT_1:def 7;
A17: fm.y in NAT\{0} by A15,FUNCT_1:def 7;
not y in {x} by A15,XBOOLE_0:def 5;
then y <> x by TARSKI:def 1;
then fm.y = f.y by A6,A7,A16;
hence thesis by A6,A7,A16,A17,FUNCT_1:def 7;
end;
then reconsider f9 = f as Element of finite-MultiSet_over A by A5,Def6;
set g = |.(m.x) .--> x.|;
A18: card {x} = 1 by CARD_1:30;
reconsider V9 = f9"(NAT\{0}) as finite set by Def6;
{x} c= fm"(NAT\{0}) by A5,CARD_1:27,ZFMISC_1:31;
then card V9 = n+1-1 by A5,A10,A18,CARD_2:44
.= n;
then for V being finite set st V = f9"(NAT\{0}) holds card V = n;
then consider p such that
A19: f = |.p.| by A3;
take q = p^((m.x) .--> x);
now
let a;
A20: 0 + m.a = m.a;
A21: a <> x implies f.a = m.a & g.a = 0 by A7,Th41;
f.x = 0 & g.x = m.x by A7,Th41;
hence (f[*]g).a = m.a by A20,A21,Th29;
end;
hence fm = f[*]g by Th32
.= |.q.| by A19,Th40;
end;
A22: Z[0]
proof
set a = the Element of A;
let fm such that
A23: for V being finite set st V = fm"(NAT\{0}) holds card V = 0;
carr(finite-MultiSet_over A) c= carr(MultiSet_over A) by MONOID_0:23;
then reconsider m = fm as Multiset of A;
reconsider V = m"(NAT\{0}) as finite set by Def6;
card V = 0 by A23;
then fm"(NAT\{0}) = {};
then rng fm misses (NAT\{0}) by RELAT_1:138;
then
A24: {} = rng fm /\ (NAT\{0})
.= (rng fm /\ NAT)\{0} by XBOOLE_1:49;
take p = <*> A;
rng m c= NAT;
then rng fm /\ NAT = rng fm by XBOOLE_1:28;
then
A25: rng fm c= {0} by A24,XBOOLE_1:37;
A26: dom m = A by Th28;
then
A27: fm.a in rng fm by FUNCT_1:def 3;
then fm.a = 0 by A25,TARSKI:def 1;
then {0} c= rng fm by A27,ZFMISC_1:31;
then rng fm = {0} by A25;
hence fm = A --> 0 by A26,FUNCOP_1:9
.= |.p.| by Th37;
end;
for n being Nat holds Z[n] from NAT_1:sch 2(A22,A2);
hence thesis by A1;
end;
begin :: Monoid of subsets of a semigroup
reserve a,b,c for Element of D;
definition
let D1,D2,D be non empty set, f be Function of [:D1,D2:],D;
func f.:^2 -> Function of [:bool D1, bool D2:], bool D means
: Def8:
for x being Element of [:bool D1, bool D2:] holds it.x = f.:[:x`1,x`2:];
existence
proof
deffunc F(Element of [:bool D1, bool D2:]) = f.:[:$1`1,$1`2:];
ex f being Function of [:bool D1,bool D2:],bool D st
for x being Element
of [:bool D1, bool D2:] holds f.x = F(x) from FUNCT_2:sch 4;
hence thesis;
end;
uniqueness
proof
let F1,F2 be Function of [:bool D1, bool D2:], bool D such that
A1: for x being Element of [:bool D1, bool D2:] holds F1.x = f.:[:x`1,
x`2:] and
A2: for x being Element of [:bool D1, bool D2:] holds F2.x = f.:[:x`1, x`2:];
now
let x be Element of [:bool D1, bool D2:];
thus F1.x = f.:[:x`1,x`2:] by A1
.= F2.x by A2;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem Th44:
for D1,D2,D being non empty set, f being Function of [:D1,D2:],D for
X1 being Subset of D1, X2 being Subset of D2 holds (f.:^2).(X1,X2) = f.:[:X1,X2
:]
proof
let D1,D2,D be non empty set, f be Function of [:D1,D2:],D;
let X1 be Subset of D1, X2 be Subset of D2;
[X1,X2]`1 = X1 & [X1,X2]`2 = X2;
hence thesis by Def8;
end;
theorem Th45:
for D1,D2,D being non empty set, f being Function of [:D1,D2:],D for
X1 being Subset of D1, X2 being Subset of D2, x1,x2 being set st x1 in X1 & x2
in X2 holds f.(x1,x2) in (f.:^2).(X1,X2)
proof
let D1,D2,D be non empty set, f be Function of [:D1,D2:],D;
let X1 be Subset of D1, X2 be Subset of D2, x1,x2 be set;
assume that
A1: x1 in X1 and
A2: x2 in X2;
reconsider b = x2 as Element of D2 by A2;
reconsider a = x1 as Element of D1 by A1;
A3: (f.:^2).(X1,X2) = f.:[:X1,X2:] & dom f = [:D1,D2:] by Th44,FUNCT_2:def 1;
[a,b] in [:X1,X2:] by A1,A2,ZFMISC_1:87;
hence thesis by A3,FUNCT_1:def 6;
end;
theorem
for D1,D2,D being non empty set, f being Function of [:D1,D2:],D for X1
being Subset of D1, X2 being Subset of D2 holds (f.:^2).(X1,X2) = {f.(a,b)
where a is Element of D1, b is Element of D2: a in X1 & b in X2}
proof
let D1,D2,D be non empty set, f be Function of [:D1,D2:],D;
let X1 be Subset of D1, X2 be Subset of D2;
set A = {f.(a,b) where a is Element of D1, b is Element of D2: a in X1 & b
in X2};
A1: (f.:^2).(X1,X2) = f.:[:X1,X2:] by Th44;
thus (f.:^2).(X1,X2) c= A
proof
let x be object;
assume x in f.:^2.(X1,X2);
then consider y being object such that
y in dom f and
A2: y in [:X1,X2:] and
A3: x = f.y by A1,FUNCT_1:def 6;
consider y1,y2 being object such that
A4: y1 in X1 and
A5: y2 in X2 and
A6: y = [y1,y2] by A2,ZFMISC_1:84;
reconsider y2 as Element of D2 by A5;
reconsider y1 as Element of D1 by A4;
x = f.(y1,y2) by A3,A6;
hence thesis by A4,A5;
end;
let x be object;
assume x in A;
then ex a being Element of D1, b being Element of D2 st x = f.(a,b) & a in
X1 & b in X2;
hence thesis by Th45;
end;
theorem Th47:
o is commutative implies o.:[:X,Y:] = o.:[:Y,X:]
proof
assume
A1: o.(a,b) = o.(b,a);
now
let X,Y;
thus o.:[:X,Y:] c= o.:[:Y,X:]
proof
let x be object;
assume x in o.:[:X,Y:];
then consider y being object such that
A2: y in dom o and
A3: y in [:X,Y:] and
A4: x = o.y by FUNCT_1:def 6;
reconsider y as Element of [:D,D:] by A2;
y = [y`1,y`2] by MCART_1:21;
then y`1 in X & y`2 in Y by A3,ZFMISC_1:87;
then
A5: [y`2,y`1] in [:Y,X:] by ZFMISC_1:87;
A6: dom o = [:D,D:] & o.(y`1,y`2) = o.(y`2,y`1 ) by A1,FUNCT_2:def 1;
x = o.(y`1,y`2) by A4,MCART_1:21;
hence thesis by A6,A5,FUNCT_1:def 6;
end;
end;
hence o.:[:X,Y:] c= o.:[:Y,X:] & o.:[:Y,X:] c= o.:[:X,Y:];
end;
theorem Th48:
o is associative implies o.:[:o.:[:X,Y:],Z:] = o.:[:X,o.:[:Y,Z:] :]
proof
A1: dom o = [:D,D:] by FUNCT_2:def 1;
assume
A2: o.(o.(a,b),c) = o.(a,o.(b,c));
thus o.:[:o.:[:X,Y:],Z:] c= o.:[:X,o.:[:Y,Z:]:]
proof
let x be object;
assume x in o.:[:o.:[:X,Y:],Z:];
then consider y being object such that
A3: y in dom o and
A4: y in [:o.:[:X,Y:],Z:] and
A5: x = o.y by FUNCT_1:def 6;
reconsider y as Element of [:D,D:] by A3;
A6: y = [y`1,y`2] by MCART_1:21;
then
A7: y`2 in Z by A4,ZFMISC_1:87;
y`1 in o.:[:X,Y:] by A4,A6,ZFMISC_1:87;
then consider z being object such that
A8: z in dom o and
A9: z in [:X,Y:] and
A10: y`1 = o.z by FUNCT_1:def 6;
reconsider z as Element of [:D,D:] by A8;
A11: y`1 = o.(z`1,z`2) by A10,MCART_1:21;
A12: z = [z`1,z`2] by MCART_1:21;
then z`2 in Y by A9,ZFMISC_1:87;
then [z`2,y`2] in [:Y,Z:] by A7,ZFMISC_1:87;
then
A13: o.(z`2,y`2) in o.:[:Y,Z:] by A1,FUNCT_1:def 6;
z`1 in X by A9,A12,ZFMISC_1:87;
then
A14: [z`1,o.(z`2,y`2)] in [:X,o.:[:Y,Z:]:] by A13,ZFMISC_1:87;
x = o.(y`1,y`2) by A5,MCART_1:21;
then x = o.(z`1,o.(z`2,y`2)) by A2,A11;
hence thesis by A1,A14,FUNCT_1:def 6;
end;
let x be object;
assume x in o.:[:X,o.:[:Y,Z:]:];
then consider y being object such that
A15: y in dom o and
A16: y in [:X,o.:[:Y,Z:]:] and
A17: x = o.y by FUNCT_1:def 6;
reconsider y as Element of [:D,D:] by A15;
A18: y = [y`1,y`2] by MCART_1:21;
then
A19: y`1 in X by A16,ZFMISC_1:87;
y`2 in o.:[:Y,Z:] by A16,A18,ZFMISC_1:87;
then consider z being object such that
A20: z in dom o and
A21: z in [:Y,Z:] and
A22: y`2 = o.z by FUNCT_1:def 6;
reconsider z as Element of [:D,D:] by A20;
A23: y`2 = o.(z`1,z`2) by A22,MCART_1:21;
A24: z = [z`1,z`2] by MCART_1:21;
then z`1 in Y by A21,ZFMISC_1:87;
then [y`1,z`1] in [:X,Y:] by A19,ZFMISC_1:87;
then
A25: o.(y`1,z`1) in o.:[:X,Y:] by A1,FUNCT_1:def 6;
z`2 in Z by A21,A24,ZFMISC_1:87;
then
A26: [o.(y`1,z`1),z`2] in [:o.:[:X,Y:],Z:] by A25,ZFMISC_1:87;
x = o.(y`1,y`2) by A17,MCART_1:21;
then x = o.(o.(y`1,z`1),z`2) by A2,A23;
hence thesis by A1,A26,FUNCT_1:def 6;
end;
theorem Th49:
o is commutative implies o.:^2 is commutative
proof
assume
A1: o is commutative;
let x,y be Subset of D;
thus (o.:^2).(x,y) = o.:[:x,y:] by Th44
.= o.:[:y,x:] by A1,Th47
.= (o.:^2).(y,x) by Th44;
end;
theorem Th50:
o is associative implies o.:^2 is associative
proof
assume
A1: o is associative;
let x,y,z be Subset of D;
thus (o.:^2).((o.:^2).(x,y),z) = (o.:^2).(o.:[:x,y:],z) by Th44
.= o.:[:o.:[:x,y:],z:] by Th44
.= o.:[:x,o.:[:y,z:]:] by A1,Th48
.= (o.:^2).(x,o.:[:y,z:]) by Th44
.= (o.:^2).(x,(o.:^2).(y,z)) by Th44;
end;
theorem Th51:
a is_a_unity_wrt o implies o.:[:{a},X:] = D /\ X & o.:[:X,{a}:] = D /\ X
proof
assume
A1: a is_a_unity_wrt o;
thus o.:[:{a},X:] c= D /\ X
proof
let x be object;
assume x in o.:[:{a},X:];
then consider y being object such that
A2: y in dom o and
A3: y in [:{a},X:] and
A4: x = o.y by FUNCT_1:def 6;
reconsider y as Element of [:D,D:] by A2;
A5: x = o.(y`1,y`2) by A4,MCART_1:21;
A6: y = [y`1,y`2] by MCART_1:21;
then y`1 in {a} by A3,ZFMISC_1:87;
then
A7: y`1 = a by TARSKI:def 1;
A8: o.(a,y`2) = y`2 by A1,BINOP_1:3;
y`2 in X by A3,A6,ZFMISC_1:87;
hence thesis by A5,A8,A7,XBOOLE_0:def 4;
end;
A9: dom o = [:D,D:] by FUNCT_2:def 1;
thus D /\ X c= o.:[:{a},X:]
proof
let x be object;
A10: a in {a} by TARSKI:def 1;
assume
A11: x in D /\ X;
then reconsider d = x as Element of D by XBOOLE_0:def 4;
A12: x = o.(a,d) by A1,BINOP_1:3
.= o.[a,x];
x in X by A11,XBOOLE_0:def 4;
then [a,d] in [:{a},X:] by A10,ZFMISC_1:87;
hence thesis by A9,A12,FUNCT_1:def 6;
end;
thus o.:[:X,{a}:] c= D /\ X
proof
let x be object;
assume x in o.:[:X,{a}:];
then consider y being object such that
A13: y in dom o and
A14: y in [:X,{a}:] and
A15: x = o.y by FUNCT_1:def 6;
reconsider y as Element of [:D,D:] by A13;
A16: x = o.(y`1,y`2) by A15,MCART_1:21;
A17: y = [y`1,y`2] by MCART_1:21;
then y`2 in {a} by A14,ZFMISC_1:87;
then
A18: y`2 = a by TARSKI:def 1;
A19: o.(y`1,a) = y`1 by A1,BINOP_1:3;
y`1 in X by A14,A17,ZFMISC_1:87;
hence thesis by A16,A19,A18,XBOOLE_0:def 4;
end;
thus D /\ X c= o.:[:X,{a}:]
proof
let x be object;
A20: a in {a} by TARSKI:def 1;
assume
A21: x in D /\ X;
then reconsider d = x as Element of D by XBOOLE_0:def 4;
A22: x = o.(d,a) by A1,BINOP_1:3
.= o.[x,a];
x in X by A21,XBOOLE_0:def 4;
then [d,a] in [:X,{a}:] by A20,ZFMISC_1:87;
hence thesis by A9,A22,FUNCT_1:def 6;
end;
end;
theorem Th52:
a is_a_unity_wrt o implies {a} is_a_unity_wrt o.:^2 & o.:^2 is
having_a_unity & the_unity_wrt o.:^2 = {a}
proof
assume
A1: a is_a_unity_wrt o;
now
let x be Subset of D;
thus (o.:^2).({a},x) = o.:[:{a},x:] by Th44
.= D /\ x by A1,Th51
.= x by XBOOLE_1:28;
thus (o.:^2).(x,{a}) = o.:[:x,{a}:] by Th44
.= D /\ x by A1,Th51
.= x by XBOOLE_1:28;
end;
hence
A2: {a} is_a_unity_wrt o.:^2 by BINOP_1:3;
hence ex A being Subset of D st A is_a_unity_wrt o.:^2;
thus thesis by A2,BINOP_1:def 8;
end;
theorem Th53:
o is having_a_unity implies o.:^2 is having_a_unity & {
the_unity_wrt o} is_a_unity_wrt o.:^2 & the_unity_wrt o.:^2 = {the_unity_wrt o}
proof
given a such that
A1: a is_a_unity_wrt o;
a = the_unity_wrt o by A1,BINOP_1:def 8;
hence thesis by A1,Th52;
end;
theorem Th54:
o is uniquely-decomposable implies o.:^2 is uniquely-decomposable
proof
assume that
A1: o is having_a_unity and
A2: o.(a,b) = the_unity_wrt o implies a = b & b = the_unity_wrt o;
thus o.:^2 is having_a_unity by A1,Th53;
let A,B be Subset of D such that
A3: (o.:^2).(A,B) = the_unity_wrt o.:^2;
set a = the_unity_wrt o;
A4: the_unity_wrt o.:^2 = {a} by A1,Th53;
set a1 = the Element of A,a2 = the Element of B;
o.:[:A,B:] = (o.:^2).(A,B) by Th44;
then dom o meets [:A,B:] by A3,A4,RELAT_1:118;
then dom o /\ [:A,B:] <> {};
then
A5: [:A,B:] <> {};
then
A6: A <> {} by ZFMISC_1:90;
A7: B <> {} by A5,ZFMISC_1:90;
then reconsider a1,a2 as Element of D by A6,TARSKI:def 3;
A8: {a1} c= A by A6,ZFMISC_1:31;
o.(a1,a2) in {a} by A3,A4,A6,A7,Th45;
then
A9: o.(a1,a2) = a by TARSKI:def 1;
then
A10: a2 = a by A2;
A11: A c= {a}
proof
let x be object;
assume
A12: x in A;
then reconsider c = x as Element of D;
o.(c,a2) in {a} by A3,A4,A7,A12,Th45;
then o.(c,a2) = a by TARSKI:def 1;
then c = a2 by A2;
hence thesis by A10,TARSKI:def 1;
end;
A13: B c= {a}
proof
let x be object;
assume
A14: x in B;
then reconsider c = x as Element of D;
o.(a1,c) in {a} by A3,A4,A6,A14,Th45;
then o.(a1,c) = a by TARSKI:def 1;
then c = a by A2;
hence thesis by TARSKI:def 1;
end;
A15: a1 = a2 by A2,A9;
{a2} c= B by A7,ZFMISC_1:31;
then B = {a} by A10,A13;
hence thesis by A1,A15,A10,A8,A11,Th53;
end;
definition
let G be non empty multMagma;
func bool G -> multMagma equals
: Def9:
multLoopStr(#bool the carrier of G,
(the multF of G).:^2, {the_unity_wrt the multF of G}#) if G is unital otherwise
multMagma(#bool the carrier of G, (the multF of G).:^2#);
correctness;
end;
registration
let G be non empty multMagma;
cluster bool G -> non empty;
coherence
proof
per cases;
suppose
G is unital;
then
bool G = multLoopStr(#bool the carrier of G, (the multF of G).:^2, {
the_unity_wrt the multF of G}#) by Def9;
hence the carrier of bool G is non empty;
end;
suppose
G is not unital;
then
bool G = multMagma(#bool the carrier of G, (the multF of G).:^2#) by Def9
;
hence the carrier of bool G is non empty;
end;
end;
end;
definition
let G be unital non empty multMagma;
redefine func bool G -> well-unital strict non empty multLoopStr; :: redefines bool (MONOID_1, definition)
coherence
proof
set M = multLoopStr(#bool carr(G), op(G).:^2,{the_unity_wrt op(G)}#);
op(G) is having_a_unity by MONOID_0:def 10;
then
A1: {the_unity_wrt op(G)} is_a_unity_wrt op(G).:^2 by Th53;
1.M = {the_unity_wrt op(G)} & bool G = M by Def9;
hence thesis by A1,MONOID_0:def 21;
end;
end;
theorem Th55:
the carrier of bool G = bool the carrier of G & the multF of
bool G = (the multF of G).:^2
proof
bool G = multLoopStr(#bool carr(G), op(G).:^2,{the_unity_wrt op(G)}#) or
bool G = multMagma(#bool the carrier of G, op(G).:^2#) by Def9;
hence thesis;
end;
theorem
for G being unital non empty multMagma holds 1.bool G = {
the_unity_wrt the multF of G}
proof
let G be unital non empty multMagma;
bool G = multLoopStr(#bool carr(G), op(G).:^2,{the_unity_wrt op(G)}#) by Def9
;
hence thesis;
end;
theorem
for G being non empty multMagma holds (G is commutative implies bool G
is commutative) & (G is associative implies bool G is associative) & (G is
uniquely-decomposable implies bool G is uniquely-decomposable)
proof
let G be non empty multMagma;
A1: op(bool G) = op(G).:^2 & carr(bool G) = bool carr(G) by Th55;
thus G is commutative implies bool G is commutative
by A1,Th49;
thus G is associative implies bool G is associative
by A1,Th50;
assume op(G) is uniquely-decomposable;
hence op(bool G) is uniquely-decomposable by A1,Th54;
end;