:: Monoids
:: 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 STRUCT_0, ALGSTR_0, BINOP_1, SUBSET_1, FUNCT_1, FINSEQ_1,
RELAT_1, ORDINAL4, XBOOLE_0, ALGSTR_1, SETWISEO, FUNCOP_1, ZFMISC_1,
GROUP_1, FINSEQOP, MESFUNC1, VECTSP_1, TARSKI, REALSET1, MCART_1,
NUMBERS, BINOP_2, REAL_1, ARYTM_3, CARD_1, GR_CY_1, INT_1, PARTFUN1,
FUNCT_2, MONOID_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, XTUPLE_0, MCART_1, DOMAIN_1, BINOP_2, REALSET1, STRUCT_0,
RELAT_1, FINSEQOP, FUNCT_1, FINSEQ_1, PARTFUN1, FUNCT_2, BINOP_1,
FINSEQ_2, INT_1, GROUP_1, VECTSP_1, SETWISEO, FUNCOP_1, GR_CY_1,
ALGSTR_0;
constructors RELAT_2, PARTFUN1, BINOP_1, SETWISEO, BINOP_2, FINSEQOP,
REALSET1, VECTSP_2, GR_CY_1, RELSET_1, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1,
FUNCT_2, NUMBERS, BINOP_2, MEMBERED, FINSEQ_1, REALSET1, STRUCT_0,
GROUP_1, ALGSTR_0, GR_CY_1, XREAL_0, NAT_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, BINOP_1, SETWISEO, FINSEQOP, GROUP_1, STRUCT_0, XBOOLE_0,
VECTSP_1;
equalities BINOP_1, STRUCT_0, REALSET1, ALGSTR_0, FUNCOP_1;
expansions TARSKI, BINOP_1, FINSEQOP, GROUP_1, VECTSP_1;
theorems TARSKI, NAT_1, INT_1, FINSEQ_1, BINOP_1, GROUP_1, SETWISEO, MCART_1,
ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_4, FUNCOP_1, PARTFUN1, GR_CY_1,
GRFUNC_1, RELAT_1, RELSET_1, XCMPLX_1, NUMBERS, BINOP_2, ORDINAL1;
schemes FUNCT_2, BINOP_1, XBOOLE_0;
begin :: Updating
reserve x,y,X,Y for set;
deffunc carr(1-sorted) = the carrier of $1;
deffunc op(multMagma) = the multF of $1;
definition
let G be 1-sorted;
mode BinOp of G is BinOp of the carrier of G;
end;
definition
let IT be 1-sorted;
attr IT is constituted-Functions means
:Def1:
for a being Element of IT holds a is Function;
attr IT is constituted-FinSeqs means
:Def2:
for a being Element of IT holds a is FinSequence;
end;
registration
cluster constituted-Functions for 1-sorted;
existence
proof
set f = the Function;
take X = 1-sorted(#{f}#);
let a be Element of X;
thus thesis;
end;
cluster constituted-FinSeqs for 1-sorted;
existence
proof
set f = the FinSequence;
take X = 1-sorted(#{f}#);
let a be Element of X;
thus thesis by TARSKI:def 1;
end;
end;
registration
let X be constituted-Functions 1-sorted;
cluster -> Function-like Relation-like for Element of X;
coherence by Def1;
end;
registration
cluster constituted-FinSeqs -> constituted-Functions for 1-sorted;
coherence;
end;
registration
let X be constituted-FinSeqs 1-sorted;
cluster -> FinSequence-like for Element of X;
coherence by Def2;
end;
definition
let D be set, p,q be FinSequence of D;
redefine func p^q -> Element of D*; :: redefines ^ (FINSEQ_1, definition)
coherence
proof
thus p^q is Element of D* by FINSEQ_1:def 11;
end;
end;
notation
let g,f be Function;
synonym f(*)↑g for f*g;
end;
definition
let D be non empty set;
let IT be BinOp of D;
attr IT is left-invertible means
for a,b being Element of D ex l being Element of D st IT.(l,a) = b;
attr IT is right-invertible means
for a,b being Element of D ex r being Element of D st IT.(a,r) = b;
attr IT is invertible means
for a,b being Element of D ex r,l being
Element of D st IT.(a,r) = b & IT.(l,a) = b;
attr IT is left-cancelable means
for a,b,c being Element of D st IT.(a,b) = IT.(a,c) holds b = c;
attr IT is right-cancelable means
for a,b,c being Element of D st IT.(b,a) = IT.(c,a) holds b = c;
attr IT is cancelable means
for a,b,c being Element of D st IT.(a,b) = IT.(a
,c) or IT.(b,a) = IT.(c,a) holds b = c;
attr IT is uniquely-decomposable means
IT is having_a_unity & for a,b being
Element of D st IT.(a,b) = the_unity_wrt IT holds a = b & b = the_unity_wrt IT;
end;
theorem Th1:
for D be non empty set, f being BinOp of D holds f is invertible
iff f is left-invertible right-invertible
proof
let D be non empty set, f be BinOp of D;
thus f is invertible implies f is left-invertible right-invertible
proof
assume
A1: for a,b being Element of D ex r,l being Element of D st f.(a,r) =
b & f.(l,a) = b;
now
let a,b be Element of D;
consider r,l being Element of D such that
f.(a,r) = b and
A2: f.(l,a) = b by A1;
take l;
thus f.(l,a) = b by A2;
end;
hence for a,b being Element of D ex l being Element of D st f.(l,a) = b;
let a,b be Element of D;
consider r,l being Element of D such that
A3: f.(a,r) = b and
f.(l,a) = b by A1;
take r;
thus thesis by A3;
end;
assume that
A4: for a,b being Element of D ex l being Element of D st f.(l,a) = b and
A5: for a,b being Element of D ex r being Element of D st f.(a,r) = b;
let a,b be Element of D;
consider l being Element of D such that
A6: f.(l,a) = b by A4;
consider r being Element of D such that
A7: f.(a,r) = b by A5;
take r, l;
thus thesis by A6,A7;
end;
theorem
for D be non empty set, f being BinOp of D holds f is cancelable
iff f is left-cancelable right-cancelable;
theorem Th3:
for f being BinOp of {x} holds f = (x,x) .--> x & f is
having_a_unity & f is commutative & f is associative & f is idempotent & f is
invertible cancelable uniquely-decomposable
proof
let f be BinOp of {x};
reconsider a = x as Element of {x} by TARSKI:def 1;
A1: [:{x},{x}:] = {[x,x]} by ZFMISC_1:29;
A2: now
let y be object;
assume
A3: y in {[x,x]};
then reconsider b = y as Element of [:{x},{x}:] by ZFMISC_1:29;
thus f.y = f.b .= x by TARSKI:def 1
.= ((x,x) .--> x).y by A3,FUNCOP_1:7;
end;
dom f = [:{x},{x}:] & dom ((x,x) .--> x) = {[x,x]} by FUNCT_2:def 1;
hence f = (x,x) .--> x by A1,A2,FUNCT_1:2;
A4: now
let a,b be Element of {x};
a = x by TARSKI:def 1;
hence a = b by TARSKI:def 1;
end;
then for b being Element of {x} holds f.(a,b) = b & f.(b,a) = b;
then
A5: a is_a_unity_wrt f by BINOP_1:3;
hence ex a being Element of {x} st a is_a_unity_wrt f;
thus for a,b being Element of {x} holds f.(a,b) = f.(b,a) by A4;
thus for a,b,c being Element of {x} holds f.(a,f.(b,c)) = f.(f.(a,b),c) by A4
;
thus for a being Element of {x} holds f.(a,a) = a by A4;
thus for a,b being Element of {x} ex r,l being Element of {x} st f.(a,r) = b
& f.(l,a) = b
proof
let a,b be Element of {x};
take a,a;
thus thesis by A4;
end;
thus for a,b,c being Element of {x} st f.(a,b) = f.(a,c) or f.(b,a) = f.(c,a
) holds b = c by A4;
thus ex a being Element of {x} st a is_a_unity_wrt f by A5;
let a,b be Element of {x};
thus thesis by A4;
end;
begin :: Semigroups
reserve G for non empty multMagma,
D for set,
a,b,c,r,l for Element of G;
definition
let IT be non empty multMagma;
redefine attr IT is unital means :Def10: :: redefines unital (GROUP_1, definition)
the multF of IT is having_a_unity;
compatibility
proof
thus IT is unital implies the multF of IT is having_a_unity;
given x being Element of IT such that
A1: x is_a_unity_wrt the multF of IT;
take x;
let h be Element of IT;
thus thesis by A1,BINOP_1:3;
end;
end;
definition
let G;
redefine attr G is commutative means :Def11: :: redefines commutative (GROUP_1, definition)
the multF of G is commutative;
compatibility
proof
thus G is commutative implies the multF of G is commutative
proof
assume
A1: a*b = b*a;
let a,b;
op(G).(a,b) = a*b & op(G).(b,a) = b*a;
hence thesis by A1;
end;
assume
A2: for a,b holds op(G).(a,b) = op(G).(b,a);
let a,b;
thus thesis by A2;
end;
redefine attr G is associative means :Def12: :: redefines associative (GROUP_1, definition)
the multF of G is associative;
compatibility;
end;
definition
let IT be non empty multMagma;
attr IT is idempotent means
the multF of IT is idempotent;
attr IT is left-invertible means
the multF of IT is left-invertible;
attr IT is right-invertible means
the multF of IT is right-invertible;
attr IT is invertible means
the multF of IT is invertible;
attr IT is left-cancelable means
the multF of IT is left-cancelable;
attr IT is right-cancelable means
the multF of IT is right-cancelable;
attr IT is cancelable means
the multF of IT is cancelable;
attr IT is uniquely-decomposable means :Def20:
the multF of IT is uniquely-decomposable;
end;
registration
cluster unital commutative associative cancelable idempotent invertible
uniquely-decomposable constituted-Functions constituted-FinSeqs strict
for non empty multMagma;
existence
proof
set p = the FinSequence,o = the BinOp of {p};
take G = multMagma(#{p},o#);
thus op(G) is having_a_unity & op(G) is commutative & op(G) is associative
& op(G) is cancelable & op(G) is idempotent & op(G) is invertible
uniquely-decomposable by Th3;
thus (for x being Element of G holds x is Function) & for x being Element
of G holds x is FinSequence by TARSKI:def 1;
thus thesis;
end;
end;
theorem Th4:
G is unital implies
the_unity_wrt the multF of G is_a_unity_wrt the multF of G
proof
given a such that
A1: a is_a_unity_wrt op(G);
thus thesis by A1,BINOP_1:def 8;
end;
theorem
G is unital iff for a holds
(the_unity_wrt the multF of G)*a = a &
a*(the_unity_wrt the multF of G) = a
proof
set u = the_unity_wrt the multF of G;
thus G is unital implies for b holds u*b = b & b*u = b
proof
given a such that
A1: a is_a_unity_wrt op(G);
let b;
u = a by A1,BINOP_1:def 8;
hence thesis by A1,BINOP_1:3;
end;
assume
A2: u*b = b & b*u = b;
take a = u;
thus a is_a_left_unity_wrt the multF of G
proof
let b;
a*b = b by A2;
hence thesis;
end;
let b;
b*a = b by A2;
hence thesis;
end;
theorem Th6:
G is unital iff ex a st for b holds a*b = b & b*a = b;
Lm1: G is associative iff for a,b,c holds a*b*c = a*(b*c);
theorem Th7:
G is idempotent iff for a holds a*a = a
proof
thus G is idempotent implies for a holds a*a = a
proof
assume
A1: op(G).(a,a) = a;
let a;
thus thesis by A1;
end;
assume
A2: a*a = a;
let a;
thus op(G).(a,a) = a*a .= a by A2;
end;
theorem
G is left-invertible iff for a,b ex l st l*a = b
proof
thus G is left-invertible implies for a,b ex l st l*a = b
proof
assume
A1: for a,b ex l st op(G).(l,a) = b;
let a,b;
consider l such that
A2: op(G).(l,a) = b by A1;
take l;
thus thesis by A2;
end;
assume
A3: for a,b ex l st l*a = b;
let a,b;
consider l such that
A4: l*a = b by A3;
take l;
thus thesis by A4;
end;
theorem
G is right-invertible iff for a,b ex r st a*r = b
proof
thus G is right-invertible implies for a,b ex r st a*r = b
proof
assume
A1: for a,b ex r st op(G).(a,r) = b;
let a,b;
consider r such that
A2: op(G).(a,r) = b by A1;
take r;
thus thesis by A2;
end;
assume
A3: for a,b ex r st a*r = b;
let a,b;
consider r such that
A4: a*r = b by A3;
take r;
thus thesis by A4;
end;
theorem Th10:
G is invertible iff for a,b ex r,l st a*r = b & l*a = b
proof
thus G is invertible implies for a,b ex r,l st a*r = b & l*a = b
proof
assume
A1: for a,b ex r,l st op(G).(a,r) = b & op(G).(l,a) = b;
let a,b;
consider r, l such that
A2: op(G).(a,r) = b & op(G).(l,a) = b by A1;
take r, l;
thus thesis by A2;
end;
assume
A3: for a,b ex r,l st a*r = b & l*a = b;
let a,b;
consider r, l such that
A4: a*r = b & l*a = b by A3;
take r, l;
thus thesis by A4;
end;
theorem
G is left-cancelable iff for a,b,c st a*b = a*c holds b = c
proof
thus G is left-cancelable implies for a,b,c st a*b = a*c holds b = c
proof
assume
A1: op(G).(a,b) = op(G).(a,c) implies b = c;
let a,b,c;
thus thesis by A1;
end;
assume
A2: for a,b,c st a*b = a*c holds b = c;
let a,b,c;
a*b = op(G).(a,b) & a*c = op(G).(a,c);
hence thesis by A2;
end;
theorem
G is right-cancelable iff for a,b,c st b*a = c*a holds b = c
proof
thus G is right-cancelable implies for a,b,c st b*a = c*a holds b = c
proof
assume
A1: for a,b,c st op(G).(b,a) = op(G).(c,a) holds b = c;
let a,b,c;
thus thesis by A1;
end;
assume
A2: for a,b,c st b*a = c*a holds b = c;
let a,b,c;
b*a = op(G).(b,a) & c*a = op(G).(c,a);
hence thesis by A2;
end;
theorem Th13:
G is cancelable iff for a,b,c st a*b = a*c or b*a = c*a holds b = c
proof
thus G is cancelable implies for a,b,c st a*b = a*c or b*a = c*a holds b=c
proof
assume
A1: op(G).(a,b) = op(G).(a,c) or op(G).(b,a) = op(G).(c,a) implies b = c;
let a,b,c;
thus thesis by A1;
end;
assume
A2: for a,b,c st a*b = a*c or b*a = c*a holds b = c;
let a,b,c;
A3: b*a = op(G).(b,a) & c*a = op(G).(c,a);
a*b = op(G).(a,b) & a*c = op(G).(a,c);
hence thesis by A2,A3;
end;
theorem Th14:
G is uniquely-decomposable iff the multF of G is having_a_unity &
for a,b being Element of G st a*b = the_unity_wrt the multF of G holds a = b
& b = the_unity_wrt the multF of G
proof
thus G is uniquely-decomposable implies op(G) is having_a_unity & for a,b
being Element of G st a*b = the_unity_wrt op(G) holds a = b & b = the_unity_wrt
the multF of G
proof
assume that
A1: op(G) is having_a_unity and
A2: for a,b being Element of G st op(G).(a,b) = the_unity_wrt op(G)
holds a = b & b = the_unity_wrt op(G);
thus op(G) is having_a_unity by A1;
let a,b be Element of G;
thus thesis by A2;
end;
assume that
A3: op(G) is having_a_unity and
A4: for a,b being Element of G st a*b = the_unity_wrt op(G) holds a = b
& b = the_unity_wrt op(G);
thus op(G) is having_a_unity by A3;
let a,b be Element of G;
a*b = op(G).(a,b);
hence thesis by A4;
end;
theorem Th15:
G is associative implies
(G is invertible iff
G is unital & the multF of G is having_an_inverseOp)
proof
assume
A1: G is associative;
thus G is invertible implies G is unital & op(G) is having_an_inverseOp
proof
set e = the Element of G;
assume
A2: G is invertible;
then consider x,y being Element of G such that
A3: e*x = e and
A4: y*e = e by Th10;
A5: now
let a;
A6: ex b,c st e*b = a & c*e = a by A2,Th10;
hence y*a = a by A1,A4;
thus a*x = a by A1,A3,A6;
end;
then
A7: y*x = x & y*x = y;
hence G is unital by A5;
defpred P[Element of G,Element of G] means $1*$2 = x & $2*$1 = x;
A8: for a ex b st P[a,b]
proof
let a;
consider b,c such that
A9: a*b = x & c*a = x by A2,Th10;
take b;
c*(a*b) = c*a*b & x*b = b by A1,A5,A7;
hence thesis by A5,A9;
end;
ex f being Function of the carrier of G,the carrier of G st for x
being Element of G holds P[x,f.x] from FUNCT_2:sch 3(A8);
then consider u being UnOp of carr(G) such that
A10: for a being Element of G holds P[a,(u.a)];
now
let b;
x*b = op(G).(x,b) & b*x = op(G).(b,x);
hence op(G).(x,b) = b & op(G).(b,x) = b by A5,A7;
end;
then x is_a_unity_wrt op(G) by BINOP_1:3;
then
A11: x = the_unity_wrt op(G) by BINOP_1:def 8;
take u;
let a;
op(G).(a,u.a) = a*(u.a) & op(G).(u.a,a) = (u.a)*a;
hence thesis by A10,A11;
end;
assume
A12: op(G) is having_a_unity;
given u being UnOp of carr(G) such that
A13: u is_an_inverseOp_wrt op(G);
let a,c;
take l = (u.a)*c, r = c*(u.a);
thus op(G).(a,l) = a*l .= a*(u.a)*c by A1
.= op(G).(the_unity_wrt op(G),c) by A13
.= c by A12,SETWISEO:15;
thus op(G).(r,a) = r*a .= c*((u.a)*a) by A1
.= op(G).(c,the_unity_wrt op(G)) by A13
.= c by A12,SETWISEO:15;
end;
Lm2: G is invertible iff G is left-invertible right-invertible
by Th1;
Lm3: G is cancelable iff G is left-cancelable right-cancelable
proof
thus G is cancelable implies G is left-cancelable right-cancelable
proof
assume op(G) is cancelable;
hence op(G) is left-cancelable right-cancelable;
end;
assume op(G) is left-cancelable right-cancelable;
hence op(G) is cancelable;
end;
Lm4: G is associative invertible implies G is Group-like
proof
assume
A1: G is associative invertible;
then G is unital by Th15;
then consider a such that
A2: for b holds a*b = b & b*a = b;
take a;
let b;
thus b*a = b & a*b = b by A2;
op(G) is invertible by A1;
then consider l,r being Element of G such that
A3: op(G).(b,l) = a & op(G).(r,b) = a;
take l;
A4: b*l = a & r*b = a by A3;
r = r*a by A2
.= a*l by A1,A4
.= l by A2;
hence thesis by A3;
end;
registration
cluster associative Group-like -> invertible for non empty multMagma;
coherence by Th15;
cluster associative invertible -> Group-like for non empty multMagma;
coherence by Lm4;
end;
registration
cluster invertible -> left-invertible right-invertible for
non empty multMagma;
coherence by Lm2;
cluster left-invertible right-invertible -> invertible for
non empty multMagma;
coherence by Lm2;
cluster cancelable -> left-cancelable right-cancelable for
non empty multMagma;
coherence by Lm3;
cluster left-cancelable right-cancelable -> cancelable for
non empty multMagma;
coherence by Lm3;
cluster associative invertible -> unital cancelable for
non empty multMagma;
coherence
proof
let G be non empty multMagma;
assume G is associative invertible;
then reconsider G as associative invertible non empty multMagma;
for a,b,c being Element of G st a*b = a*c or b*a = c*a holds b = c
by GROUP_1:6;
hence thesis by Th13;
end;
end;
begin :: Monoids
deffunc un(multLoopStr) = 1.$1;
reserve M for non empty multLoopStr;
definition
let IT be non empty multLoopStr;
redefine attr IT is well-unital means :: redefines well-unital (VECTSP_1, definition)
:Def21:
1.IT is_a_unity_wrt the multF of IT;
compatibility
proof
thus IT is well-unital implies 1.IT is_a_unity_wrt the multF of IT
proof
assume
A1: IT is well-unital;
thus 1.IT is_a_left_unity_wrt the multF of IT
proof
let a be Element of IT;
thus (the multF of IT).(1.IT,a) = (1.IT)*a .= a by A1;
end;
let a be Element of IT;
thus (the multF of IT).(a,1.IT) = a*(1.IT) .= a by A1;
end;
assume
A2: 1.IT is_a_unity_wrt the multF of IT;
let x be Element of IT;
1.IT is_a_right_unity_wrt the multF of IT by A2;
hence x*(1.IT) = x;
1.IT is_a_left_unity_wrt the multF of IT by A2;
hence thesis;
end;
end;
theorem Th16:
M is well-unital iff
for a being Element of M holds (1.M)*a = a & a*(1.M) = a;
theorem Th17:
for M being non empty multLoopStr st M is well-unital holds
1.M = the_unity_wrt the multF of M by BINOP_1:def 8;
registration
cluster well-unital commutative associative cancelable idempotent invertible
uniquely-decomposable unital constituted-Functions constituted-FinSeqs
strict for non empty multLoopStr;
existence
proof
set p = the FinSequence,o = the BinOp of {p},e = the Element of {p};
take G = multLoopStr(#{p},o,e#);
reconsider e as Element of G;
reconsider o as BinOp of G;
now
let b be Element of G;
o.(e,b) = p & o.(b,e) = p by TARSKI:def 1;
hence o.(e,b) = b & o.(b,e) = b by TARSKI:def 1;
end;
hence un(G) is_a_unity_wrt op(G) by BINOP_1:3;
hence op(G) is commutative & op(G) is associative & op(G) is cancelable &
op(G) is idempotent & op(G) is invertible uniquely-decomposable & ex e being
Element of G st e is_a_unity_wrt op(G) by Th3;
thus (for x being Element of G holds x is Function) & for x being Element
of G holds x is FinSequence by TARSKI:def 1;
thus thesis;
end;
end;
definition
mode Monoid is well-unital associative non empty multLoopStr;
end;
definition
let G be multMagma;
mode MonoidalExtension of G -> multLoopStr means
:Def22:
the multMagma of it = the multMagma of G;
existence
proof
set g = the Element of G;
take multLoopStr(#carr(G), op(G), g#);
thus thesis;
end;
end;
registration
let G be non empty multMagma;
cluster -> non empty for MonoidalExtension of G;
coherence
proof
let M be MonoidalExtension of G;
the multMagma of M = the multMagma of G by Def22;
hence the carrier of M is non empty;
end;
end;
theorem Th18:
for M being MonoidalExtension of G holds
the carrier of M = the carrier of G &
the multF of M = the multF of G &
for a,b being Element of M,
a9,b9 being Element of G st a = a9 & b = b9 holds
a*b = a9*b9
proof
let M be MonoidalExtension of G;
A1: the multMagma of M = the multMagma of G by Def22;
hence carr(M) = carr(G) & op(M) = op(G);
let a,b be Element of M, a9,b9 be Element of G;
thus thesis by A1;
end;
registration
let G be multMagma;
cluster strict for MonoidalExtension of G;
existence
proof
set g = the Element of G;
set M = multLoopStr(#carr(G), op(G), g#);
the multMagma of M = the multMagma of G;
then M is MonoidalExtension of G by Def22;
hence thesis;
end;
end;
theorem Th19:
for G being non empty multMagma, M being MonoidalExtension of G holds
(G is unital implies M is unital) &
(G is commutative implies M is commutative) &
(G is associative implies M is associative) &
(G is invertible implies M is invertible) &
(G is uniquely-decomposable implies M is uniquely-decomposable) &
(G is cancelable implies M is cancelable)
proof
let G be non empty multMagma, M be MonoidalExtension of G;
A1: the multMagma of M = the multMagma of G by Def22;
thus G is unital implies M is unital by A1;
thus G is commutative implies M is commutative by A1;
thus G is associative implies M is associative by A1;
thus G is invertible implies M is invertible by A1;
thus G is uniquely-decomposable implies M is uniquely-decomposable
by A1;
assume op(G) is cancelable;
hence op(M) is cancelable by A1;
end;
registration
let G be constituted-Functions multMagma;
cluster -> constituted-Functions for MonoidalExtension of G;
coherence
proof
let M be MonoidalExtension of G;
let a be Element of M;
the multMagma of M = the multMagma of G by Def22;
hence thesis;
end;
end;
registration
let G be constituted-FinSeqs multMagma;
cluster -> constituted-FinSeqs for MonoidalExtension of G;
coherence
proof
let M be MonoidalExtension of G;
let a be Element of M;
the multMagma of M = the multMagma of G by Def22;
hence thesis;
end;
end;
registration
let G be unital non empty multMagma;
cluster -> unital for MonoidalExtension of G;
coherence by Th19;
end;
registration
let G be associative non empty multMagma;
cluster -> associative for MonoidalExtension of G;
coherence by Th19;
end;
registration
let G be commutative non empty multMagma;
cluster -> commutative for MonoidalExtension of G;
coherence by Th19;
end;
registration
let G be invertible non empty multMagma;
cluster -> invertible for MonoidalExtension of G;
coherence by Th19;
end;
registration
let G be cancelable non empty multMagma;
cluster -> cancelable for MonoidalExtension of G;
coherence by Th19;
end;
registration
let G be uniquely-decomposable non empty multMagma;
cluster -> uniquely-decomposable for MonoidalExtension of G;
coherence by Th19;
end;
registration
let G be unital non empty multMagma;
cluster well-unital strict for MonoidalExtension of G;
existence
proof
set M = multLoopStr(#carr(G), op(G), the_unity_wrt op(G)#);
the multMagma of M = the multMagma of G;
then reconsider M as MonoidalExtension of G by Def22;
take M;
thus un(M) is_a_unity_wrt op(M) by Th4;
thus thesis;
end;
end;
theorem Th20:
for G being unital non empty multMagma
for M1,M2 being well-unital strict MonoidalExtension of G
holds M1 = M2
proof
let G be unital non empty multMagma;
let M1,M2 be well-unital strict MonoidalExtension of G;
A1: un(M1) = the_unity_wrt op(M1) & un(M2) = the_unity_wrt op(M2) by Th17;
the multMagma of M1 = the multMagma of G & the multMagma of M2 = the
multMagma of G by Def22;
hence thesis by A1;
end;
begin :: Subsystems
definition
let G be multMagma;
mode SubStr of G -> multMagma means
:Def23:
the multF of it c= the multF of G;
existence;
end;
registration
let G be multMagma;
cluster strict for SubStr of G;
existence
proof
the multMagma of G is SubStr of G by Def23;
hence thesis;
end;
end;
registration
let G be non empty multMagma;
cluster strict non empty for SubStr of G;
existence
proof
the multMagma of G is SubStr of G by Def23;
hence thesis;
end;
end;
registration
let G be unital non empty multMagma;
cluster unital associative commutative cancelable idempotent invertible
uniquely-decomposable strict for non empty SubStr of G;
existence
proof
consider a being Element of G such that
A1: for b being Element of G holds a*b = b & b*a = b by Th6;
A2: a = a*a by A1;
set f = the BinOp of {a};
set H = multMagma(#{a},f#);
A3: dom op(G) = [:carr(G),carr(G):] by FUNCT_2:def 1;
f = (a,a) .--> a by Th3
.= [a,a] .--> a;
then op(H) c= op(G) by A2,A3,FUNCT_4:7;
then reconsider H as non empty SubStr of G by Def23;
take H;
thus op(H) is having_a_unity & op(H) is associative & op(H) is commutative
& op(H) is cancelable & op(H) is idempotent & op(H) is invertible
uniquely-decomposable by Th3;
thus thesis;
end;
end;
definition
let G be multMagma;
mode MonoidalSubStr of G -> multLoopStr means
:Def24:
the multF of it c= the multF of G &
for M being multLoopStr st G = M holds 1.it = 1.M;
existence
proof
set M = the MonoidalExtension of G;
A1: now
given M being multLoopStr such that
A2: G = M;
take M;
thus op(M) c= op(G) by A2;
thus for N being multLoopStr st G = N holds un(M) = un(N) by A2;
end;
A3: (ex M being multLoopStr st G = M) or for N being multLoopStr st G = N
holds un(M) = un(N);
the multMagma of M = the multMagma of G by Def22;
hence thesis by A1,A3;
end;
end;
registration
let G be multMagma;
cluster strict for MonoidalSubStr of G;
existence
proof
set N = the MonoidalSubStr of G;
un(the multLoopStr of N) = un(N);
then
A1: for M being multLoopStr st G = M holds un(the multLoopStr of N) = un(M
) by Def24;
op(the multLoopStr of N) c= op(G) by Def24;
then the multLoopStr of N is MonoidalSubStr of G by A1,Def24;
hence thesis;
end;
end;
registration
let G be non empty multMagma;
cluster strict non empty for MonoidalSubStr of G;
existence
proof
per cases;
suppose
G is multLoopStr;
then reconsider L = G as multLoopStr;
for N being multLoopStr st G = N holds 1.the multLoopStr of L = 1.N;
then reconsider M = the multLoopStr of L as MonoidalSubStr of G by Def24;
take M;
thus M is strict;
thus the carrier of M is non empty;
end;
suppose
A1: G is not multLoopStr;
set M = the strict MonoidalExtension of G;
A2: for N being multLoopStr st G = N holds 1.M = 1.N by A1;
the multMagma of M = the multMagma of G by Def22;
then reconsider M as MonoidalSubStr of G by A2,Def24;
take M;
thus thesis;
end;
end;
end;
definition
let M be multLoopStr;
redefine mode MonoidalSubStr of M means :: redefines MonoidalSubStr (MONOID_0, definition)
:Def25:
the multF of it c= the multF of M & 1.it = 1.M;
compatibility
proof
let N be multLoopStr;
thus N is MonoidalSubStr of M implies op(N) c= op(M) & un(N) = un(M)
proof
assume
op(N) c= op(M) & for K being multLoopStr st M = K holds un(N) = un(K);
hence thesis;
end;
assume op(N) c= op(M) & un(N) = un(M);
hence
op(N) c= op(M) & for K being multLoopStr st M = K holds un(N) = un(K);
end;
end;
registration
let G be well-unital non empty multLoopStr;
cluster well-unital associative commutative cancelable idempotent invertible
uniquely-decomposable strict for non empty MonoidalSubStr of G;
existence
proof
set a = un(G);
reconsider e = a as Element of {a} by TARSKI:def 1;
set f = the BinOp of {a};
set H = multLoopStr(#{a},f,e#);
A1: a = a*a & dom op(G) = [:carr(G),carr(G):] by Th16,FUNCT_2:def 1;
[a,a] .--> a = {[a,a]} --> a & f = (a,a) .--> a by Th3;
then 1.H = 1.G & op(H) c= op(G) by A1,FUNCT_4:7;
then reconsider H as non empty MonoidalSubStr of G by Def25;
take H;
now
let b be Element of H;
b = a by TARSKI:def 1;
hence op(H).(un(H),b) = b & op(H).(b,un(H)) = b by TARSKI:def 1;
end;
hence un(H) is_a_unity_wrt op(H) by BINOP_1:3;
thus op(H) is associative & op(H) is commutative & op(H) is cancelable &
op(H) is idempotent & op(H) is invertible uniquely-decomposable by Th3;
thus thesis;
end;
end;
theorem Th21:
for G being multMagma, M being MonoidalSubStr of G holds M is SubStr of G
proof
let G be multMagma, M be MonoidalSubStr of G;
thus op(M) c= op(G) by Def24;
end;
definition
let G be multMagma, M be MonoidalExtension of G;
redefine mode SubStr of M -> SubStr of G; :: redefines SubStr (MONOID_0, definition)
coherence
proof
let N be SubStr of M;
the multMagma of M = the multMagma of G by Def22;
hence op(N) c= op(G) by Def23;
end;
end;
definition
let G1 be multMagma, G2 be SubStr of G1;
redefine mode SubStr of G2 -> SubStr of G1; :: redefines SubStr (MONOID_0, definition)
coherence
proof
let G be SubStr of G2;
op(G) c= op(G2) & op(G2) c= op(G1) by Def23;
hence op(G) c= op(G1);
end;
end;
definition
let G1 be multMagma, G2 be MonoidalSubStr of G1;
redefine mode SubStr of G2 -> SubStr of G1; :: redefines SubStr (MONOID_0, definition)
coherence
proof
reconsider H = G2 as SubStr of G1 by Th21;
let G be SubStr of G2;
G is SubStr of H;
hence thesis;
end;
end;
definition
let G be multMagma, M be MonoidalSubStr of G;
redefine mode MonoidalSubStr of M -> MonoidalSubStr of G; :: redefines MonoidalSubStr (MONOID_0, redefinition) → MonoidalSubStr (MONOID_0, definition)
coherence
proof
let M9 be MonoidalSubStr of M;
A1: un(M9) = un(M) by Def24;
op(M9) c= op(M) & op(M) c= op(G) by Def24;
hence op(M9) c= op(G) & for N being multLoopStr st G = N holds
un(M9) = un(N) by A1,Def24;
end;
end;
theorem
G is SubStr of G & M is MonoidalSubStr of M
proof
thus op(G) c= op(G);
thus op(M) c= op(M);
thus thesis;
end;
reserve H for non empty SubStr of G,
N for non empty MonoidalSubStr of G;
theorem Th23:
the carrier of H c= the carrier of G & the carrier of N c= the carrier of G
proof
A1: dom op(N) = [:carr(N), carr(N):] by FUNCT_2:def 1;
A2: dom op(G) = [:carr(G), carr(G):] by FUNCT_2:def 1;
op(H) c= op(G) by Def23;
then
A3: dom op(H) c= dom op(G) by GRFUNC_1:2;
A4: dom op(H) = [:carr(H), carr(H):] by FUNCT_2:def 1;
thus carr(H) c= carr(G)
proof
let x be object;
assume x in carr(H);
then [x,x] in dom op(H) by A4,ZFMISC_1:87;
hence thesis by A3,A2,ZFMISC_1:87;
end;
let x be object;
op(N) c= op(G) by Def24;
then
A5: dom op(N) c= dom op(G) by GRFUNC_1:2;
assume x in carr(N);
then [x,x] in dom op(N) by A1,ZFMISC_1:87;
hence thesis by A5,A2,ZFMISC_1:87;
end;
theorem Th24:
for G being non empty multMagma, H being non empty SubStr of G
holds the multF of H = (the multF of G)||the carrier of H
proof
let G be non empty multMagma, H be non empty SubStr of G;
op(H) c= op(G) & dom op(H) = [:carr(H),carr(H):] by Def23,FUNCT_2:def 1;
hence thesis by GRFUNC_1:23;
end;
theorem Th25:
for a,b being Element of H, a9,b9 being Element of G st
a = a9 & b = b9 holds a*b = a9*b9
proof
let a,b be Element of H, a9,b9 be Element of G such that
A1: a = a9 & b = b9;
A2: dom op(H) = [:carr(H), carr(H):] & op(H) c= op(G) by Def23,FUNCT_2:def 1;
thus a*b = op(H).[a,b] .= a9*b9 by A1,A2,GRFUNC_1:2;
end;
theorem Th26:
for H1,H2 being non empty SubStr of G st
the carrier of H1 = the carrier of H2 holds
the multMagma of H1 = the multMagma of H2
proof
let H1,H2 be non empty SubStr of G;
A1: op(H2) c= op(G) by Def23;
op(H1) c= op(G) & dom op(H1) = [:carr(H1), carr(H1):] by Def23,FUNCT_2:def 1;
then
A2: op(H1) = op(G)||carr(H1) by GRFUNC_1:23;
assume
A3: carr(H1) = carr(H2);
then dom op(H2) = [:carr(H1), carr(H1):] by FUNCT_2:def 1;
hence thesis by A3,A1,A2,GRFUNC_1:23;
end;
theorem
for H1,H2 being non empty MonoidalSubStr of M st
the carrier of H1 = the carrier of H2 holds
the multLoopStr of H1 = the multLoopStr of H2
proof
let H1,H2 be non empty MonoidalSubStr of M such that
A1: the carrier of H1 = the carrier of H2;
reconsider N1 = H1, N2 = H2 as SubStr of M by Th21;
A2: un(H1) = un(M) & un(H2) = un(M) by Def25;
the multMagma of N1 = the multMagma of N2 by A1,Th26;
hence thesis by A2;
end;
theorem Th28:
for H1,H2 being non empty SubStr of G st
the carrier of H1 c= the carrier of H2 holds H1 is SubStr of H2
proof
let H1,H2 be non empty SubStr of G;
assume carr(H1) c= carr(H2);
then [:carr(H1), carr(H1):] c= [:carr(H2), carr(H2):] by ZFMISC_1:96;
then
A1: op(G)||carr(H2)||carr(H1) = op(G)||carr(H1) by FUNCT_1:51;
op(H2) c= op(G) & dom op(H2) = [:carr(H2), carr(H2):] by Def23,FUNCT_2:def 1;
then
A2: op(H2) = op(G)||carr(H2) by GRFUNC_1:23;
op(H1) c= op(G) & dom op(H1) = [:carr(H1), carr(H1):] by Def23,FUNCT_2:def 1;
then op(H1) = op(G)||carr(H1) by GRFUNC_1:23;
hence op(H1) c= op(H2) by A1,A2,RELAT_1:59;
end;
theorem
for H1,H2 being non empty MonoidalSubStr of M st
the carrier of H1 c= the carrier of H2 holds
H1 is MonoidalSubStr of H2
proof
let H1,H2 be non empty MonoidalSubStr of M such that
A1: carr(H1) c= carr(H2);
H1 is SubStr of M & H2 is SubStr of M by Th21;
then H1 is SubStr of H2 by A1,Th28;
hence op(H1) c= op(H2) by Def23;
un(H1) = un(M) by Def25;
hence thesis by Def25;
end;
theorem Th30:
G is unital & the_unity_wrt the multF of G in the carrier of H implies
H is unital &
the_unity_wrt the multF of G = the_unity_wrt the multF of H
proof
set e9 = the_unity_wrt op(G);
assume G is unital;
then
A1: e9 is_a_unity_wrt op(G) by Th4;
assume the_unity_wrt op(G) in carr(H);
then reconsider e = the_unity_wrt op(G) as Element of H;
A2: now
let a be Element of H;
carr(H) c= carr(G) by Th23;
then reconsider a9 = a as Element of G;
thus e*a = e9*a9 by Th25
.= a by A1,BINOP_1:3;
thus a*e = a9*e9 by Th25
.= a by A1,BINOP_1:3;
end;
hence H is unital;
now
let a be Element of H;
e*a = op(H).(e,a) & a*e = op(H).(a,e);
hence op(H).(e,a) = a & op(H).(a,e) = a by A2;
end;
then e is_a_unity_wrt op(H) by BINOP_1:3;
hence thesis by BINOP_1:def 8;
end;
theorem Th31:
for M being well-unital non empty multLoopStr
for N being non empty MonoidalSubStr of M holds
N is well-unital
proof
let M be well-unital non empty multLoopStr,
N be non empty MonoidalSubStr of M;
A1: un(M) is_a_unity_wrt op(M) by Def21;
A2: N is SubStr of M & un(N) = un(M) by Def24,Th21;
now
let a be Element of N;
carr(N) c= carr(M) by Th23;
then reconsider a9 = a as Element of M;
thus op(N).(un(N),a) = (un(N))*a .= (un(M))*a9 by A2,Th25
.= a by A1,BINOP_1:3;
thus op(N).(a,un(N)) = a*(un(N)) .= a9*(un(M)) by A2,Th25
.= a by A1,BINOP_1:3;
end;
hence un(N) is_a_unity_wrt op(N) by BINOP_1:3;
end;
theorem Th32:
G is commutative implies H is commutative
proof
assume
A1: G is commutative;
now
let a,b be Element of H;
carr(H) c= carr(G) by Th23;
then reconsider a9 = a, b9 = b as Element of G;
thus a*b = a9*b9 by Th25
.= b9*a9 by A1
.= b*a by Th25;
end;
hence thesis;
end;
theorem Th33:
G is associative implies H is associative
proof
assume
A1: G is associative;
now
let a,b,c be Element of H;
carr(H) c= carr(G) by Th23;
then reconsider
a9 = a, b9 = b, c9 = c, ab = a*b, bc = b*c as Element of G;
thus a*b*c = ab*c9 by Th25
.= a9*b9*c9 by Th25
.= a9*(b9*c9) by A1
.= a9*bc by Th25
.= a*(b*c) by Th25;
end;
hence thesis;
end;
theorem Th34:
G is idempotent implies H is idempotent
proof
assume
A1: G is idempotent;
A2: carr(H) c= carr(G) by Th23;
now
let a be Element of H;
reconsider a9 = a as Element of G by A2;
thus a*a = a9*a9 by Th25
.= a by A1,Th7;
end;
hence thesis by Th7;
end;
theorem Th35:
G is cancelable implies H is cancelable
proof
assume
A1: G is cancelable;
A2: carr(H) c= carr(G) by Th23;
now
let a,b,c be Element of H;
reconsider a9 = a, b9 = b, c9 = c as Element of G by A2;
A3: b*a = b9*a9 & c*a = c9*a9 by Th25;
a*b = a9*b9 & a*c = a9*c9 by Th25;
hence a*b = a*c or b*a = c*a implies b = c by A1,A3,Th13;
end;
hence thesis by Th13;
end;
theorem Th36:
the_unity_wrt the multF of G in the carrier of H &
G is uniquely-decomposable implies H is uniquely-decomposable
proof
assume
A1: the_unity_wrt op(G) in carr(H);
assume that
A2: op(G) is having_a_unity and
A3: for a,b being Element of G st op(G).(a,b) = the_unity_wrt op(G)
holds a = b & b = the_unity_wrt op(G);
A4: G is unital by A2;
then H is unital by A1,Th30;
hence op(H) is having_a_unity;
let a,b be Element of H;
carr(H) c= carr(G) by Th23;
then reconsider a9 = a, b9 = b as Element of G;
A5: op(H).(a,b) = a*b .= a9*b9 by Th25
.= op(G).(a9,b9);
the_unity_wrt op(G) = the_unity_wrt op(H) by A1,A4,Th30;
hence thesis by A3,A5;
end;
theorem Th37:
for M being well-unital uniquely-decomposable non empty
multLoopStr for N being non empty MonoidalSubStr of M holds
N is uniquely-decomposable
proof
let M be well-unital uniquely-decomposable non empty multLoopStr;
let N be non empty MonoidalSubStr of M;
A1: un(M) = un(N) by Def25;
N is SubStr of M & un(M) = the_unity_wrt op(M) by Th17,Th21;
hence thesis by A1,Th36;
end;
registration
let G be constituted-Functions non empty multMagma;
cluster -> constituted-Functions for non empty SubStr of G;
coherence
proof
let H be non empty SubStr of G;
let a be Element of H;
carr(H) c= carr(G) by Th23;
then a is Element of G;
hence thesis;
end;
cluster -> constituted-Functions for non empty MonoidalSubStr of G;
coherence
proof
let H be non empty MonoidalSubStr of G;
let a be Element of H;
carr(H) c= carr(G) by Th23;
then a is Element of G;
hence thesis;
end;
end;
registration
let G be constituted-FinSeqs non empty multMagma;
cluster -> constituted-FinSeqs for non empty SubStr of G;
coherence
proof
let H be non empty SubStr of G;
let a be Element of H;
carr(H) c= carr(G) by Th23;
then a is Element of G;
hence thesis;
end;
cluster -> constituted-FinSeqs for non empty MonoidalSubStr of G;
coherence
proof
let H be non empty MonoidalSubStr of G;
let a be Element of H;
carr(H) c= carr(G) by Th23;
then a is Element of G;
hence thesis;
end;
end;
registration
let M be well-unital non empty multLoopStr;
cluster -> well-unital for non empty MonoidalSubStr of M;
coherence by Th31;
end;
registration
let G be commutative non empty multMagma;
cluster -> commutative for non empty SubStr of G;
coherence by Th32;
cluster -> commutative for non empty MonoidalSubStr of G;
coherence
proof
let N be non empty MonoidalSubStr of G;
N is SubStr of G by Th21;
hence thesis;
end;
end;
registration
let G be associative non empty multMagma;
cluster -> associative for non empty SubStr of G;
coherence by Th33;
cluster -> associative for non empty MonoidalSubStr of G;
coherence
proof
let N be non empty MonoidalSubStr of G;
N is SubStr of G by Th21;
hence thesis;
end;
end;
registration
let G be idempotent non empty multMagma;
cluster -> idempotent for non empty SubStr of G;
coherence by Th34;
cluster -> idempotent for non empty MonoidalSubStr of G;
coherence
proof
let N be non empty MonoidalSubStr of G;
N is SubStr of G by Th21;
hence thesis;
end;
end;
registration
let G be cancelable non empty multMagma;
cluster -> cancelable for non empty SubStr of G;
coherence by Th35;
cluster -> cancelable for non empty MonoidalSubStr of G;
coherence
proof
let N be non empty MonoidalSubStr of G;
N is SubStr of G by Th21;
hence thesis;
end;
end;
registration
let M be well-unital uniquely-decomposable non empty multLoopStr;
cluster -> uniquely-decomposable for non empty MonoidalSubStr of M;
coherence by Th37;
end;
Lm5:
now let G be non empty multMagma, D be non empty Subset of G;
assume
A1: for x,y being Element of D holds x*y in D;
thus ex H being strict non empty SubStr of G st the carrier of H = D
proof
set op = the multF of G, carr = the carrier of G;
A2: dom op = [:carr,carr:] by FUNCT_2:def 1;
A3: rng (op||D) c= D
proof
let x be object;
assume x in rng (op||D);
then consider y being object such that
A4: y in dom (op||D) and
A5: x = (op||D).y by FUNCT_1:def 3;
reconsider y as Element of [:D,D:] by A2,A4,RELAT_1:62;
reconsider y1 = y`1, y2 = y`2 as Element of D;
y = [y1,y2] by MCART_1:21;
then x = y1*y2 by A4,A5,FUNCT_1:47;
hence thesis by A1;
end;
dom (op||D) = [:D,D:] by A2,RELAT_1:62;
then reconsider f = op||D as BinOp of D by A3,FUNCT_2:def 1,RELSET_1:4;
f c= op by RELAT_1:59;
then reconsider H = multMagma(#D,f#) as strict non empty SubStr of G
by Def23;
take H;
thus thesis;
end;
end;
scheme
SubStrEx2 {G() -> non empty multMagma, P[object]} :
ex H being strict non empty SubStr of G() st
for x being Element of G() holds
x in the carrier of H iff P[x]
provided
A1: for x,y being Element of G() holds P[x] & P[y] implies P[x*y] and
A2: ex x being Element of G() st P[x]
proof
consider X such that
A3: for x being object holds x in X iff x in carr(G()) & P[x]
from XBOOLE_0:sch 1;
reconsider X as non empty set by A2,A3;
X c= carr(G())
by A3;
then reconsider X as non empty Subset of G();
A4: now
let x,y be Element of X;
( P[x])& P[y] by A3;
then P[x*y] by A1;
hence x*y in X by A3;
end;
consider H being strict non empty SubStr of G() such that
A5: the carrier of H = X by Lm5,A4;
take H;
thus thesis by A3,A5;
end;
scheme
MonoidalSubStrEx2 {G() -> non empty multLoopStr, P[set]}:
ex M being strict non empty MonoidalSubStr of G() st
for x being Element of G() holds x in the carrier of M iff P[x]
provided
A1: for x,y being Element of G() holds P[x] & P[y] implies P[x*y] and
A2: P[1.G()]
proof
reconsider G = G() as non empty multMagma;
A3: ex x being Element of G st P[x] by A2;
A4: for x,y being Element of G holds P[x] & P[y] implies P[x*y] by A1;
consider H being strict non empty SubStr of G such that
A5: for x being Element of G holds x in the carrier of H iff P[x] from
SubStrEx2(A4,A3);
reconsider e = 1.G() as Element of H by A2,A5;
set M = multLoopStr(#carr(H), op(H), e#);
1.G() = 1.M & the multF of H c= the multF of G() by Def23;
then reconsider M as strict non empty MonoidalSubStr of G() by Def25;
take M;
thus thesis by A5;
end;
notation
let G be multMagma, a,b be Element of G;
synonym a [*] b for a*b;
end;
begin :: Monoids on Nats
definition
func <REAL,+> -> non empty multMagma equals
multMagma(#REAL, addreal#);
coherence;
end;
registration
cluster <REAL,+> -> unital associative invertible commutative cancelable
strict;
coherence by GROUP_1:46;
end;
theorem
x is Element of <REAL,+> iff x is Element of REAL;
theorem Th39:
for N being non empty SubStr of <REAL,+>
for a,b being Element of N, x,y being Real st
a = x & b = y holds a*b = x+y
proof
let N be non empty SubStr of <REAL,+>;
let a,b be Element of N;
carr(N) c= carr(<REAL,+>) by Th23;
then reconsider a9 = a, b9 = b as Element of <REAL,+>;
a*b = a9*b9 by Th25;
hence thesis by BINOP_2:def 9;
end;
theorem Th40:
for N being unital non empty SubStr of <REAL,+> holds
the_unity_wrt the multF of N = 0
proof
let N be unital non empty SubStr of <REAL,+>;
consider a be Element of N such that
A1: for b being Element of N holds a*b = b & b*a = b by Th6;
carr(N) c= REAL by Th23;
then reconsider x = a as Real;
now
let b be Element of N;
a*b = op(N).(a,b) & b*a = op(N).(b,a);
hence op(N).(a,b) = b & op(N).(b,a) = b by A1;
end;
then
A2: a is_a_unity_wrt op(N) by BINOP_1:3;
x+0 = a*a by A1
.= x+x by Th39;
hence thesis by A2,BINOP_1:def 8;
end;
registration
let G be unital non empty multMagma;
cluster associative invertible -> unital cancelable Group-like for non empty
SubStr of G;
coherence;
end;
definition
redefine func INT.Group -> strict non empty SubStr of <REAL,+>; :: redefines INT.Group (GR_CY_1, definition)
coherence
proof
dom addreal = [:REAL,REAL:] by FUNCT_2:def 1;
then
A1: dom (addreal||INT) = [:INT,INT:] by NUMBERS:15,RELAT_1:62,ZFMISC_1:96;
A2: now
let x be object;
assume
A3: x in [:INT,INT:];
then
A4: x = [x`1,x`2] by MCART_1:21;
reconsider i1 = x`1, i2 = x`2 as Element of INT by A3,MCART_1:10;
thus addint.x = addint.(i1,i2) by A3,MCART_1:21
.= addreal.(i1,i2) by GR_CY_1:def 1
.= (addreal||INT).x by A1,A3,A4,FUNCT_1:47;
end;
dom addint = [:INT,INT:] by FUNCT_2:def 1;
then addint = addreal||INT by A1,A2,FUNCT_1:2;
then op(INT.Group) c= op(<REAL,+>) by GR_CY_1:def 3,RELAT_1:59;
hence thesis by Def23;
end;
end;
:: corollary
:: INT.Group is unital commutative associative cancelable invertible;
theorem
for G being strict non empty SubStr of <REAL,+> holds G = INT.Group
iff the carrier of G = INT by Th26,GR_CY_1:def 3;
theorem
x is Element of INT.Group iff x is Integer by GR_CY_1:def 3,INT_1:def 2;
definition
func <NAT,+> -> unital uniquely-decomposable strict non empty SubStr of
INT.Group means
: Def27:
the carrier of it = NAT;
existence
proof
set f = addint||NAT;
dom addint = [:INT,INT:] by FUNCT_2:def 1;
then
A1: dom f = [:NAT,NAT:] by NUMBERS:17,RELAT_1:62,ZFMISC_1:96;
rng f c= NAT
proof
let x be object;
assume x in rng f;
then consider y being object such that
A2: y in dom f and
A3: x = f.y by FUNCT_1:def 3;
reconsider n1 = y`1, n2 = y`2 as Element of NAT by A1,A2,MCART_1:10;
reconsider i1 = n1, i2 = n2 as Integer;
x = addint.y by A2,A3,FUNCT_1:47
.= addint.(i1,i2) by A1,A2,MCART_1:21
.= n1+n2 by BINOP_2:def 20;
hence thesis by ORDINAL1:def 12;
end;
then reconsider f as BinOp of NAT by A1,FUNCT_2:def 1,RELSET_1:4;
f c= op(INT.Group) by GR_CY_1:def 3,RELAT_1:59;
then reconsider
N = multMagma(#NAT,f#) as strict non empty SubStr of INT.Group
by Def23;
reconsider a = 0 as Element of N;
A4: now
let b be Element of N;
reconsider n = b as Element of NAT;
thus a*b = 0+n by Th39
.= b;
thus b*a = n+0 by Th39
.= b;
end;
now
let b be Element of N;
thus op(N).(a,b) = a*b .= b by A4;
thus op(N).(b,a) = b*a .= b by A4;
end;
then
A5: a is_a_unity_wrt op(N) by BINOP_1:3;
then
A6: the_unity_wrt op(N) = a by BINOP_1:def 8;
A7: now
let a,b be Element of N such that
A8: a*b = the_unity_wrt op(N);
reconsider n = a, m = b as Element of NAT;
A9: a*b = n+m by Th39;
then a = 0 by A6,A8;
hence a = b & b = the_unity_wrt op(N) by A5,A8,A9,BINOP_1:def 8;
end;
A10: N is unital by A4;
then N is uniquely-decomposable by A7,Th14;
hence thesis by A10;
end;
uniqueness by Th26;
end;
:: corollary
:: <NAT,+> is unital commutative associative cancelable uniquely-decomposable;
definition
func <NAT,+,0> -> well-unital strict non empty MonoidalExtension of <NAT,+>
means
not contradiction;
existence;
uniqueness by Th20;
end;
:: corollary
:: <NAT,+,0> is
:: well-unital commutative associative cancelable uniquely-decomposable;
definition
redefine func addnat equals :: redefines addnat (BINOP_2, definition)
the multF of <NAT,+>;
compatibility
proof
let b be BinOp of NAT;
A1: the carrier of <NAT,+> = NAT by Def27;
now
let n1,n2 be Element of NAT;
thus addnat.(n1,n2) = n1 + n2 by BINOP_2:def 23
.= addint.(n1,n2) by BINOP_2:def 20
.= (addint||NAT).[n1,n2] by FUNCT_1:49
.= (the multF of <NAT,+>).(n1,n2) by A1,Th24,GR_CY_1:def 3;
end;
hence thesis by A1,BINOP_1:2;
end;
end;
theorem Th43:
<NAT,+> = multMagma(#NAT,addnat#) by Def27;
theorem
x is Element of <NAT,+,0> iff x is Element of NAT
proof
carr(<NAT,+,0>) = carr(<NAT,+>) by Th18
.= NAT by Def27;
hence thesis;
end;
theorem
for n1,n2 being Element of NAT, m1,m2 being Element of <NAT,+,0> st
n1 = m1 & n2 = m2 holds m1*m2 = n1+n2
proof
op(<NAT,+,0>) = op(<NAT,+>) by Th18;
then <NAT,+,0> is SubStr of <NAT,+> qua SubStr of <REAL,+> by Def23;
hence thesis by Th39;
end;
theorem
<NAT,+,0> = multLoopStr(#NAT,addnat,0#)
proof
set N = <NAT,+,0>;
the multMagma of N = <NAT,+> & the_unity_wrt op(N) = un(N) by Def22,Th17;
hence thesis by Th40,Th43;
end;
theorem
addnat = addreal||NAT & addnat = addint||NAT
proof
carr(<NAT,+>) = NAT by Def27;
hence thesis by Th24,GR_CY_1:def 3;
end;
theorem
0 is_a_unity_wrt addnat & addnat is uniquely-decomposable
proof
the_unity_wrt addnat = 0 & ex n being Element of NAT st n is_a_unity_wrt
addnat by Th40,Th43,SETWISEO:def 2;
hence 0 is_a_unity_wrt addnat by BINOP_1:def 8;
thus thesis by Def20,Th43;
end;
definition
func <REAL,*> -> unital commutative associative strict non empty multMagma
equals
multMagma(#REAL,multreal#);
coherence by Def10,Def11,Def12;
end;
theorem
x is Element of <REAL,*> iff x is Element of REAL;
theorem Th50:
for N being non empty SubStr of <REAL,*>
for a,b being Element of N, x,y being Real st
a = x & b = y holds a*b = x*y
proof
let N be non empty SubStr of <REAL,*>;
let a,b be Element of N;
carr(N) c= carr(<REAL,*>) by Th23;
then reconsider a9 = a, b9 = b as Element of <REAL,*>;
a*b = a9*b9 by Th25;
hence thesis by BINOP_2:def 11;
end;
theorem
for N being unital non empty SubStr of <REAL,*> holds
the_unity_wrt the multF of N = 0 or the_unity_wrt the multF of N = 1
proof
let N be unital non empty SubStr of <REAL,*>;
set e = the_unity_wrt op(N);
carr(N) c= carr(<REAL,*>) by Th23;
then reconsider x = e as Real;
e is_a_unity_wrt op(N) by Th4;
then e = e*e by BINOP_1:3
.= x*x by Th50;
then x*1 = x*x;
hence thesis by XCMPLX_1:5;
end;
definition
func <NAT,*> -> unital uniquely-decomposable strict non empty SubStr of
<REAL,*> means
:Def31:
the carrier of it = NAT;
existence
proof
set f = multreal||NAT;
A1: dom multreal = [:REAL,REAL:] by FUNCT_2:def 1;
[:NAT,NAT:] c= [:REAL,REAL:] by ZFMISC_1:96,NUMBERS:19;
then
A2: dom f = [:NAT,NAT:] by RELAT_1:62,A1;
rng f c= NAT
proof
let x be object;
assume x in rng f;
then consider y being object such that
A3: y in dom f and
A4: x = f.y by FUNCT_1:def 3;
reconsider n1 = y`1, n2 = y`2 as Element of NAT by A2,A3,MCART_1:10;
x = multreal.y by A3,A4,FUNCT_1:47
.= multreal.(n1,n2) by A2,A3,MCART_1:21
.= n1*n2 by BINOP_2:def 11;
hence thesis by ORDINAL1:def 12;
end;
then reconsider f as BinOp of NAT by A2,FUNCT_2:def 1,RELSET_1:4;
f c= op(<REAL,*>) by RELAT_1:59;
then reconsider
N = multMagma(#NAT,f#) as strict non empty SubStr of <REAL,*>
by Def23;
reconsider a = 1 as Element of N;
A5: now
let b be Element of N;
reconsider n = b as Element of NAT;
thus a*b = 1*n by Th50
.= b;
thus b*a = n*1 by Th50
.= b;
end;
now
let b be Element of N;
thus op(N).(a,b) = a*b .= b by A5;
thus op(N).(b,a) = b*a .= b by A5;
end;
then
A6: a is_a_unity_wrt op(N) by BINOP_1:3;
then
A7: the_unity_wrt op(N) = a by BINOP_1:def 8;
A8: now
let a,b be Element of N such that
A9: a*b = the_unity_wrt op(N);
reconsider n = a, m = b as Element of NAT;
A10: a*b = n*m by Th50;
then a = 1 by A7,A9,NAT_1:15;
hence a = b & b = the_unity_wrt op(N) by A6,A9,A10,BINOP_1:def 8;
end;
A11: N is unital by A5;
then N is uniquely-decomposable by A8,Th14;
hence thesis by A11;
end;
uniqueness by Th26;
end;
:: corollary
:: <NAT,*> is unital commutative associative uniquely-decomposable;
definition
func <NAT,*,1> -> well-unital strict non empty MonoidalExtension of <NAT,*>
means
not contradiction;
uniqueness by Th20;
existence;
end;
:: corollary
:: <NAT,*,1> is well-unital commutative associative uniquely-decomposable;
definition
redefine func multnat equals :: redefines multnat (BINOP_2, definition)
the multF of <NAT,*>;
compatibility
proof
let b be BinOp of NAT;
A1: the carrier of <NAT,*> = NAT by Def31;
now
let n1,n2 be Element of NAT;
thus multnat.(n1,n2) = n1 * n2 by BINOP_2:def 24
.= multreal.(n1,n2) by BINOP_2:def 11
.= (multreal||NAT).[n1,n2] by FUNCT_1:49
.= (the multF of <NAT,*>).(n1,n2) by A1,Th24;
end;
hence thesis by A1,BINOP_1:2;
end;
end;
theorem Th52:
<NAT,*> = multMagma(#NAT,multnat#) by Def31;
theorem
for n1,n2 being Element of NAT, m1,m2 being Element of <NAT,*> st
n1 = m1 & n2 = m2 holds m1*m2 = n1*n2 by Th50;
theorem Th54:
the_unity_wrt the multF of <NAT,*> = 1
proof
carr(<NAT,*>) = NAT by Def31;
hence thesis by Th30,BINOP_2:7;
end;
theorem
for n1,n2 being Element of NAT, m1,m2 being Element of <NAT,*,1> st
n1 = m1 & n2 = m2 holds m1*m2 = n1*n2
proof
let n1,n2 be Element of NAT, m1,m2 be Element of <NAT,*,1>;
the multMagma of <NAT,*,1> = <NAT,*> by Def22;
then reconsider x1 = m1, x2 = m2 as Element of <NAT,*>;
x1*x2 = m1*m2 by Th18;
hence thesis by Th50;
end;
theorem
<NAT,*,1> = multLoopStr(#NAT,multnat,1#)
proof
set N = <NAT,*,1>;
the multMagma of N = <NAT,*> & the_unity_wrt op(N) = un(N) by Def22,Th17;
hence thesis by Def31,Th54;
end;
theorem
multnat = multreal||NAT by Th24,Th52;
theorem
1 is_a_unity_wrt multnat & multnat is uniquely-decomposable
proof
ex n being Element of NAT st n is_a_unity_wrt multnat by SETWISEO:def 2;
hence 1 is_a_unity_wrt multnat by Th52,Th54,BINOP_1:def 8;
thus thesis by Def20,Th52;
end;
begin :: Monoid of finite sequences
definition
let D be set;
func D*+^ -> unital associative cancelable uniquely-decomposable
constituted-FinSeqs strict non empty multMagma means
:Def34:
the carrier of it = D* & for p,q being Element of it holds p [*] q = p^q;
existence
proof
deffunc F(Element of D*,Element of D*) = (($1 qua Element of D*) ^($2 qua
Element of D*));
consider f being BinOp of D* such that
A1: for a,b being Element of D* holds f.(a,b) = F(a,b) from BINOP_1:
sch 4;
set G = multMagma(#D*, f#);
G is constituted-FinSeqs;
then reconsider G as constituted-FinSeqs strict non empty multMagma;
G is unital associative cancelable uniquely-decomposable
proof
set N = G, f = op(N);
<*>D = {};
then reconsider a = {} as Element of N by FINSEQ_1:def 11;
A2: now
let b be Element of N;
thus a[*]b = a^b by A1
.= b by FINSEQ_1:34;
thus b[*]a = b^a by A1
.= b by FINSEQ_1:34;
end;
hence N is unital;
now
let a,b,c be Element of N;
reconsider p = a[*]b, q = b[*]c as Element of N;
thus a*b*c = p^c by A1
.= a^b^c by A1
.= a^(b^c) by FINSEQ_1:32
.= a^q by A1
.= a*(b*c) by A1;
end;
hence N is associative;
now
let a,b,c be Element of N;
A3: b*a = b^a & c*a = c^a by A1;
a*b = a^b & a*c = a^c by A1;
hence a*b = a*c or b*a = c*a implies b = c by A3,FINSEQ_1:33;
end;
hence N is cancelable by Th13;
N is unital by A2;
hence op(N) is having_a_unity;
let a9,b be Element of N;
now
let b be Element of N;
a[*]b = f.(a,b) & b[*]a = f.(b,a);
hence f.(a,b) = b & f.(b,a) = b by A2;
end;
then
A4: a is_a_unity_wrt op(N) by BINOP_1:3;
assume f.(a9,b) = the_unity_wrt op(N);
then
A5: {} = a9[*]b by A4,BINOP_1:def 8
.= a9^b by A1;
then a = b;
hence thesis by A4,A5,BINOP_1:def 8;
end;
then reconsider G as unital associative cancelable uniquely-decomposable
constituted-FinSeqs strict non empty multMagma;
take G;
thus thesis by A1;
end;
uniqueness
proof
let G1,G2 be unital associative cancelable uniquely-decomposable
constituted-FinSeqs strict non empty multMagma such that
A6: carr(G1) = D* and
A7: for p,q being Element of G1 holds p [*] q = p^q and
A8: carr(G2) = D* and
A9: for p,q being Element of G2 holds p [*] q = p^q;
set f1 = op(G1), f2 = op(G2);
now
let a,b be Element of D*;
reconsider a2 = a, b2 = b as Element of G2 by A8;
reconsider a1 = a, b1 = b as Element of G1 by A6;
reconsider p = a, q = b as Element of D*;
a2[*]b2 = p^q & a1[*]b1 = p^q by A7,A9;
hence f1.(a,b) = f2.(a,b);
end;
hence thesis by A6,A8,BINOP_1:2;
end;
end;
definition
let D be set;
func D*+^+<0> -> well-unital strict non empty MonoidalExtension of D*+^
means
not contradiction;
correctness by Th20;
func D-concatenation -> BinOp of D* equals
the multF of D*+^;
correctness
proof
carr(D*+^) = D* by Def34;
hence thesis;
end;
end;
theorem
D*+^ = multMagma(#D*, D-concatenation#) by Def34;
theorem Th60:
for D being set holds
the_unity_wrt the multF of D*+^ = {}
proof
let D be set;
set N = D*+^, f = op(N);
carr(N) = D* & {} = <*>D by Def34;
then reconsider a = {} as Element of N by FINSEQ_1:def 11;
now
let b be Element of N;
thus f.(a,b) = a[*]b .= {}^b by Def34
.= b by FINSEQ_1:34;
thus f.(b,a) = b[*]a .= b^{} by Def34
.= b by FINSEQ_1:34;
end;
then a is_a_unity_wrt op(N) by BINOP_1:3;
hence thesis by BINOP_1:def 8;
end;
theorem Th61:
for D being set holds
the carrier of D*+^+<0> = D* &
the multF of D*+^+<0> = D-concatenation &
1.(D*+^+<0>) = {}
proof
let D be set;
set M = D*+^+<0>;
the multMagma of M = D*+^ & the_unity_wrt op(M) = un(M) by Def22,Th17;
hence thesis by Def34,Th60;
end;
theorem
for a,b being Element of D*+^+<0> holds a [*] b = a^b
proof
let a,b be Element of D*+^+<0>;
the multMagma of D*+^+<0> = D*+^ by Def22;
then reconsider p = a, q = b as Element of D*+^;
thus a [*] b = p [*] q by Th18
.= a^b by Def34;
end;
theorem Th63:
for F being non empty SubStr of D*+^ for p,q being Element of F
holds p[*]q = p^q
proof
let F be non empty SubStr of D*+^, p,q be Element of F;
carr(F) c= carr(D*+^) by Th23;
then reconsider p9 = p, q9 = q as Element of D*+^;
thus p[*]q = p9[*]q9 by Th25
.= p^q by Def34;
end;
theorem
for F being unital non empty SubStr of D*+^ holds
the_unity_wrt the multF of F = {}
proof
let F be unital non empty SubStr of D*+^;
set p = the_unity_wrt op(F);
reconsider q = p as Element of F qua SubStr of D*+^;
q^{} = p by FINSEQ_1:34
.= p[*]p by SETWISEO:15
.= q^q by Th63;
hence thesis by FINSEQ_1:33;
end;
theorem
for F being non empty SubStr of D*+^ st {} is Element of F holds
F is unital & the_unity_wrt the multF of F = {}
proof
let F be non empty SubStr of D*+^;
the_unity_wrt op(D*+^) = {} by Th60;
hence thesis by Th30;
end;
theorem
for A,B being non empty set st A c= B holds A*+^ is SubStr of B*+^
proof
let A,B be non empty set;
carr(A*+^) = A* by Def34;
then
A1: dom op(A*+^) = [:A*,A*:] by FUNCT_2:def 1;
carr(B*+^) = B* by Def34;
then
A2: dom op(B*+^) = [:B*,B*:] by FUNCT_2:def 1;
assume A c= B;
then
A3: A* c= B* by FINSEQ_1:62;
A4: now
let x be object;
assume
A5: x in [:A*,A*:]; then
A6: x`1 in A* & x`2 in A* by MCART_1:10;
then reconsider x1 = x`1, x2 = x`2 as Element of A*+^ by Def34;
reconsider y1 = x`1, y2 = x`2 as Element of B*+^ by A3,A6,Def34;
thus op(A*+^).x = x1[*]x2 by A5,MCART_1:21
.= x1^x2 by Def34
.= y1[*]y2 by Def34
.= op(B*+^).x by A5,MCART_1:21;
end;
[:A*,A*:] c= [:B*,B*:] by A3,ZFMISC_1:96;
hence op(A*+^) c= op(B*+^) by A1,A2,A4,GRFUNC_1:2;
end;
theorem
D-concatenation is having_a_unity &
the_unity_wrt (D-concatenation) = {} &
D-concatenation is associative
proof
multMagma(#D*,D-concatenation#) = D*+^ by Def34;
hence thesis by Th60;
end;
begin :: Monoids of mappings
definition
let X be set;
func GPFuncs X -> constituted-Functions strict multMagma means
:Def37:
the carrier of it = PFuncs(X,X) &
for f,g being Element of it holds f [*] g = g (*) f;
existence
proof
reconsider g = id X as PartFunc of X,X;
set D = PFuncs(X,X);
defpred P[Element of D,Element of D,Element of D] means ex f,g being
PartFunc of X,X st $1 = f & $2 = g & $3 = g(*)f;
A1: for a,b being Element of D ex c being Element of D st P[a,b,c]
proof
let a,b be Element of D;
reconsider f = a, g = b as PartFunc of X,X by PARTFUN1:46;
reconsider c = g*f as Element of D by PARTFUN1:45;
take c, f, g;
thus thesis;
end;
consider f being BinOp of D such that
A2: for a,b being Element of D holds P[a,b,f.(a,b)] from BINOP_1:sch 3
(A1);
set G = multMagma(#D, f#);
G is constituted-Functions;
then reconsider G as constituted-Functions strict multMagma;
take G;
thus carr(G) = PFuncs(X,X);
let g,h be Element of G;
reconsider g9 = g, h9 = h as Element of D;
ex g,h being PartFunc of X,X st g9 = g & h9 = h & f.(g9,h9) = h(*)g by A2;
hence thesis;
end;
uniqueness
proof
let G1,G2 be constituted-Functions strict multMagma such that
A3: carr(G1) = PFuncs(X,X) and
A4: for f,g being Element of G1 holds f [*] g = g(*)f and
A5: carr(G2) = PFuncs(X,X) and
A6: for f,g being Element of G2 holds f [*] g = g(*)f;
set f1 = op(G1), f2 = op(G2);
now
let a,b be Element of G1;
reconsider a9 = a, b9 = b as Element of G2 by A3,A5;
a[*]b = b(*)a & a9[*]b9 = b9(*)a9 by A4,A6;
hence f1.(a,b) = f2.(a,b);
end;
hence thesis by A3,A5,BINOP_1:2;
end;
end;
registration
let X be set;
cluster GPFuncs X -> unital associative non empty;
coherence
proof
set G = GPFuncs X;
reconsider g = id X as PartFunc of X,X;
set D = PFuncs(X,X);
A1: the carrier of GPFuncs X = D by Def37;
A2: now
let f9,g,h be Element of G;
reconsider fg = f9[*]g, gh = g[*]h as Element of G;
thus f9[*]g[*]h = h(*)fg by Def37
.= h(*)(g(*)f9) by Def37
.= h(*)g(*)f9 by RELAT_1:36
.= gh(*)f9 by Def37
.= f9[*](g[*]h) by Def37;
end;
reconsider f1 = g as Element of G by A1,PARTFUN1:45;
now
let h be Element of G;
reconsider j = h as PartFunc of X,X by A1,PARTFUN1:46;
thus f1[*]h = j(*)g by Def37
.= h by PARTFUN1:6;
thus h[*]f1 = g(*)j by Def37
.= h by PARTFUN1:7;
end;
hence thesis by A1,A2;
end;
end;
definition
let X be set;
func MPFuncs X -> well-unital strict non empty MonoidalExtension of GPFuncs
X means
not contradiction;
existence;
uniqueness by Th20;
func X-composition -> BinOp of PFuncs(X,X) equals
the multF of GPFuncs X;
correctness
proof
carr(GPFuncs X) = PFuncs(X,X) by Def37;
hence thesis;
end;
end;
:: corollary
:: MPFuncs X is constituted-Functions strict Monoid;
theorem
x is Element of GPFuncs X iff x is PartFunc of X,X
proof
carr(GPFuncs X) = PFuncs(X,X) by Def37;
hence thesis by PARTFUN1:45,46;
end;
theorem Th69:
the_unity_wrt the multF of GPFuncs X = id X
proof
reconsider g = id X as PartFunc of X,X;
set op = op(GPFuncs X);
A1: carr(GPFuncs X) = PFuncs(X,X) by Def37;
then reconsider f = g as Element of GPFuncs X by PARTFUN1:45;
now
let h be Element of GPFuncs X;
reconsider j = h as PartFunc of X,X by A1,PARTFUN1:46;
thus op.(f,h) = f[*]h .= j(*)g by Def37
.= h by PARTFUN1:6;
thus op.(h,f) = h[*]f .= g(*)j by Def37
.= h by PARTFUN1:7;
end;
then f is_a_unity_wrt op by BINOP_1:3;
hence thesis by BINOP_1:def 8;
end;
theorem Th70:
for F being non empty SubStr of GPFuncs X
for f,g being Element of F holds f [*] g = g (*) f
proof
let F be non empty SubStr of GPFuncs X;
let f,g be Element of F;
carr(F) c= carr(GPFuncs X) by Th23;
then reconsider f9 = f, g9 = g as Element of GPFuncs X;
f[*]g = f9[*]g9 by Th25;
hence thesis by Def37;
end;
theorem Th71:
for F being non empty SubStr of GPFuncs X st
id X is Element of F holds
F is unital & the_unity_wrt the multF of F = id X
proof
let F be non empty SubStr of GPFuncs X;
the_unity_wrt op(GPFuncs X) = id X by Th69;
hence thesis by Th30;
end;
theorem
Y c= X implies GPFuncs Y is SubStr of GPFuncs X
proof
carr(GPFuncs Y) = PFuncs(Y,Y) by Def37;
then
A1: dom op(GPFuncs Y) = [:PFuncs(Y,Y),PFuncs(Y,Y):] by FUNCT_2:def 1;
carr(GPFuncs X) = PFuncs(X,X) by Def37;
then
A2: dom op(GPFuncs X) = [:PFuncs(X,X),PFuncs(X,X):] by FUNCT_2:def 1;
assume Y c= X;
then
A3: PFuncs(Y,Y) c= PFuncs(X,X) by PARTFUN1:50;
A4: now
let x be object;
assume
A5: x in [:PFuncs(Y,Y),PFuncs(Y,Y):];
then
A6: x`1 in PFuncs(Y,Y) & x`2 in PFuncs(Y,Y) by MCART_1:10;
then reconsider x1 = x`1, x2 = x`2 as Element of GPFuncs Y by Def37;
reconsider y1 = x`1, y2 = x`2 as Element of GPFuncs X by A3,A6,Def37;
thus op(GPFuncs Y).x = x1[*]x2 by A5,MCART_1:21
.= x2(*)x1 by Def37
.= y1[*]y2 by Def37
.= op(GPFuncs X).x by A5,MCART_1:21;
end;
[:PFuncs(Y,Y),PFuncs(Y,Y):] c= [:PFuncs(X,X),PFuncs(X,X):] by A3,ZFMISC_1:96;
hence op(GPFuncs Y) c= op(GPFuncs X) by A1,A2,A4,GRFUNC_1:2;
end;
definition
let X be set;
func GFuncs X -> strict SubStr of GPFuncs X means
:Def40:
the carrier of it = Funcs(X,X);
existence
proof
Funcs(X,X) c= PFuncs(X,X) by FUNCT_2:72;
then reconsider F = Funcs(X,X) as non empty Subset of GPFuncs X by Def37;
A1: for x,y being Element of F holds x [*] y in F
proof
let x,y be Element of F;
reconsider f = x, g = y as Function of X,X by FUNCT_2:66;
x[*]y = g*f by Def37;
hence thesis by FUNCT_2:9;
end;
consider G being strict non empty SubStr of GPFuncs X such that
A2: the carrier of G = F by Lm5,A1;
take G;
thus thesis by A2;
end;
uniqueness by Th26;
end;
registration
let X be set;
cluster GFuncs X -> unital non empty;
coherence
proof
A1: the carrier of GFuncs X = Funcs(X,X) by Def40;
id X in Funcs(X,X) by FUNCT_2:9;
hence thesis by A1,Th71;
end;
end;
:: corollary
:: GFuncs X is unital associative constituted-Functions;
definition
let X be set;
func MFuncs X -> well-unital strict MonoidalExtension of GFuncs X means
not contradiction;
correctness by Th20;
end;
:: corollary
:: GFuncs X is constituted-Functions Monoid;
theorem
x is Element of GFuncs X iff x is Function of X,X
proof
carr(GFuncs X) = Funcs(X,X) by Def40;
hence thesis by FUNCT_2:9,66;
end;
theorem Th74:
the multF of GFuncs X = (X-composition)||Funcs(X,X)
proof
A1: carr(GFuncs X) = Funcs(X,X) by Def40;
op(GFuncs X) c= op(GPFuncs X) & dom op(GFuncs X) = [:carr(GFuncs X),
carr( GFuncs X):] by Def23,FUNCT_2:def 1;
hence thesis by A1,GRFUNC_1:23;
end;
theorem Th75:
the_unity_wrt the multF of GFuncs X = id X
proof
id X in Funcs(X,X) & carr(GFuncs X) = Funcs(X,X) by Def40,FUNCT_2:9;
hence thesis by Th71;
end;
theorem
the carrier of MFuncs X = Funcs(X,X) &
the multF of MFuncs X = (X-composition)||Funcs(X,X) &
1.MFuncs X = id X
proof
the_unity_wrt op(GFuncs X) = id X & the multMagma of MFuncs X = GFuncs X
by Def22,Th75;
hence thesis by Def40,Th17,Th74;
end;
definition
let X be set;
func GPerms X -> strict non empty SubStr of GFuncs X means :Def42:
for f being Element of GFuncs X holds f in the carrier of it iff
f is Permutation of X;
existence
proof
defpred P[Element of GFuncs X] means $1 is Permutation of X;
A1: ex x being Element of GFuncs X st P[x]
proof
set f = the Permutation of X;
carr(GFuncs X) = Funcs(X,X) by Def40;
then reconsider x = f as Element of GFuncs X by FUNCT_2:9;
take x;
thus thesis;
end;
carr(GFuncs X) = Funcs(X,X) by Def40;
then reconsider f = id X as Element of GFuncs X by FUNCT_2:9;
A2: for x,y being Element of GFuncs X st P[x] & P[y] holds P[x [*] y]
proof
let x,y be Element of GFuncs X;
assume x is Permutation of X & y is Permutation of X;
then reconsider f = x, g = y as Permutation of X;
x[*]y = g*f by Th70;
hence thesis;
end;
consider G being strict non empty SubStr of GFuncs X such that
A3: for f being Element of GFuncs X holds f in the carrier of G iff P[
f] from SubStrEx2(A2,A1);
take G;
thus thesis by A3;
end;
uniqueness
proof
let G1,G2 be strict non empty SubStr of GFuncs X such
that
A4: for f being Element of GFuncs X holds f in carr(G1) iff f is
Permutation of X and
A5: for f being Element of GFuncs X holds f in carr(G2) iff f is
Permutation of X;
A6: carr(G2) c= carr(GFuncs X) by Th23;
A7: carr(G1) c= carr(GFuncs X) by Th23;
carr(G1) = carr(G2)
proof
thus carr(G1) c= carr(G2)
proof
let x be object;
assume
A8: x in carr(G1);
then reconsider f = x as Element of GFuncs X by A7;
f is Permutation of X by A4,A8;
hence thesis by A5;
end;
let x be object;
assume
A9: x in carr(G2);
then reconsider f = x as Element of GFuncs X by A6;
f is Permutation of X by A5,A9;
hence thesis by A4;
end;
hence thesis by Th26;
end;
end;
registration
let X be set;
cluster GPerms X -> unital invertible;
coherence
proof
set G = GPerms X;
A1: carr(GFuncs X) = Funcs(X,X) by Def40;
then reconsider f = id X as Element of GFuncs X by FUNCT_2:9;
f in carr(G) by Def42;
hence G is unital by Th71;
now
reconsider i = f as Element of G by Def42;
let a,b be Element of G;
carr(G) c= carr(GFuncs X) by Th23;
then reconsider a9 = a, b9 = b as Element of GFuncs X;
reconsider f = a9, g = b9 as Permutation of X by Def42;
A2: i = f(*)(f") & i = f"(*)f by FUNCT_2:61;
reconsider f9 = f" as Element of GFuncs X by A1,FUNCT_2:9;
A3: g(*)i = g & i(*)g = g by FUNCT_2:17;
reconsider f9 as Element of G by Def42;
reconsider r = f9[*]b, l = b[*]f9 as Element of G;
take r,l;
A4: i[*]b = g(*)id X & b[*]i = id X(*)g by Th70;
a[*]f9 = f"(*)f & f9[*]a = f(*)(f") by Th70;
hence a[*]r = b & l[*]a = b by A2,A3,A4,Lm1;
end;
hence thesis by Th10;
end;
end;
:: corollary
:: GPerms X is constituted-Functions Group;
theorem Th77:
x is Element of GPerms X iff x is Permutation of X
proof
A1: x is Permutation of X implies x in Funcs(X,X) by FUNCT_2:9;
carr(GPerms X) c= carr(GFuncs X) by Th23;
then
A2: x is Element of GPerms X implies x is Element of GFuncs X;
carr(GFuncs X) = Funcs(X,X) by Def40;
hence thesis by A1,A2,Def42;
end;
theorem Th78:
the_unity_wrt the multF of GPerms X = id X & 1_GPerms X = id X
proof
reconsider i = id X as Element of GPerms X by Th77;
now
let a be Element of GPerms X;
reconsider f = a as Permutation of X by Th77;
a[*]i = i(*)a by Th70;
then
A1: op(GPerms X).(a,i) = i(*)f;
i[*]a = a(*)i by Th70;
hence op(GPerms X).(i,a) = a & op(GPerms X).(a,i) = a by A1,FUNCT_2:17;
end;
then i is_a_unity_wrt op(GPerms X) by BINOP_1:3;
hence the_unity_wrt op(GPerms X) = id X by BINOP_1:def 8;
hence thesis by GROUP_1:22;
end;
theorem
for f being Element of GPerms X holds f" = (f qua Function)"
proof
let f be Element of GPerms X;
reconsider g = f as Permutation of X by Th77;
A1: g(*)(g") = id X & g"(*)g = id X by FUNCT_2:61;
reconsider b = g" as Element of GPerms X by Th77;
reconsider b as Element of GPerms X;
A2: b[*]f = g(*)(g") by Th70;
id X = 1_GPerms X & f[*]b = g"(*)g by Th70,Th78;
hence thesis by A1,A2,GROUP_1:def 5;
end;
:: 2005.05.13, A.T.
theorem
for S being 1-sorted st the carrier of S is functional holds
S is constituted-Functions;
theorem
for G be non empty multMagma, D be non empty Subset of G st
for x,y being Element of D holds x*y in D
ex H being strict non empty SubStr of G st the carrier of H = D
by Lm5;
theorem
for G be non empty multLoopStr, D be non empty Subset of G st
(for x,y being Element of D holds x*y in D) & 1.G in D
ex H being strict non empty MonoidalSubStr of G st the carrier of H = D
proof let G be non empty multLoopStr, D be non empty Subset of G;
assume that
A1: for x,y being Element of D holds x*y in D and
A2: 1.G in D;
thus ex H being strict non empty MonoidalSubStr of G st the carrier of H = D
proof
consider H being strict non empty SubStr of G such that
A3: the carrier of H = D by Lm5,A1;
reconsider e = 1.G as Element of H by A2,A3;
set N = multLoopStr(#the carrier of H, the multF of H, e#);
op(N) c= op(G) & for M being multLoopStr st G = M holds 1.N = 1.M by Def23;
then reconsider N as strict non empty MonoidalSubStr of G by Def25;
take N;
thus thesis by A3;
end;
end;
registration
let D be set;
cluster the carrier of D*+^ -> FinSequence-membered;
coherence
proof
the carrier of D*+^ = D* by Def34;
hence thesis;
end;
cluster the carrier of D*+^+<0> -> FinSequence-membered;
coherence
proof
the carrier of D*+^+<0> = D* by Th61;
hence thesis;
end;
end;