### The Mizar article:

### Monoids

**by****Grzegorz Bancerek**

- Received December 29, 1992
Copyright (c) 1992 Association of Mizar Users

- MML identifier: MONOID_0
- [ MML identifier index ]

environ vocabulary VECTSP_1, BINOP_1, FUNCT_1, FINSEQ_1, RELAT_1, FUNCT_2, PARTFUN1, CAT_1, ALGSTR_1, SETWISEO, FUNCOP_1, GROUP_1, FINSEQOP, VECTSP_2, MCART_1, REALSET1, GR_CY_1, INT_1, BOOLE, MONOID_0; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, REAL_1, MCART_1, DOMAIN_1, NAT_1, STRUCT_0, RELAT_1, FINSEQOP, FUNCT_1, FINSEQ_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FINSEQ_2, INT_1, VECTSP_1, VECTSP_2, SETWISEO, FUNCOP_1, GROUP_1, FUNCT_4, GR_CY_1; constructors DOMAIN_1, NAT_1, BINOP_1, PARTFUN1, SETWISEO, FINSEQOP, GR_CY_1, VECTSP_2, REAL_1, MEMBERED, RELAT_2, XBOOLE_0; clusters SUBSET_1, FUNCT_1, FINSEQ_1, INT_1, VECTSP_1, GROUP_1, RELSET_1, STRUCT_0, PARTFUN1, FUNCOP_1, MEMBERED, ZFMISC_1, FUNCT_2, XBOOLE_0, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, BINOP_1, SETWISEO, FINSEQOP, GROUP_1, VECTSP_1, STRUCT_0, VECTSP_2, XBOOLE_0; theorems TARSKI, NAT_1, INT_1, LANG1, FINSEQ_1, BINOP_1, GROUP_1, FINSEQOP, SETWISEO, VECTSP_1, MCART_1, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_4, FUNCOP_1, PARTFUN1, RVSUM_1, GR_CY_1, GRFUNC_1, RELAT_1, STRUCT_0, RELSET_1, VECTSP_2, XBOOLE_1, XCMPLX_1; 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(HGrStr) = the mult 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; definition cluster constituted-Functions 1-sorted; existence proof consider f being Function; take X = 1-sorted(#{f}#); let a be Element of X; thus thesis by TARSKI:def 1; end; cluster constituted-FinSeqs 1-sorted; existence proof consider f being FinSequence; take X = 1-sorted(#{f}#); let a be Element of X; thus thesis by TARSKI:def 1; end; end; definition let X be constituted-Functions 1-sorted; cluster -> Function-like Relation-like Element of X; coherence by Def1; end; definition cluster constituted-FinSeqs -> constituted-Functions 1-sorted; coherence proof let X be 1-sorted such that A1: X is constituted-FinSeqs; let a be Element of carr(X); thus thesis by A1,Def2; end; end; definition cluster constituted-FinSeqs -> constituted-Functions HGrStr; coherence proof now let G be HGrStr; assume G is constituted-FinSeqs; then G is constituted-FinSeqs 1-sorted; hence G is constituted-Functions; end; hence thesis; end; end; definition let X be constituted-FinSeqs 1-sorted; cluster -> FinSequence-like 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*; coherence proof thus p^q is Element of D* by FINSEQ_1:def 11; end; end; Lm1: (for X for f,g being Function of X,X holds f*g is Function of X,X) & (for X for f,g being Permutation of X holds f*g is Permutation of X) & (for X,Y,Z be set for f being PartFunc of X,Y for g being PartFunc of Y,Z holds g*f is PartFunc of X,Z) & (for X for A,B be non empty set for f being Function of X,A for g be Function of A,B holds g*f is Function of X,B); definition let g,f be Function; redefine func f*g; synonym f(*)g; end; definition let X be set, g,f be Function of X,X; redefine func f*g -> Function of X,X; coherence by Lm1; end; definition let X be set, g,f be Permutation of X; redefine func f*g -> Permutation of X; coherence by Lm1; 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:Def5: 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 has_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 A2: f.(a,r) = b & 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 & 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 Th2: for D be non empty set, f being BinOp of D holds f is cancelable iff f is left-cancelable right-cancelable proof let D be non empty set, f be BinOp of D; thus f is cancelable implies f is left-cancelable right-cancelable proof assume A1: for a,b,c being Element of D st f.(a,b) = f.(a,c) or f.(b,a) = f.(c,a) holds b = c; hence for a,b,c being Element of D st f.(a,b) = f.(a,c) holds b = c; thus for a,b,c being Element of D st f.(b,a) = f.(c,a) holds b = c by A1; end; assume that A2: for a,b,c being Element of D st f.(a,b) = f.(a,c) holds b = c and A3: for a,b,c being Element of D st f.(b,a) = f.(c,a) holds b = c; thus for a,b,c being Element of D st f.(a,b) = f.(a,c) or f.(b,a) = f.(c,a) holds b = c by A2,A3; end; theorem Th3: for f being BinOp of {x} holds f = {[x,x]} --> x & f has_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: dom f = [:{x},{x}:] & dom ({[x,x]} --> x) = {[x,x]} & [:{x},{x}:] = {[x,x]} by FUNCOP_1:19,FUNCT_2:def 1,ZFMISC_1:35; now let y; assume A2: y in {[x,x]}; then reconsider b = y as Element of [:{x},{x}:] by ZFMISC_1:35; thus f.y = f.b .= x by TARSKI:def 1 .= ({[x,x]} --> x).y by A2,FUNCOP_1:13; end; hence f = {[x,x]} --> x by A1,FUNCT_1:9; A3: now let a,b be Element of {x}; a = x & b = x by TARSKI:def 1; hence a = b; end; then for b being Element of {x} holds f.(a,b) = b & f.(b,a) = b; then A4: a is_a_unity_wrt f by BINOP_1:11; 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 A3; thus for a,b,c being Element of {x} holds f.(a,f.(b,c)) = f.(f.(a,b),c) by A3; thus for a being Element of {x} holds f.(a,a) = a by A3; 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 f.(a,a) = b & f.(a,a) = b by A3; 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 A3; thus ex a being Element of {x} st a is_a_unity_wrt f by A4; let a,b be Element of {x}; thus thesis by A3; end; begin :: Semigroups reserve G for non empty HGrStr, D for non empty set, a,b,c,r,l for Element of G; definition let IT be non empty HGrStr; redefine attr IT is unital means: Def10: the mult of IT has_a_unity; compatibility proof thus IT is unital implies the mult of IT has_a_unity proof given e being Element of IT such that A1: for h being Element of IT holds h * e = h & e * h = h; take e; for a being Element of IT holds (the mult of IT).(e,a) = a & (the mult of IT).(a,e) = a proof let a be Element of IT; thus (the mult of IT).(e,a) = e*a by VECTSP_1:def 10 .= a by A1; thus (the mult of IT).(a,e) = a*e by VECTSP_1:def 10 .= a by A1; end; hence e is_a_unity_wrt the mult of IT by BINOP_1:11; end; given x being Element of IT such that A2: x is_a_unity_wrt the mult of IT; take x; let h be Element of IT; for a holds (the mult of IT).(x,h) = h & (the mult of IT).(h,x) = h by A2,BINOP_1:11; hence h * x = h & x * h = h by VECTSP_1:def 10; end; end; definition let G; redefine attr G is commutative means:Def11: the mult of G is commutative; compatibility proof thus G is commutative implies the mult 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 by VECTSP_1:def 10; hence thesis by A1; end; assume A2: for a,b holds op(G).(a,b) = op(G).(b,a); let a,b; op(G).(a,b) = a*b & op(G).(b,a) = b*a by VECTSP_1:def 10; hence thesis by A2; end; attr G is associative means: Def12: the mult of G is associative; compatibility proof thus G is associative implies the mult of G is associative proof assume A3: a*b*c = a*(b*c); let a,b,c; op(G).(a,b) = a*b & op(G).(b,c) = b*c & op(G).(a*b,c) = a*b*c & op(G).(a,b*c) = a*(b*c) by VECTSP_1:def 10; hence thesis by A3; end; assume A4: for a,b,c holds op(G).(a,op(G).(b,c)) = op(G).(op(G).(a,b),c); let a,b,c; op(G).(a,b) = a*b & op(G).(b,c) = b*c & op(G).(a*b,c) = a*b*c & op(G).(a,b*c) = a*(b*c) by VECTSP_1:def 10; hence thesis by A4; end; end; definition let IT be non empty HGrStr; attr IT is idempotent means the mult of IT is idempotent; attr IT is left-invertible means the mult of IT is left-invertible; attr IT is right-invertible means the mult of IT is right-invertible; attr IT is invertible means:Def16: the mult of IT is invertible; attr IT is left-cancelable means the mult of IT is left-cancelable; attr IT is right-cancelable means the mult of IT is right-cancelable; attr IT is cancelable means the mult of IT is cancelable; attr IT is uniquely-decomposable means:Def20: the mult of IT is uniquely-decomposable; end; definition cluster unital commutative associative cancelable idempotent invertible uniquely-decomposable constituted-Functions constituted-FinSeqs strict (non empty HGrStr); existence proof consider p being FinSequence, o being BinOp of {p}; take G = HGrStr(#{p},o#); thus op(G) has_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 mult of G is_a_unity_wrt the mult 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 mult of G)*a = a & a*(the_unity_wrt the mult of G) = a proof set u = the_unity_wrt the mult 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; a*b = (op(G)).(a,b) & b*a = (op(G)).(b,a) & u = a by A1,BINOP_1:def 8,VECTSP_1:def 10; hence thesis by A1,BINOP_1:11; end; assume A2: u*b = b & b*u = b; take a = u; thus a is_a_left_unity_wrt the mult of G proof let b; a*b = b by A2; hence thesis by VECTSP_1:def 10; end; let b; b*a = b by A2; hence thesis by VECTSP_1:def 10; end; theorem Th6: G is unital iff ex a st for b holds a*b = b & b*a = b proof thus G is unital implies ex a st for b holds a*b = b & b*a = b proof given a such that A1: a is_a_unity_wrt the mult of G; take a; let b; a*b = (op(G)).(a,b) & b*a = (op(G)).(b,a) & a is_a_left_unity_wrt op(G) & a is_a_right_unity_wrt the mult of G by A1,BINOP_1:def 7,VECTSP_1:def 10; hence thesis by BINOP_1:def 5,def 6; end; given a such that A2: a*b = b & b*a = b; take a; thus a is_a_left_unity_wrt the mult of G proof let b; a*b = b by A2; hence thesis by VECTSP_1:def 10; end; let b; b*a = b by A2; hence thesis by VECTSP_1:def 10; end; Lm2: G is commutative iff for a,b holds a*b = b*a proof thus G is commutative implies for a,b holds a*b = b*a proof assume A1: for a,b holds op(G).(a,b) = op(G).(b,a); let a,b; op(G).(a,b) = a*b & op(G).(b,a) = b*a by VECTSP_1:def 10; hence thesis by A1; end; assume A2: a*b = b*a; let a,b; op(G).(a,b) = a*b & op(G).(b,a) = b*a by VECTSP_1:def 10; hence thesis by A2; end; Lm3: G is associative iff for a,b,c holds a*b*c = a*(b*c) proof thus G is associative implies for a,b,c holds a*b*c = a*(b*c) proof assume A1: for a,b,c holds op(G).(a,op(G).(b,c)) = op(G).(op(G).(a,b),c); let a,b,c; op(G).(a,b) = a*b & op(G).(b,c) = b*c & op(G).(a*b,c) = a*b*c & op(G).(a,b*c) = a*(b*c) by VECTSP_1:def 10; hence thesis by A1; end; assume A2: a*b*c = a*(b*c); let a,b,c; op(G).(a,b) = a*b & op(G).(b,c) = b*c & op(G).(a*b,c) = a*b*c & op(G).(a,b*c) = a*(b*c) by VECTSP_1:def 10; hence thesis by A2; end; canceled 2; theorem Th9: 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 a*a = op(G).(a,a) by VECTSP_1:def 10 .= a by A1; end; assume A2: a*a = a; let a; thus op(G).(a,a) = a*a by VECTSP_1:def 10 .= 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,VECTSP_1:def 10; 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,VECTSP_1:def 10; 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,VECTSP_1:def 10; 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,VECTSP_1:def 10; end; theorem Th12: 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,VECTSP_1:def 10; 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,VECTSP_1:def 10; 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; a*b = op(G).(a,b) & a*c = op(G).(a,c) by VECTSP_1:def 10; hence 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) by VECTSP_1:def 10; 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; b*a = op(G).(b,a) & c*a = op(G).(c,a) by VECTSP_1:def 10; hence 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) by VECTSP_1:def 10; hence thesis by A2; end; theorem Th15: 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; a*b = op(G).(a,b) & a*c = op(G).(a,c) & b*a = op(G).(b,a) & c*a = op(G).(c,a) by VECTSP_1:def 10; hence 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; a*b = op(G).(a,b) & a*c = op(G).(a,c) & b*a = op(G).(b,a) & c*a = op(G).(c,a) by VECTSP_1:def 10; hence thesis by A2; end; theorem Th16: G is uniquely-decomposable iff the mult of G has_a_unity & for a,b being Element of G st a*b = the_unity_wrt the mult of G holds a = b & b = the_unity_wrt the mult of G proof thus G is uniquely-decomposable implies op(G) has_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 mult of G proof assume A1: op(G) has_a_unity & 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); hence op(G) has_a_unity; let a,b be Element of G; a*b = op(G).(a,b) by VECTSP_1:def 10; hence thesis by A1; end; assume A2: op(G) has_a_unity & for a,b being Element of G st a*b = the_unity_wrt op(G) holds a = b & b = the_unity_wrt op(G); hence op(G) has_a_unity; let a,b be Element of G; a*b = op(G).(a,b) by VECTSP_1:def 10; hence thesis by A2; end; theorem Th17: G is associative implies (G is invertible iff G is unital & the mult of G has_an_inverseOp) proof assume A1: G is associative; thus G is invertible implies G is unital & op(G) has_an_inverseOp proof assume A2: G is invertible; consider e being Element of G; consider x,y being Element of G such that A3: e*x = e & y*e = e by A2,Th12; A4: now let a; consider b,c such that A5: e*b = a & c*e = a by A2,Th12; thus y*a = a by A1,A3,A5,Lm3; thus a*x = a by A1,A3,A5,Lm3; end; then A6: y*x = x & y*x = y; hence G is unital by A4,Th6; defpred P[Element of G,Element of G] means $1*$2 = x & $2*$1 = x; A7: for a ex b st P[a,b] proof let a; consider b,c such that A8: a*b = x & c*a = x by A2,Th12; take b; c*(a*b) = c*a*b & x*b = b & c*x = c by A1,A4,A6,Lm3; hence thesis by A8; 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 FuncExD(A7); then consider u being UnOp of carr(G) such that A9: for a being Element of G holds P[a,(u.a)];:: from FuncExD(A7); take u; let a; now let b; x*b = op(G).(x,b) & b*x = op(G).(b,x) by VECTSP_1:def 10; hence op(G).(x,b) = b & op(G).(b,x) = b by A4,A6; end; then x is_a_unity_wrt op(G) by BINOP_1:11; then x = the_unity_wrt op(G) & op(G).(a,u.a) = a*(u.a) & op(G).(u.a,a) = (u.a)*a by BINOP_1:def 8,VECTSP_1:def 10; hence thesis by A9; end; assume A10: op(G) has_a_unity; given u being UnOp of carr(G) such that A11: 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 by VECTSP_1:def 10 .= a*(u.a)*c by A1,Lm3 .= op(G).(a*(u.a),c) by VECTSP_1:def 10 .= op(G).(op(G).(a,u.a),c) by VECTSP_1:def 10 .= op(G).(the_unity_wrt op(G),c) by A11,FINSEQOP:def 1 .= c by A10,SETWISEO:23; thus op(G).(r,a) = r*a by VECTSP_1:def 10 .= c*((u.a)*a) by A1,Lm3 .= op(G).(c,(u.a)*a) by VECTSP_1:def 10 .= op(G).(c,op(G).(u.a,a)) by VECTSP_1:def 10 .= op(G).(c,the_unity_wrt op(G)) by A11,FINSEQOP:def 1 .= c by A10,SETWISEO:23; end; Lm4: G is invertible iff G is left-invertible right-invertible proof thus G is invertible implies G is left-invertible right-invertible proof assume op(G) is invertible; hence op(G) is left-invertible right-invertible by Th1; end; assume op(G) is left-invertible right-invertible; hence op(G) is invertible by Th1; end; Lm5: 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 by Th2; end; assume op(G) is left-cancelable right-cancelable; hence op(G) is cancelable by Th2; end; Lm6: G is associative invertible implies G is Group-like proof assume A1: G is associative invertible; then G is unital by Th17; then consider a such that A2: for b holds a*b = b & b*a = b by Th6; take a; let b; thus b*a = b & a*b = b by A2; op(G) is invertible by A1,Def16; then consider l,r being Element of G such that A3: op(G).(b,l) = a & op(G).(r,b) = a by Def5; A4: b*l = a & r*b = a by A3,VECTSP_1:def 10; take l; r = r*a by A2 .= a*l by A1,A4,Lm3 .= l by A2; hence thesis by A3,VECTSP_1:def 10; end; definition cluster associative Group-like -> invertible (non empty HGrStr); coherence proof let G be non empty HGrStr; assume G is associative Group-like; then reconsider G as associative Group-like (non empty HGrStr); G is unital associative & op(G) has_an_inverseOp by GROUP_1:36; hence thesis by Th17; end; cluster associative invertible -> Group-like (non empty HGrStr); coherence by Lm6; end; definition cluster invertible -> left-invertible right-invertible (non empty HGrStr); coherence by Lm4; cluster left-invertible right-invertible -> invertible (non empty HGrStr); coherence by Lm4; cluster cancelable -> left-cancelable right-cancelable (non empty HGrStr); coherence by Lm5; cluster left-cancelable right-cancelable -> cancelable (non empty HGrStr); coherence by Lm5; cluster associative invertible -> unital cancelable (non empty HGrStr); coherence proof let G be non empty HGrStr; assume G is associative invertible; then reconsider G as associative invertible (non empty HGrStr); for a,b,c being Element of G st a*b = a*c or b*a = c*a holds b = c by GROUP_1:14; hence thesis by Th15; end; end; begin :: Monoids deffunc un(multLoopStr) = the unity of $1; reserve M for non empty multLoopStr; definition let IT be non empty multLoopStr; redefine attr IT is well-unital means:Def21: the unity of IT is_a_unity_wrt the mult of IT; compatibility proof thus IT is well-unital implies the unity of IT is_a_unity_wrt the mult of IT proof assume A1: IT is well-unital; thus the unity of IT is_a_left_unity_wrt the mult of IT proof let a be Element of IT; thus (the mult of IT).(the unity of IT,a) = (the unity of IT)*a by VECTSP_1:def 10 .= (1_ IT)*a by VECTSP_1:def 9 .= a by A1,VECTSP_2:def 2; end; let a be Element of IT; thus (the mult of IT).(a,the unity of IT) = a*(the unity of IT) by VECTSP_1:def 10 .= a*(1_ IT) by VECTSP_1:def 9 .= a by A1,VECTSP_2:def 2; end; assume A2: the unity of IT is_a_unity_wrt the mult of IT; let x be Element of IT; A3: the unity of IT is_a_right_unity_wrt the mult of IT by A2,BINOP_1:def 7; thus x*(1_ IT) = x*(the unity of IT) by VECTSP_1:def 9 .= (the mult of IT).(x,the unity of IT) by VECTSP_1:def 10 .= x by A3,BINOP_1:def 6; A4: the unity of IT is_a_left_unity_wrt the mult of IT by A2,BINOP_1:def 7; thus (1_ IT)*x = (the unity of IT)*x by VECTSP_1:def 9 .= (the mult of IT).(the unity of IT,x) by VECTSP_1:def 10 .= x by A4,BINOP_1:def 5; end; end; theorem Th18: M is well-unital iff for a being Element of M holds (the unity of M)*a = a & a*(the unity of M) = a proof A1: M is well-unital iff un(M) is_a_unity_wrt op(M) by Def21; thus M is well-unital implies for a being Element of M holds un(M)*a = a & a*un(M) = a proof assume A2: M is well-unital; let a be Element of M; op(M).(un(M),a) = a & (the mult of M).(a,un(M)) = a by A1,A2,BINOP_1:11; hence thesis by VECTSP_1:def 10; end; assume A3: for a being Element of M holds un(M)*a = a & a*un(M) = a; now let a be Element of M; un(M)*a = a & a*un(M) = a by A3; hence op(M).(un(M),a) = a & op(M).(a,un(M)) = a by VECTSP_1:def 10; end; hence thesis by A1,BINOP_1:11; end; Lm7: for M being non empty multLoopStr st M is well-unital holds M is unital proof let M be non empty multLoopStr; assume un(M) is_a_unity_wrt the mult of M; hence op(M) has_a_unity by SETWISEO:def 2; end; definition cluster well-unital -> unital (non empty multLoopStr); coherence by Lm7; end; theorem Th19: for M being non empty multLoopStr st M is well-unital holds the unity of M = the_unity_wrt the mult of M proof let M be non empty multLoopStr; assume un(M) is_a_unity_wrt the mult of M; hence thesis by BINOP_1:def 8; end; definition let A be non empty set, m be BinOp of A, u be Element of A; cluster multLoopStr(#A,m,u#) -> non empty; coherence by STRUCT_0:def 1; end; definition cluster well-unital commutative associative cancelable idempotent invertible uniquely-decomposable unital constituted-Functions constituted-FinSeqs strict (non empty multLoopStr); existence proof consider p being FinSequence, o being BinOp of {p}, e being 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 & b = p by TARSKI:def 1; hence o.(e,b) = b & o.(b,e) = b; end; hence un(G) is_a_unity_wrt op(G) by BINOP_1:11; 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 HGrStr; mode MonoidalExtension of G -> multLoopStr means:Def22: the HGrStr of it = the HGrStr of G; existence proof consider g being Element of G; take M = multLoopStr(#carr(G), op(G), g#); thus the HGrStr of M = the HGrStr of G; end; end; definition let G be non empty HGrStr; cluster -> non empty MonoidalExtension of G; coherence proof let M be MonoidalExtension of G; the HGrStr of M = the HGrStr of G by Def22; hence the carrier of M is non empty; end; end; theorem Th20: for M being MonoidalExtension of G holds the carrier of M = the carrier of G & the mult of M = the mult of G & for a,b being Element of M, a',b' being Element of G st a = a' & b = b' holds a*b = a'*b' proof let M be MonoidalExtension of G; A1: the HGrStr of M = the HGrStr of G by Def22; hence carr(M) = carr(G) & op(M) = op(G); let a,b be Element of M, a',b' be Element of G; a*b = op(M).(a,b) & a'*b' = op(G).(a',b') by VECTSP_1:def 10; hence thesis by A1; end; definition let G be HGrStr; cluster strict MonoidalExtension of G; existence proof consider g being Element of G; set M = multLoopStr(#carr(G), op(G), g#); the HGrStr of M = the HGrStr of G; then M is MonoidalExtension of G by Def22; hence thesis; end; end; theorem Th21: for G being non empty HGrStr, 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 HGrStr, M be MonoidalExtension of G; A1: the HGrStr of M = the HGrStr of G by Def22; thus G is unital implies M is unital proof assume op(G) has_a_unity; hence op(M) has_a_unity by A1; end; thus G is commutative implies M is commutative proof assume op(G) is commutative; hence op(M) is commutative by A1; end; thus G is associative implies M is associative proof assume op(G) is associative; hence op(M) is associative by A1; end; thus G is invertible implies M is invertible proof assume op(G) is invertible; hence op(M) is invertible by A1; end; thus G is uniquely-decomposable implies M is uniquely-decomposable proof assume op(G) is uniquely-decomposable; hence op(M) is uniquely-decomposable by A1; end; assume op(G) is cancelable; hence op(M) is cancelable by A1; end; definition let G be constituted-Functions HGrStr; cluster -> constituted-Functions MonoidalExtension of G; coherence proof let M be MonoidalExtension of G; let a be Element of M; the HGrStr of M = the HGrStr of G by Def22; then a is Element of G; hence thesis; end; end; definition let G be constituted-FinSeqs HGrStr; cluster -> constituted-FinSeqs MonoidalExtension of G; coherence proof let M be MonoidalExtension of G; let a be Element of M; the HGrStr of M = the HGrStr of G by Def22; then a is Element of G; hence thesis; end; end; definition let G be unital (non empty HGrStr); cluster -> unital MonoidalExtension of G; coherence by Th21; end; definition let G be associative (non empty HGrStr); cluster -> associative MonoidalExtension of G; coherence by Th21; end; definition let G be commutative (non empty HGrStr); cluster -> commutative MonoidalExtension of G; coherence by Th21; end; definition let G be invertible (non empty HGrStr); cluster -> invertible MonoidalExtension of G; coherence by Th21; end; definition let G be cancelable (non empty HGrStr); cluster -> cancelable MonoidalExtension of G; coherence by Th21; end; definition let G be uniquely-decomposable (non empty HGrStr); cluster -> uniquely-decomposable MonoidalExtension of G; coherence by Th21; end; definition let G be unital (non empty HGrStr); cluster well-unital strict MonoidalExtension of G; existence proof set M = multLoopStr(#carr(G), op(G), the_unity_wrt op(G)#); M is MonoidalExtension of G proof thus the HGrStr of M = the HGrStr of G; end; then reconsider M as MonoidalExtension of G; take M; thus un(M) is_a_unity_wrt op(M) by Th4; thus thesis; end; end; theorem Th22: for G being unital (non empty HGrStr) for M1,M2 being well-unital strict MonoidalExtension of G holds M1 = M2 proof let G be unital (non empty HGrStr); let M1,M2 be well-unital strict MonoidalExtension of G; the HGrStr of M1 = the HGrStr of G & the HGrStr of M2 = the HGrStr of G & un(M1) = the_unity_wrt op(M1) & un(M2) = the_unity_wrt op(M2) by Def22,Th19; hence thesis; end; begin :: Subsystems definition let G be HGrStr; mode SubStr of G -> HGrStr means:Def23: the mult of it <= the mult of G; existence; end; definition let G be HGrStr; cluster strict SubStr of G; existence proof the HGrStr of G is SubStr of G by Def23; hence thesis; end; end; definition let G be non empty HGrStr; cluster strict non empty SubStr of G; existence proof the HGrStr of G is SubStr of G by Def23; hence thesis; end; end; definition let G be unital (non empty HGrStr); cluster unital associative commutative cancelable idempotent invertible uniquely-decomposable strict (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; consider f being BinOp of {a}; set H = HGrStr(#{a},f#); f = {[a,a]} --> a & a = a*a & a*a = op(G).(a,a) & op(G).(a,a) = op(G).[a,a] & dom op(G) = [:carr(G),carr(G):] by A1,Th3,BINOP_1:def 1,FUNCT_2:def 1,VECTSP_1:def 10; then op(H) <= op(G) by FUNCT_4:8; then reconsider H as non empty SubStr of G by Def23; take H; thus op(H) has_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 HGrStr; mode MonoidalSubStr of G -> multLoopStr means:Def24: the mult of it <= the mult of G & for M being multLoopStr st G = M holds the unity of it = the unity of M; existence proof consider M being MonoidalExtension of G; A1: the HGrStr of M = the HGrStr of G by Def22; A2: now given M being multLoopStr such that A3: G = M; take M; thus op(M) <= op(G) by A3; thus for N being multLoopStr st G = N holds un(M) = un(N) by A3; end; (ex M being multLoopStr st G = M) or for N being multLoopStr st G = N holds un(M) = un(N); hence thesis by A1,A2; end; end; definition let G be HGrStr; cluster strict MonoidalSubStr of G; existence proof consider N being MonoidalSubStr of G; op(the multLoopStr of N) <= op(G) & for M being multLoopStr st G = M holds un(the multLoopStr of N) = un(M) by Def24; then reconsider N' = the multLoopStr of N as MonoidalSubStr of G by Def24; take N'; thus thesis; end; end; definition let G be non empty HGrStr; cluster strict non empty 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 the unity of the multLoopStr of L = the unity of N; then reconsider M = the multLoopStr of L as MonoidalSubStr of G by Def24; take M; thus M is strict; the carrier of M = the carrier of G; hence the carrier of M is non empty; suppose A1: G is not multLoopStr; consider M being strict MonoidalExtension of G; A2: the HGrStr of M = the HGrStr of G by Def22; for N being multLoopStr st G = N holds the unity of M = the unity of N by A1; then reconsider M as MonoidalSubStr of G by A2,Def24; take M; thus thesis; end; end; definition let M be multLoopStr; redefine mode MonoidalSubStr of M means:Def25: the mult of it <= the mult of M & the unity of it = the unity of M; compatibility proof let N be multLoopStr; thus N is MonoidalSubStr of M implies op(N) <= op(M) & un(N) = un(M) proof assume op(N) <= op(M) & for K being multLoopStr st M = K holds un(N) = un(K); hence thesis; end; assume op(N) <= op(M) & un(N) = un(M); hence op(N) <= op(M) & for K being multLoopStr st M = K holds un(N) = un(K); end; end; definition let G be well-unital (non empty multLoopStr); cluster well-unital associative commutative cancelable idempotent invertible uniquely-decomposable strict (non empty MonoidalSubStr of G); existence proof set a = un(G); reconsider e = a as Element of {a} by TARSKI:def 1; consider f being BinOp of {a}; set H = multLoopStr(#{a},f,e#); f = {[a,a]} --> a & a = a*a & a*a = op(G).(a,a) & op(G).(a,a) = op(G).[a,a] & dom op(G) = [:carr(G),carr(G):] by Th3,Th18,BINOP_1:def 1,FUNCT_2:def 1,VECTSP_1:def 10; then op(H) <= op(G) by FUNCT_4:8; 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:11; 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 Th23: for G being HGrStr, M being MonoidalSubStr of G holds M is SubStr of G proof let G be HGrStr, M be MonoidalSubStr of G; thus op(M) <= op(G) by Def24; end; definition let G be HGrStr, M be MonoidalExtension of G; redefine mode SubStr of M -> SubStr of G; coherence proof let N be SubStr of M; the HGrStr of M = the HGrStr of G by Def22; hence op(N) <= op(G) by Def23; end; end; definition let G1 be HGrStr, G2 be SubStr of G1; redefine mode SubStr of G2 -> SubStr of G1; coherence proof let G be SubStr of G2; op(G) <= op(G2) & op(G2) <= op(G1) by Def23; hence op(G) <= op(G1) by XBOOLE_1:1; end; end; definition let G1 be HGrStr, G2 be MonoidalSubStr of G1; redefine mode SubStr of G2 -> SubStr of G1; coherence proof let G be SubStr of G2; reconsider H = G2 as SubStr of G1 by Th23; G is SubStr of H; hence thesis; end; end; definition let G be HGrStr, M be MonoidalSubStr of G; redefine mode MonoidalSubStr of M -> MonoidalSubStr of G; coherence proof let M' be MonoidalSubStr of M; op(M') <= op(M) & op(M) <= op(G) & un(M') = un(M) & for N being multLoopStr st G = N holds un(M) = un(N) by Def24; hence op(M') <= op(G) & for N being multLoopStr st G = N holds un(M') = un(N) by XBOOLE_1:1; end; end; theorem G is SubStr of G & M is MonoidalSubStr of M proof thus op(G) <= op(G); thus op(M) <= op(M); thus thesis; end; reserve H for non empty SubStr of G, N for non empty MonoidalSubStr of G; theorem Th25: the carrier of H c= the carrier of G & the carrier of N c= the carrier of G proof op(H) <= op(G) & op(N) <= op(G) by Def23,Def24; then A1: dom op(H) c= dom op(G) & dom op(H) = [:carr(H), carr(H):] & dom op(N) c= dom op(G) & dom op(N) = [:carr(N), carr(N):] & dom op(G) = [:carr(G), carr(G):] by FUNCT_2:def 1,GRFUNC_1:8; thus carr(H) c= carr(G) proof let x; assume x in carr(H); then [x,x] in dom op(H) by A1,ZFMISC_1:106; hence thesis by A1,ZFMISC_1: 106; end; let x; assume x in carr(N); then [x,x] in dom op(N) by A1,ZFMISC_1:106; hence thesis by A1,ZFMISC_1:106 ; end; theorem Th26: for G being non empty HGrStr, H being non empty SubStr of G holds the mult of H = (the mult of G)|[:the carrier of H,the carrier of H:] proof let G be non empty HGrStr, H be non empty SubStr of G; op(H) <= op(G) & dom op(H) = [:carr(H),carr(H):] by Def23,FUNCT_2:def 1; hence thesis by GRFUNC_1:64; end; theorem Th27: for a,b being Element of H, a',b' being Element of G st a = a' & b = b' holds a*b = a'*b' proof let a,b be Element of H, a',b' be Element of G such that A1: a = a' & b = b'; A2: dom op(H) = [:carr(H), carr(H):] & op(H) <= op(G) by Def23,FUNCT_2:def 1; thus a*b = op(H).(a,b) by VECTSP_1:def 10 .= op(H).[a,b] by BINOP_1:def 1 .= op(G).[a',b'] by A1,A2,GRFUNC_1:8 .= op(G).(a',b') by BINOP_1:def 1 .= a'*b' by VECTSP_1:def 10; end; theorem Th28: for H1,H2 being non empty SubStr of G st the carrier of H1 = the carrier of H2 holds the HGrStr of H1 = the HGrStr of H2 proof let H1,H2 be non empty SubStr of G; assume A1: carr(H1) = carr(H2); then op(H1) <= op(G) & op(H2) <= op(G) & dom op(H1) = [:carr(H1), carr(H1):] & dom op(H2) = [:carr(H1), carr(H1):] by Def23,FUNCT_2:def 1; then the HGrStr of H1 = HGrStr(#carr(H1), op(H1)#) & the HGrStr of H2 = HGrStr(#carr(H2), op(H2)#) & op(H1) = op(G)|[:carr(H1), carr(H1):] & op(H2) = op(G)|[:carr(H1), carr(H1):] by GRFUNC_1:64; hence thesis by A1; 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 Th23; the HGrStr of N1 = the HGrStr of N2 & un(H1) = un(M) & un(H2) = un(M) by A1,Def25,Th28; hence thesis; end; theorem Th30: 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 op(H1) <= op(G) & op(H2) <= op(G) & dom op(H1) = [:carr(H1), carr(H1):] & [:carr(H1), carr(H1):] c= [:carr(H2), carr(H2):] & dom op(H2) = [:carr(H2), carr(H2):] by Def23,FUNCT_2:def 1,ZFMISC_1:119; then (op(G)|[:carr(H2), carr(H2):])|[:carr(H1), carr(H1):] = op(G)|[:carr(H1), carr(H1):] & op(H1) = op(G)|[:carr(H1), carr(H1):] & op(H2) = op(G)|[:carr(H2), carr(H2):] by FUNCT_1:82,GRFUNC_1:64; hence op(H1) <= op(H2) by RELAT_1:88; 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 Th23; then H1 is SubStr of H2 by A1,Th30; hence op(H1) <= op(H2) by Def23; un(H1) = un(M) & un(H2) = un(M) by Def25; hence thesis; end; theorem Th32: G is unital & the_unity_wrt the mult of G in the carrier of H implies H is unital & the_unity_wrt the mult of G = the_unity_wrt the mult of H proof set e' = the_unity_wrt op(G); assume G is unital; then A1: e' 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 Th25; then reconsider a' = a as Element of G by TARSKI:def 3; thus e*a = e'*a' by Th27 .= op(G).(e',a') by VECTSP_1:def 10 .= a by A1,BINOP_1:11; thus a*e = a'*e' by Th27 .= op(G).(a',e') by VECTSP_1:def 10 .= a by A1,BINOP_1:11; end; hence H is unital by Th6; now let a be Element of H; e*a = op(H).(e,a) & a*e = op(H).(a,e) by VECTSP_1:def 10; 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:11; hence thesis by BINOP_1:def 8; end; theorem Th33: 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: N is SubStr of M by Th23; A2: un(N) = un(M) & un(M) is_a_unity_wrt op(M) by Def21,Def24; now let a be Element of N; carr(N) c= carr(M) by Th25; then reconsider a' = a as Element of M by TARSKI:def 3; thus op(N).(un(N),a) = (un(N))*a by VECTSP_1:def 10 .= (un(M))*a' by A1,A2,Th27 .= op(M).(un(M),a') by VECTSP_1:def 10 .= a by A2,BINOP_1:11; thus op(N).(a,un(N)) = a*(un(N)) by VECTSP_1:def 10 .= a'*(un(M)) by A1,A2,Th27 .= op(M).(a',un(M)) by VECTSP_1:def 10 .= a by A2,BINOP_1:11; end; hence un(N) is_a_unity_wrt op(N) by BINOP_1:11; end; theorem Th34: 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 Th25; then reconsider a' = a, b' = b as Element of G by TARSKI: def 3; thus a*b = a'*b' by Th27 .= b'*a' by A1,Lm2 .= b*a by Th27; end; hence thesis by Lm2; end; theorem Th35: 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 Th25; then reconsider a' = a, b' = b, c' = c, ab = a*b, bc = b*c as Element of G by TARSKI:def 3; thus a*b*c = ab*c' by Th27 .= a'*b'*c' by Th27 .= a'*(b'*c') by A1,Lm3 .= a'*bc by Th27 .= a*(b*c) by Th27; end; hence thesis by Lm3; end; theorem Th36: G is idempotent implies H is idempotent proof assume A1: G is idempotent; then A2: carr(H) c= carr(G) & for a being Element of G holds a* a = a by Th9,Th25; now let a be Element of H; reconsider a' = a as Element of G by A2,TARSKI:def 3; thus a*a = a'*a' by Th27 .= a by A1,Th9; end; hence thesis by Th9; end; theorem Th37: G is cancelable implies H is cancelable proof assume A1: G is cancelable; then A2: carr(H) c= carr(G) & for a,b,c being Element of G st a*b = a*c or b*a = c*a holds b = c by Th15,Th25; now let a,b,c be Element of H; reconsider a' = a, b' = b, c' = c as Element of G by A2,TARSKI:def 3; a*b = a'*b' & a*c = a'*c' & b*a = b'*a' & c*a = c'*a' by Th27; hence a*b = a*c or b*a = c*a implies b = c by A1,Th15; end; hence thesis by Th15; end; theorem Th38: the_unity_wrt the mult 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 A2: op(G) has_a_unity & 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); then G is unital by Def10; then A3: H is unital & the_unity_wrt op(G) = the_unity_wrt op(H) by A1,Th32; hence op(H) has_a_unity by Def10; let a,b be Element of H; carr(H) c= carr(G) by Th25; then reconsider a' = a, b' = b as Element of G by TARSKI:def 3; op(H).(a,b) = a*b by VECTSP_1:def 10 .= a'*b' by Th27 .= op(G).(a',b') by VECTSP_1:def 10; hence thesis by A2,A3; end; theorem Th39: 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; N is SubStr of M & un(M) = the_unity_wrt op(M) & un(M) = un(N) by Def25,Th19,Th23; hence thesis by Th38; end; definition let G be constituted-Functions non empty HGrStr; cluster -> constituted-Functions (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 Th25; then a is Element of G by TARSKI:def 3; hence thesis; end; cluster -> constituted-Functions (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 Th25; then a is Element of G by TARSKI:def 3; hence thesis; end; end; definition let G be constituted-FinSeqs non empty HGrStr; cluster -> constituted-FinSeqs (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 Th25; then a is Element of G by TARSKI:def 3; hence thesis; end; cluster -> constituted-FinSeqs (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 Th25; then a is Element of G by TARSKI:def 3; hence thesis; end; end; definition let M be well-unital (non empty multLoopStr); cluster -> well-unital (non empty MonoidalSubStr of M); coherence by Th33; end; definition let G be commutative (non empty HGrStr); cluster -> commutative (non empty SubStr of G); coherence by Th34; cluster -> commutative (non empty MonoidalSubStr of G); coherence proof let N be non empty MonoidalSubStr of G; N is SubStr of G by Th23; hence thesis by Th34; end; end; definition let G be associative (non empty HGrStr); cluster -> associative (non empty SubStr of G); coherence by Th35; cluster -> associative (non empty MonoidalSubStr of G); coherence proof let N be non empty MonoidalSubStr of G; N is SubStr of G by Th23; hence thesis by Th35; end; end; definition let G be idempotent (non empty HGrStr); cluster -> idempotent (non empty SubStr of G); coherence by Th36; cluster -> idempotent (non empty MonoidalSubStr of G); coherence proof let N be non empty MonoidalSubStr of G; N is SubStr of G by Th23; hence thesis by Th36; end; end; definition let G be cancelable (non empty HGrStr); cluster -> cancelable (non empty SubStr of G); coherence by Th37; cluster -> cancelable (non empty MonoidalSubStr of G); coherence proof let N be non empty MonoidalSubStr of G; N is SubStr of G by Th23; hence thesis by Th37; end; end; definition let M be well-unital uniquely-decomposable (non empty multLoopStr); cluster -> uniquely-decomposable (non empty MonoidalSubStr of M); coherence by Th39; end; scheme SubStrEx1 {G() -> non empty HGrStr, D() -> non empty Subset of G()}: ex H being strict non empty SubStr of G() st the carrier of H = D() provided A1: for x,y being Element of D() holds x*y in D() proof set op = the mult of G(), carr = the carrier of G(); A2: [:D(),D():] c= [:carr,carr:] & dom op = [:carr,carr:] by FUNCT_2:def 1; then A3: dom (op|([:D(),D():] qua set)) = [:D(),D():] by RELAT_1:91; rng (op|([:D(),D():] qua set)) c= D() proof let x; assume x in rng (op|([:D(),D():] qua set)); then consider y such that A4: y in dom (op|([:D(),D():] qua set)) & x = (op|([:D(),D():] qua set)).y by FUNCT_1:def 5; reconsider y as Element of [:D(),D():] by A2,A4,RELAT_1:91; reconsider y1 = y`1, y2 = y`2 as Element of D(); y = [y1,y2] by MCART_1:23; then op.(y1,y2) = op.y by BINOP_1:def 1 .= x by A4,FUNCT_1:70; then x = y1*y2 by VECTSP_1:def 10; hence thesis by A1; end; then reconsider f = op|([:D(),D():] qua set) as BinOp of D() by A3,FUNCT_2: def 1,RELSET_1:11; f <= op by RELAT_1:88; then reconsider H = HGrStr(#D(),f#) as strict non empty SubStr of G() by Def23; take H; thus thesis; end; scheme SubStrEx2 {G() -> non empty HGrStr, P[set]}: 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 defpred Q[set] means P[$1]; consider X such that A3: x in X iff x in carr(G()) & Q[x] from Separation; consider x being Element of G() such that A4: P[x] by A2; reconsider X as non empty set by A3,A4; X c= carr(G()) proof let x; thus thesis by A3; end; then reconsider X as non empty Subset of G(); A5: 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 A6: the carrier of H = X from SubStrEx1(A5); take H; thus thesis by A3,A6; end; scheme MonoidalSubStrEx1 {G() -> non empty multLoopStr, D() -> non empty Subset of G()}: ex H being strict non empty MonoidalSubStr of G() st the carrier of H = D() provided A1: for x,y being Element of D() holds x*y in D() and A2: the unity of G() in D() proof reconsider G = G() as non empty HGrStr; reconsider D = D() as non empty Subset of G; A3: for x,y being Element of D holds x*y in D by A1; consider H being strict non empty SubStr of G such that A4: the carrier of H = D from SubStrEx1(A3); reconsider e = the unity of G() as Element of H by A2,A4; set N = multLoopStr(#the carrier of H, the mult of H, e#); N is MonoidalSubStr of G() proof thus op(N) <= op(G()) by Def23; thus thesis; end; then reconsider N as strict non empty MonoidalSubStr of G(); take N; thus thesis by A4; 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[the unity of G()] proof reconsider G = G() as non empty HGrStr; defpred Q[set] means P[$1]; A3: for x,y being Element of G holds Q[x] & Q[y] implies Q[x*y] by A1; A4: ex x being Element of G st Q[x] by A2; 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 Q[x] from SubStrEx2(A3,A4); reconsider e = the unity of G() as Element of H by A2,A5; the mult of H <= the mult of G() by Def23; then reconsider M = multLoopStr(#carr(H), op(H), e#) as strict non empty MonoidalSubStr of G() by Def25; take M; thus thesis by A5; end; definition let G,a,b; redefine func a*b -> Element of G; coherence; synonym a [*] b; end; begin :: Monoids on natural numbers definition func <REAL,+> -> unital associative invertible commutative cancelable strict (non empty HGrStr) equals:Def26: HGrStr(#REAL, addreal#); coherence proof HGrStr(#REAL, addreal#) is commutative Group by GROUP_1:92; hence thesis; end; end; theorem Th40: the carrier of <REAL,+> = REAL & the mult of <REAL,+> = addreal & for a,b being Element of <REAL,+>, x,y being Real st a = x & b = y holds a*b = x+y proof thus carr(<REAL,+>) = REAL & op(<REAL,+>) = addreal by Def26; let a,b be Element of <REAL,+>, x,y be Real; a*b = op(<REAL,+>).(a,b) & addreal.(x,y) = x+y by VECTSP_1:def 4,def 10; hence thesis by Def26; end; theorem x is Element of <REAL,+> iff x is Real by Th40; theorem the_unity_wrt the mult of <REAL,+> = 0 by Th40,RVSUM_1:4; theorem Th43: 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 Th25; then reconsider a' = a, b' = b as Element of <REAL,+> by TARSKI:def 3; a*b = a'*b' by Th27; hence thesis by Th40; end; theorem Th44: for N being unital (non empty SubStr of <REAL,+>) holds the_unity_wrt the mult 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 Th25,Th40; then reconsider x = a as Real by TARSKI:def 3; x+0 = a*a by A1 .= x+x by Th43; then A2: a = 0 by XCMPLX_1:2; now let b be Element of N; a*b = op(N).(a,b) & b*a = op(N).(b,a) by VECTSP_1:def 10; hence op(N).(a,b) = b & op(N).(b,a) = b by A1; end; then a is_a_unity_wrt op(N) by BINOP_1:11; hence thesis by A2,BINOP_1:def 8; end; definition let G be unital (non empty HGrStr); cluster associative invertible -> unital cancelable Group-like (non empty SubStr of G); coherence proof let H be non empty SubStr of G; assume H is associative invertible; then H is associative invertible (non empty HGrStr); hence thesis; end; end; definition redefine func INT.Group -> unital invertible strict (non empty SubStr of <REAL,+>); coherence proof INT c= REAL proof let x; thus thesis by INT_1:11; end; then A1: INT.Group = HGrStr(#INT,addint#) & dom addint = [:INT,INT:] & [:INT,INT:] c= [:REAL,REAL:] & dom addreal = [:REAL,REAL:] by FUNCT_2:def 1,GR_CY_1:def 4,ZFMISC_1:119; then A2: dom (addreal|[:INT,INT:]) = [:INT,INT:] by RELAT_1:91; now let x; assume A3: x in [:INT,INT:]; then A4: x`1 in INT & x`2 in INT & x = [x`1,x`2] by MCART_1:10,23; reconsider i1 = x`1, i2 = x`2 as Element of INT by A3,MCART_1:10; thus addint.x = addint.(i1,i2) by A4,BINOP_1:def 1 .= addreal.(i1,i2) by GR_CY_1:def 2 .= addreal.x by A4,BINOP_1:def 1 .= (addreal|[:INT,INT:]).x by A2,A3,FUNCT_1:70; end; then A5: addint = addreal|[:INT,INT:] by A1,A2,FUNCT_1:9; INT.Group is SubStr of <REAL,+> proof thus op(INT.Group) <= op(<REAL,+>) by A5,Th40,GR_CY_1:def 4,RELAT_1:88; end; hence thesis; end; end; :: corollary :: INT.Group is unital commutative associative cancelable invertible; canceled; theorem for G being strict non empty SubStr of <REAL,+> holds G = INT.Group iff the carrier of G = INT by Th28,GR_CY_1:def 4; theorem x is Element of INT.Group iff x is Integer by GR_CY_1:def 4,INT_1:12; 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,NAT:] qua set); [:NAT,NAT:] c= [:INT,INT:] & dom addint = [:INT,INT:] by FUNCT_2:def 1,INT_1:14,ZFMISC_1:119; then A1: dom f = [:NAT,NAT:] by RELAT_1:91; rng f c= NAT proof let x; assume x in rng f; then consider y such that A2: y in dom f & x = f.y by FUNCT_1:def 5; reconsider n1 = y`1, n2 = y`2 as Nat by A1,A2,MCART_1:10; reconsider i1 = n1, i2 = n2 as Integer; x = addint.y by A2,FUNCT_1:70 .= addint.[n1,n2] by A2,MCART_1:23 .= addint.(i1,i2) by BINOP_1:def 1 .= n1+n2 by GR_CY_1:14; hence thesis; end; then reconsider f as BinOp of NAT by A1,FUNCT_2:def 1,RELSET_1:11; f <= op(INT.Group) by GR_CY_1:def 4,RELAT_1:88; then reconsider N = HGrStr(#NAT,f#) as strict non empty SubStr of INT.Group by Def23; reconsider a = 0 as Element of N; A3: now let b be Element of N; reconsider n = b as Nat; thus a*b = 0+n by Th43 .= b; thus b*a = n+0 by Th43 .= b; end; then A4: N is unital by Th6; then A5: op(N) has_a_unity by Def10; now let b be Element of N; thus op(N).(a,b) = a*b by VECTSP_1:def 10 .= b by A3; thus op(N).(b,a) = b*a by VECTSP_1:def 10 .= b by A3; end; then A6: a is_a_unity_wrt op(N) by BINOP_1:11; then A7: the_unity_wrt op(N) = a by BINOP_1:def 8; now let a,b be Element of N such that A8: a*b = the_unity_wrt op(N); reconsider n = a, m = b as Nat; a*b = n+m by Th43; then a = 0 & b = 0 by A7,A8,NAT_1:23; hence a = b & b = the_unity_wrt op(N) by A6,BINOP_1:def 8; end; then N is uniquely-decomposable by A5,Th16; hence thesis by A4; end; uniqueness by Th28; 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 Th22; end; :: corollary :: <NAT,+,0> is :: well-unital commutative associative cancelable uniquely-decomposable; definition func addnat -> BinOp of NAT equals:Def29: the mult of <NAT,+>; coherence proof carr(<NAT,+>) = NAT by Def27; hence thesis; end; end; canceled; theorem Th49: <NAT,+> = HGrStr(#NAT,addnat#) by Def27,Def29; theorem x is Element of <NAT,+,0> iff x is Nat proof carr(<NAT,+,0>) = carr(<NAT,+>) by Th20 .= NAT by Def27; hence thesis; end; theorem for n1,n2 being 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 Th20; then <NAT,+,0> is SubStr of <NAT,+> qua SubStr of <REAL,+> by Def23; hence thesis by Th43; end; theorem <NAT,+,0> = multLoopStr(#NAT,addnat,0#) proof set N = <NAT,+,0>; the HGrStr of N = <NAT,+> & the_unity_wrt op(N) = un(N) by Def22,Th19; hence thesis by Th44,Th49; end; theorem addnat = addreal|([:NAT,NAT:] qua set) & addnat = addint|([:NAT,NAT:] qua set ) proof carr(<NAT,+>) = NAT & op(<REAL,+>) = addreal & op(INT.Group) = addint & op(<NAT,+>) = addnat by Def26,Def27,Def29,GR_CY_1:def 4; hence thesis by Th26; end; theorem 0 is_a_unity_wrt addnat & addnat has_a_unity & the_unity_wrt addnat = 0 & addnat is commutative & addnat is associative & addnat is uniquely-decomposable proof A1: addnat has_a_unity & the_unity_wrt addnat = 0 by Def10,Th44,Th49; then ex n being Nat st n is_a_unity_wrt addnat by SETWISEO:def 2; hence 0 is_a_unity_wrt addnat by A1,BINOP_1:def 8; thus thesis by Def10,Def11,Def12,Def20,Th44,Th49; end; definition func <REAL,*> -> unital commutative associative strict (non empty HGrStr) equals:Def30: HGrStr(#REAL,multreal#); coherence proof set R = HGrStr(#REAL,multreal#); R is unital commutative associative proof thus op(R) has_a_unity & op(R) is commutative & op(R) is associative by RVSUM_1:11,12,15; end; hence thesis; end; end; theorem Th55: the carrier of <REAL,*> = REAL & the mult of <REAL,*> = multreal & for a,b being Element of <REAL,*>, x,y being Real st a = x & b = y holds a*b = x*y proof thus carr(<REAL,*>) = REAL & op(<REAL,*>) = multreal by Def30; let a,b be Element of <REAL,*>, x,y be Real; a*b = op(<REAL,*>).(a,b) & multreal.(x,y) = x*y by VECTSP_1:def 10,def 14; hence thesis by Def30; end; theorem x is Element of <REAL,*> iff x is Real by Th55; theorem the_unity_wrt the mult of <REAL,*> = 1 by Th55,RVSUM_1:14; theorem Th58: 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 Th25; then reconsider a' = a, b' = b as Element of <REAL,*> by TARSKI:def 3; a*b = a'*b' by Th27; hence thesis by Th55; end; canceled; theorem for N being unital (non empty SubStr of <REAL,*>) holds the_unity_wrt the mult of N = 0 or the_unity_wrt the mult 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 Th25; then reconsider x = e as Real by Th55,TARSKI:def 3; e is_a_unity_wrt op(N) by Th4; then e = op(N).(e,e)by BINOP_1:11 .= e*e by VECTSP_1:def 10 .= x*x by Th58; 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,NAT:] qua set); [:NAT,NAT:] c= [:REAL,REAL:] & dom multreal = [:REAL,REAL:] by FUNCT_2:def 1; then A1: dom f = [:NAT,NAT:] by RELAT_1:91; rng f c= NAT proof let x; assume x in rng f; then consider y such that A2: y in dom f & x = f.y by FUNCT_1:def 5; reconsider n1 = y`1, n2 = y`2 as Nat by A1,A2,MCART_1:10; x = multreal.y by A2,FUNCT_1:70 .= multreal.[n1,n2] by A2,MCART_1:23 .= multreal.(n1,n2) by BINOP_1:def 1 .= n1*n2 by VECTSP_1:def 14; hence thesis; end; then reconsider f as BinOp of NAT by A1,FUNCT_2:def 1,RELSET_1:11; f <= op(<REAL,*>) by Def30,RELAT_1:88; then reconsider N = HGrStr(#NAT,f#) as strict (non empty SubStr of <REAL,*> ) by Def23; reconsider a = 1 as Element of N; A3: now let b be Element of N; reconsider n = b as Nat; thus a*b = 1*n by Th58 .= b; thus b*a = n*1 by Th58 .= b; end; then A4: N is unital by Th6; then A5: op(N) has_a_unity by Def10; now let b be Element of N; thus op(N).(a,b) = a*b by VECTSP_1:def 10 .= b by A3; thus op(N).(b,a) = b*a by VECTSP_1:def 10 .= b by A3; end; then A6: a is_a_unity_wrt op(N) by BINOP_1:11; then A7: the_unity_wrt op(N) = a by BINOP_1:def 8; now let a,b be Element of N such that A8: a*b = the_unity_wrt op(N); reconsider n = a, m = b as Nat; a*b = n*m by Th58; then a = 1 & b = 1 by A7,A8,NAT_1:40; hence a = b & b = the_unity_wrt op(N) by A6,BINOP_1:def 8; end; then N is uniquely-decomposable by A5,Th16; hence thesis by A4; end; uniqueness by Th28; 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 Th22; existence; end; :: corollary :: <NAT,*,1> is well-unital commutative associative uniquely-decomposable; definition func multnat -> BinOp of NAT equals:Def33: the mult of <NAT,*>; coherence proof carr(<NAT,*>) = NAT by Def31; hence thesis; end; end; theorem Th61: <NAT,*> = HGrStr(#NAT,multnat#) by Def31,Def33; theorem for n1,n2 being Nat, m1,m2 being Element of <NAT,*> st n1 = m1 & n2 = m2 holds m1*m2 = n1*n2 by Th58; theorem Th63: the_unity_wrt the mult of <NAT,*> = 1 proof carr(<NAT,*>) = NAT by Def31; hence thesis by Th32,Th55,RVSUM_1:14; end; theorem for n1,n2 being Nat, m1,m2 being Element of <NAT,*,1> st n1 = m1 & n2 = m2 holds m1*m2 = n1*n2 proof let n1,n2 be Nat, m1,m2 be Element of <NAT,*,1>; the HGrStr of <NAT,*,1> = <NAT,*> by Def22; then reconsider x1 = m1, x2 = m2 as Element of <NAT,*>; x1*x2 = m1*m2 by Th20; hence thesis by Th58; end; theorem <NAT,*,1> = multLoopStr(#NAT,multnat,1#) proof set N = <NAT,*,1>; the HGrStr of N = <NAT,*> & the_unity_wrt op(N) = un(N) by Def22,Th19; hence thesis by Def31,Def33,Th63; end; theorem multnat = multreal|([:NAT,NAT:] qua set) by Def30,Th26,Th61; theorem 1 is_a_unity_wrt multnat & multnat has_a_unity & the_unity_wrt multnat = 1 & multnat is commutative & multnat is associative & multnat is uniquely-decomposable proof multnat has_a_unity by Def10,Th61; then ex n being Nat st n is_a_unity_wrt multnat by SETWISEO:def 2; hence 1 is_a_unity_wrt multnat by Th61,Th63,BINOP_1:def 8; thus thesis by Def10,Def11,Def12,Def20,Th61,Th63; end; begin :: Monoid of finite sequences definition let D be non empty set; func D*+^ -> unital associative cancelable uniquely-decomposable constituted-FinSeqs strict (non empty HGrStr) 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 BinOpLambda; set G = HGrStr(#D*, f#); G is constituted-FinSeqs proof let x be Element of G; x is Element of D*; hence thesis; end; then reconsider G as constituted-FinSeqs strict (non empty HGrStr); A2: now let p,q be Element of G; reconsider p' = p, q' = q as Element of D* qua non empty set; thus p [*] q = f.(p',q') by VECTSP_1:def 10 .= p^q by A1; end; 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 ; A3: now let b be Element of N; thus a[*]b = a^b by A2 .= b by FINSEQ_1:47; thus b[*]a = b^a by A2 .= b by FINSEQ_1:47; end; hence N is unital by Th6; 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 A2 .= a^b^c by A2 .= a^(b^c) by FINSEQ_1:45 .= a^q by A2 .= a*(b*c) by A2; end; hence N is associative by Lm3; now let a,b,c be Element of N; a*b = a^b & a*c = a^c & b*a = b^a & c*a = c^a by A2; hence a*b = a*c or b*a = c*a implies b = c by FINSEQ_1:46; end; hence N is cancelable by Th15; N is unital by A3,Th6; hence op(N) has_a_unity by Def10; now let b be Element of N; a[*]b = f.(a,b) & b[*]a = f.(b,a) by VECTSP_1:def 10; hence f.(a,b) = b & f.(b,a) = b by A3; end; then A4: a is_a_unity_wrt op(N) by BINOP_1:11; then A5: the_unity_wrt op(N) = a by BINOP_1:def 8; let a',b be Element of N; assume f.(a',b) = the_unity_wrt op(N); then {} = a'[*]b by A5,VECTSP_1:def 10 .= a'^b by A2; then a = a' & a = b by FINSEQ_1:48; hence thesis by A4,BINOP_1:def 8; end; then reconsider G as unital associative cancelable uniquely-decomposable constituted-FinSeqs strict (non empty HGrStr); take G; thus thesis by A2; end; uniqueness proof let G1,G2 be unital associative cancelable uniquely-decomposable constituted-FinSeqs strict (non empty HGrStr) such that A6: carr(G1) = D* & for p,q being Element of G1 holds p [*] q = p^q and A7: carr(G2) = D* & 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* qua non empty set; reconsider p = a, q = b as Element of D*; reconsider a1 = a, b1 = b as Element of G1 by A6; reconsider a2 = a, b2 = b as Element of G2 by A7; f2.(a,b) = a2[*]b2 & a2[*]b2 = p^q & f1.(a,b) = a1[*]b1 & a1[*]b1 = p^q by A6,A7,VECTSP_1:def 10; hence f1.(a,b) = f2.(a,b); end; hence thesis by A6,A7,BINOP_1:2; end; end; definition let D; func D*+^+<0> -> well-unital strict (non empty MonoidalExtension of D*+^) means not contradiction; correctness by Th22; func D-concatenation -> BinOp of D* equals:Def36: the mult of D*+^; correctness proof carr(D*+^) = D* by Def34; hence thesis; end; end; theorem Th68: D*+^ = HGrStr(#D*, D-concatenation#) proof carr(D*+^) = D* by Def34; hence thesis by Def36; end; theorem Th69: the_unity_wrt the mult of D*+^ = {} proof set N = D*+^, f = op(N); A1: carr(N) = D* & for p,q being Element of D*+^ holds p[*]q = p^q by Def34; {} = <*>D; then reconsider a = {} as Element of N by A1,FINSEQ_1:def 11; now let b be Element of N; thus f.(a,b) = a[*]b by VECTSP_1:def 10 .= {}^b by Def34 .= b by FINSEQ_1:47; thus f.(b,a) = b[*]a by VECTSP_1:def 10 .= b^{} by Def34 .= b by FINSEQ_1:47; end; then a is_a_unity_wrt op(N) by BINOP_1:11; hence thesis by BINOP_1:def 8; end; theorem the carrier of D*+^+<0> = D* & the mult of D*+^+<0> = D-concatenation & the unity of D*+^+<0> = {} proof set M = D*+^+<0>; the HGrStr of M = D*+^ & the_unity_wrt op(M) = un(M) & the_unity_wrt the mult of D*+^ = {} by Def22,Th19,Th69; hence thesis by Def34,Def36; 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 HGrStr of D*+^+<0> = D*+^ by Def22; then reconsider p = a, q = b as Element of D*+^; thus a [*] b = p [*] q by Th20 .= a^b by Def34; end; theorem Th72: 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 Th25; then reconsider p' = p, q' = q as Element of D*+^ by TARSKI: def 3; thus p[*]q = p'[*]q' by Th27 .= p^q by Def34; end; theorem for F being unital (non empty SubStr of D*+^) holds the_unity_wrt the mult 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*+^; A1: op(F) has_a_unity by Def10; q^{} = p by FINSEQ_1:47 .= op(F).(p,p) by A1,SETWISEO:23 .= p[*]p by VECTSP_1:def 10 .= q^q by Th72; hence thesis by FINSEQ_1:46; end; theorem for F being non empty SubStr of D*+^ st {} is Element of F holds F is unital & the_unity_wrt the mult of F = {} proof let F be non empty SubStr of D*+^; the_unity_wrt op(D*+^) = {} by Th69; hence thesis by Th32; 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; assume A c= B; then A1: A* c= B* by LANG1:19; then A2: [:A*,A*:] c= [:B*,B*:] by ZFMISC_1:119; carr(A*+^) = A* & carr(B*+^) = B* by Def34; then A3: dom op(A*+^) = [:A*,A*:] & dom op(B*+^) = [:B*,B*:] by FUNCT_2:def 1; now let x; assume A4: x in [:A*,A*:]; then A5: 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 A1,A5,Def34; thus op(A*+^).x = op(A*+^).[x1,x2] by A4,MCART_1:23 .= op(A*+^).(x1,x2) by BINOP_1:def 1 .= x1[*]x2 by VECTSP_1:def 10 .= x1^x2 by Def34 .= y1[*]y2 by Def34 .= op(B*+^).(y1,y2) by VECTSP_1:def 10 .= op(B*+^).[x1,x2] by BINOP_1:def 1 .= op(B*+^).x by A4,MCART_1:23; end; hence op(A*+^) <= op(B*+^) by A2,A3,GRFUNC_1:8; end; theorem D-concatenation has_a_unity & the_unity_wrt (D-concatenation) = {} & D-concatenation is associative proof HGrStr(#D*,D-concatenation#) = D*+^ by Th68; hence thesis by Def10,Def12,Th69; end; begin :: Monoids of mappings definition let X be set; func GPFuncs X -> unital associative constituted-Functions strict (non empty HGrStr) means: Def37: the carrier of it = PFuncs(X,X) & for f,g being Element of it holds f [*] g = f(*)g; existence proof 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 = f(*)g; 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:120; dom(f*g) c= dom g & rng(f*g) c= rng f by RELAT_1:44,45; then dom(f*g) c= X & rng(f*g) c= X by XBOOLE_1:1; then f*g is Relation of X,X by RELSET_1:11; then reconsider c = f*g as Element of D by PARTFUN1:119; 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 BinOpEx(A1); set G = HGrStr(#D, f#); G is constituted-Functions proof let x be Element of G; thus thesis by PARTFUN1:120; end; then reconsider G as constituted-Functions strict non empty HGrStr; A3: now let a,b be Element of G; consider g,h being PartFunc of X,X such that A4: a = g & b = h & f.(a,b) = g(*)h by A2; thus a[*]b = a(*)b by A4,VECTSP_1:def 10; end; reconsider g = id X as PartFunc of X,X; reconsider f1 = g as Element of G by PARTFUN1:119; A5: now let h be Element of G; reconsider j = h as PartFunc of X,X by PARTFUN1:120; thus f1[*]h = g(*)j by A3 .= h by PARTFUN1:37; thus h[*]f1 = j(*)g by A3 .= h by PARTFUN1:36; end; now let f',g,h be Element of G; reconsider fg = f'[*]g, gh = g[*]h as Element of G; thus f'[*]g[*]h = fg(*)h by A3 .= f'(*)g(*)h by A3 .= f'(*)(g(*)h) by RELAT_1:55 .= f'(*)gh by A3 .= f'[*](g[*]h) by A3; end; then reconsider G as unital associative constituted-Functions strict (non empty HGrStr) by A5,Lm3,Th6; take G; thus carr(G) = PFuncs(X,X); let g,h be Element of G; reconsider g' = g, h' = h as Element of D; f.(g,h) = g [*] h & ex g,h being PartFunc of X,X st g' = g & h' = h & f.(g',h') = g(*)h by A2,VECTSP_1:def 10; hence thesis; end; uniqueness proof let G1,G2 be unital associative constituted-Functions strict (non empty HGrStr) such that A6: carr(G1) = PFuncs(X,X) & for f,g being Element of G1 holds f [*] g = f(*)g and A7: carr(G2) = PFuncs(X,X) & for f,g being Element of G2 holds f [*] g = f(*)g; set f1 = op(G1), f2 = op(G2); now let a,b be Element of G1; reconsider a' = a, b' = b as Element of G2 by A6,A7; f1.(a,b) = a[*]b & a[*]b = a(*)b & f2.(a',b') = a'[*]b' & a'[*]b' = a'(*)b' by A6,A7,VECTSP_1:def 10; hence f1.(a,b) = f2.(a,b); end; hence thesis by A6,A7,BINOP_1:2; 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 Th22; func X-composition -> BinOp of PFuncs(X,X) equals:Def39: the mult 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:119,120; end; theorem Th78: the_unity_wrt the mult of GPFuncs X = id X proof reconsider g = id X as PartFunc of X,X; A1: g in PFuncs(X,X) & carr(GPFuncs X) = PFuncs(X,X) by Def37,PARTFUN1:119; then reconsider f = g as Element of GPFuncs X; set op = op(GPFuncs X); now let h be Element of GPFuncs X; reconsider j = h as PartFunc of X,X by A1,PARTFUN1:120; thus op.(f,h) = f[*]h by VECTSP_1:def 10 .= g(*)j by Def37 .= h by PARTFUN1:37; thus op.(h,f) = h[*]f by VECTSP_1:def 10 .= j(*)g by Def37 .= h by PARTFUN1:36; end; then f is_a_unity_wrt op by BINOP_1:11; hence thesis by BINOP_1:def 8; end; theorem Th79: for F being non empty SubStr of GPFuncs X for f,g being Element of F holds f [*] g = f (*) g proof let F be non empty SubStr of GPFuncs X; let f,g be Element of F; carr(F) c= carr(GPFuncs X) by Th25; then reconsider f' = f, g' = g as Element of GPFuncs X by TARSKI:def 3; f[*]g = f'[*]g' by Th27; hence thesis by Def37; end; theorem Th80: for F being non empty SubStr of GPFuncs X st id X is Element of F holds F is unital & the_unity_wrt the mult of F = id X proof let F be non empty SubStr of GPFuncs X; the_unity_wrt op(GPFuncs X) = id X by Th78; hence thesis by Th32; end; theorem Y c= X implies GPFuncs Y is SubStr of GPFuncs X proof assume Y c= X; then A1: PFuncs(Y,Y) c= PFuncs(X,X) by PARTFUN1:128; then A2: [:PFuncs(Y,Y),PFuncs(Y,Y):] c= [:PFuncs(X,X),PFuncs(X,X):] by ZFMISC_1:119; carr(GPFuncs Y) = PFuncs(Y,Y) & carr(GPFuncs X) = PFuncs(X,X) by Def37; then A3: dom op(GPFuncs Y) = [:PFuncs(Y,Y),PFuncs(Y,Y):] & dom op(GPFuncs X) = [:PFuncs(X,X),PFuncs(X,X):] by FUNCT_2:def 1; now let x; assume A4: x in [:PFuncs(Y,Y),PFuncs(Y,Y):]; then A5: 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 A1,A5,Def37; thus op(GPFuncs Y).x = op(GPFuncs Y).[x1,x2] by A4,MCART_1:23 .= op(GPFuncs Y).(x1,x2) by BINOP_1:def 1 .= x1[*]x2 by VECTSP_1:def 10 .= x1(*)x2 by Def37 .= y1[*]y2 by Def37 .= op(GPFuncs X).(y1,y2) by VECTSP_1:def 10 .= op(GPFuncs X).[x1,x2] by BINOP_1:def 1 .= op(GPFuncs X).x by A4,MCART_1:23; end; hence op(GPFuncs Y) <= op(GPFuncs X) by A2,A3,GRFUNC_1:8; end; Lm8: x in Funcs(X,X) implies x is Function of X,X proof assume x in Funcs(X,X); then ex f being Function st x = f & dom f = X & rng f c= X by FUNCT_2:def 2 ; hence thesis by FUNCT_2:4; end; definition let X be set; func GFuncs X -> unital strict (non empty SubStr of GPFuncs X) means:Def40: the carrier of it = Funcs(X,X); existence proof consider f being Function of X,X; f in Funcs(X,X) & Funcs(X,X) c= PFuncs(X,X) & carr(GPFuncs X) = PFuncs(X,X) by Def37,FUNCT_2:12,141; then reconsider F = Funcs(X,X) as non empty Subset of GPFuncs X; 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 Lm8; x[*]y = f*g by Def37; hence thesis by FUNCT_2:12; end; consider G being strict non empty SubStr of GPFuncs X such that A2: the carrier of G = F from SubStrEx1(A1); id X in F by FUNCT_2:12; then reconsider G as unital strict (non empty SubStr of GPFuncs X) by A2, Th80; take G; thus thesis by A2; end; uniqueness by Th28; 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 Th22; 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 Lm8,FUNCT_2:12; end; theorem Th83: the mult of GFuncs X = (X-composition)|[:Funcs(X,X), Funcs(X,X):] proof op(GFuncs X) <= op(GPFuncs X) & X-composition = op(GPFuncs X) & dom op(GFuncs X) = [:carr(GFuncs X), carr(GFuncs X):] & carr(GFuncs X) = Funcs(X,X) by Def23,Def39,Def40,FUNCT_2:def 1; hence thesis by GRFUNC_1:64; end; theorem Th84: the_unity_wrt the mult of GFuncs X = id X proof id X in Funcs(X,X) & carr(GFuncs X) = Funcs(X,X) by Def40,FUNCT_2:12; hence thesis by Th80; end; theorem the carrier of MFuncs X = Funcs(X,X) & the mult of MFuncs X = (X-composition)|[:Funcs(X,X), Funcs(X,X):] & the unity of MFuncs X = id X proof the_unity_wrt op(GFuncs X) = id X & the HGrStr of MFuncs X = GFuncs X by Def22,Th84; hence thesis by Def40,Th19,Th83; end; definition let X be set; func GPerms X -> unital invertible 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: 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 = f*g by Th79; hence thesis; end; A2: ex x being Element of GFuncs X st P[x] proof consider f being Permutation of X; carr(GFuncs X) = Funcs(X,X) by Def40; then reconsider x = f as Element of GFuncs X by FUNCT_2: 12; take x; thus 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(A1,A2); A4: carr(GFuncs X) = Funcs(X,X) by Def40; then reconsider f = id X as Element of GFuncs X by FUNCT_2: 12; f in carr(G) by A3; then reconsider G as unital strict (non empty SubStr of GFuncs X) by Th80; now let a,b be Element of G; carr(G) c= carr(GFuncs X) by Th25; then reconsider a' = a, b' = b as Element of GFuncs X by TARSKI:def 3; reconsider i = f as Element of G by A3; reconsider f = a', g = b' as Permutation of X by A3; reconsider f' = f" as Element of GFuncs X by A4,FUNCT_2:12; reconsider f' as Element of G by A3; reconsider r = f'[*]b, l = b[*]f' as Element of G; take r,l; i = f(*)(f") & i = f"(*)f & g(*)i = g & i(*)g = g & a[*]f' = f(*)(f") & f'[*]a = f"(*)f & i[*]b = (id X)(*)g & b[*]i = g(*) id X by Th79,FUNCT_2:74,88; hence a[*]r = b & l[*]a = b by Lm3; end; then reconsider G as unital invertible strict (non empty SubStr of GFuncs X ) by Th12; take G; thus thesis by A3; end; uniqueness proof let G1,G2 be unital invertible strict (non empty SubStr of GFuncs X) such that A5: for f being Element of GFuncs X holds f in carr(G1) iff f is Permutation of X and A6: for f being Element of GFuncs X holds f in carr(G2) iff f is Permutation of X; A7: carr(G1) c= carr(GFuncs X) & carr(G2) c= carr(GFuncs X) by Th25; carr(G1) = carr(G2) proof thus carr(G1) c= carr(G2) proof let x; assume A8: x in carr(G1); then reconsider f = x as Element of GFuncs X by A7; f is Permutation of X by A5,A8; hence thesis by A6; end; let x; assume A9: x in carr(G2); then reconsider f = x as Element of GFuncs X by A7; f is Permutation of X by A6,A9; hence thesis by A5; end; hence thesis by Th28; end; end; :: corollary :: GPerms X is constituted-Functions Group; theorem Th86: x is Element of GPerms X iff x is Permutation of X proof carr(GPerms X) c= carr(GFuncs X) by Th25; then carr(GFuncs X) = Funcs(X,X) & (x is Permutation of X implies x in Funcs(X,X)) & (x is Element of GPerms X implies x is Element of GFuncs X) by Def40,FUNCT_2:12,TARSKI:def 3; hence thesis by Def42; end; theorem Th87: the_unity_wrt the mult of GPerms X = id X & 1.GPerms X = id X proof reconsider i = id X as Element of GPerms X by Th86; now let a be Element of GPerms X; reconsider f = a as Permutation of X by Th86; a[*]i = a(*)i & i[*]a = i(*)a by Th79; then op(GPerms X).(a,i) = f(*)i & op(GPerms X).(i,a) = i(*) f by VECTSP_1:def 10; hence op(GPerms X).(i,a) = a & op(GPerms X).(a,i) = a by FUNCT_2:74; end; then i is_a_unity_wrt op(GPerms X) by BINOP_1:11; hence the_unity_wrt op(GPerms X) = id X by BINOP_1:def 8; hence thesis by GROUP_1:33; 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 Th86; reconsider b = g" as Element of GPerms X by Th86; reconsider b as Element of GPerms X; g(*)(g") = id X & g"(*)g = id X & id X = 1.GPerms X & f[*]b = g(*)(g") & b[*]f = g"(*)g by Th79,Th87,FUNCT_2:88; hence thesis by GROUP_1:def 5; end;

Back to top