:: Monoids
:: by Grzegorz Bancerek
::
:: Copyright (c) 1992-2021 Association of Mizar Users

deffunc H1( 1-sorted ) -> set = the carrier of $1; deffunc H2( multMagma ) -> Element of bool [:[: the carrier of$1, the carrier of $1:], the carrier of$1:] = 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: :: MONOID_0:def 1 for a being Element of IT holds a is Function; attr IT is constituted-FinSeqs means :Def2: :: MONOID_0:def 2 for a being Element of IT holds a is FinSequence; end; :: deftheorem Def1 defines constituted-Functions MONOID_0:def 1 : for IT being 1-sorted holds ( IT is constituted-Functions iff for a being Element of IT holds a is Function ); :: deftheorem Def2 defines constituted-FinSeqs MONOID_0:def 2 : for IT being 1-sorted holds ( IT is constituted-FinSeqs iff for a being Element of IT holds a is FinSequence ); registration existence ex b1 being 1-sorted st b1 is constituted-Functions proof end; existence ex b1 being 1-sorted st b1 is constituted-FinSeqs proof end; end; registration let X be constituted-Functions 1-sorted ; cluster -> Relation-like Function-like for Element of the carrier of X; coherence for b1 being Element of X holds ( b1 is Function-like & b1 is Relation-like ) by Def1; end; registration coherence for b1 being 1-sorted st b1 is constituted-FinSeqs holds b1 is constituted-Functions ; end; registration let X be constituted-FinSeqs 1-sorted ; cluster -> FinSequence-like for Element of the carrier of X; coherence for b1 being Element of X holds b1 is FinSequence-like by Def2; end; definition let D be set ; let p, q be FinSequence of D; :: original: ^ redefine func p ^ q -> Element of D * ; coherence p ^ q is Element of D * proof 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 :: MONOID_0:def 3 for a, b being Element of D ex l being Element of D st IT . (l,a) = b; attr IT is right-invertible means :: MONOID_0:def 4 for a, b being Element of D ex r being Element of D st IT . (a,r) = b; attr IT is invertible means :: MONOID_0:def 5 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 :: MONOID_0:def 6 for a, b, c being Element of D st IT . (a,b) = IT . (a,c) holds b = c; attr IT is right-cancelable means :: MONOID_0:def 7 for a, b, c being Element of D st IT . (b,a) = IT . (c,a) holds b = c; attr IT is cancelable means :: MONOID_0:def 8 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 :: MONOID_0:def 9 ( 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; :: deftheorem defines left-invertible MONOID_0:def 3 : for D being non empty set for IT being BinOp of D holds ( IT is left-invertible iff for a, b being Element of D ex l being Element of D st IT . (l,a) = b ); :: deftheorem defines right-invertible MONOID_0:def 4 : for D being non empty set for IT being BinOp of D holds ( IT is right-invertible iff for a, b being Element of D ex r being Element of D st IT . (a,r) = b ); :: deftheorem defines invertible MONOID_0:def 5 : for D being non empty set for IT being BinOp of D holds ( IT is invertible iff for a, b being Element of D ex r, l being Element of D st ( IT . (a,r) = b & IT . (l,a) = b ) ); :: deftheorem defines left-cancelable MONOID_0:def 6 : for D being non empty set for IT being BinOp of D holds ( IT is left-cancelable iff for a, b, c being Element of D st IT . (a,b) = IT . (a,c) holds b = c ); :: deftheorem defines right-cancelable MONOID_0:def 7 : for D being non empty set for IT being BinOp of D holds ( IT is right-cancelable iff for a, b, c being Element of D st IT . (b,a) = IT . (c,a) holds b = c ); :: deftheorem defines cancelable MONOID_0:def 8 : for D being non empty set for IT being BinOp of D holds ( IT is cancelable iff 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 ); :: deftheorem defines uniquely-decomposable MONOID_0:def 9 : for D being non empty set for IT being BinOp of D holds ( IT is uniquely-decomposable iff ( 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 ) ) ) ); theorem Th1: :: MONOID_0:1 for D being non empty set for f being BinOp of D holds ( f is invertible iff ( f is left-invertible & f is right-invertible ) ) proof end; theorem :: MONOID_0:2 for D being non empty set for f being BinOp of D holds ( f is cancelable iff ( f is left-cancelable & f is right-cancelable ) ) ; theorem Th3: :: MONOID_0:3 for x being set 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 & f is cancelable & f is uniquely-decomposable ) proof end; definition let IT be non empty multMagma ; redefine attr IT is unital means :Def10: :: MONOID_0:def 10 the multF of IT is having_a_unity ; compatibility ( IT is unital iff the multF of IT is having_a_unity ) proof end; end; :: deftheorem Def10 defines unital MONOID_0:def 10 : for IT being non empty multMagma holds ( IT is unital iff the multF of IT is having_a_unity ); definition let G be non empty multMagma ; redefine attr G is commutative means :Def11: :: MONOID_0:def 11 the multF of G is commutative ; compatibility ( G is commutative iff the multF of G is commutative ) proof end; redefine attr G is associative means :Def12: :: MONOID_0:def 12 the multF of G is associative ; compatibility ( G is associative iff the multF of G is associative ) ; end; :: deftheorem Def11 defines commutative MONOID_0:def 11 : for G being non empty multMagma holds ( G is commutative iff the multF of G is commutative ); :: deftheorem Def12 defines associative MONOID_0:def 12 : for G being non empty multMagma holds ( G is associative iff the multF of G is associative ); definition let IT be non empty multMagma ; attr IT is idempotent means :: MONOID_0:def 13 the multF of IT is idempotent ; attr IT is left-invertible means :: MONOID_0:def 14 the multF of IT is left-invertible ; attr IT is right-invertible means :: MONOID_0:def 15 the multF of IT is right-invertible ; attr IT is invertible means :: MONOID_0:def 16 the multF of IT is invertible ; attr IT is left-cancelable means :: MONOID_0:def 17 the multF of IT is left-cancelable ; attr IT is right-cancelable means :: MONOID_0:def 18 the multF of IT is right-cancelable ; attr IT is cancelable means :: MONOID_0:def 19 the multF of IT is cancelable ; attr IT is uniquely-decomposable means :Def20: :: MONOID_0:def 20 the multF of IT is uniquely-decomposable ; end; :: deftheorem defines idempotent MONOID_0:def 13 : for IT being non empty multMagma holds ( IT is idempotent iff the multF of IT is idempotent ); :: deftheorem defines left-invertible MONOID_0:def 14 : for IT being non empty multMagma holds ( IT is left-invertible iff the multF of IT is left-invertible ); :: deftheorem defines right-invertible MONOID_0:def 15 : for IT being non empty multMagma holds ( IT is right-invertible iff the multF of IT is right-invertible ); :: deftheorem defines invertible MONOID_0:def 16 : for IT being non empty multMagma holds ( IT is invertible iff the multF of IT is invertible ); :: deftheorem defines left-cancelable MONOID_0:def 17 : for IT being non empty multMagma holds ( IT is left-cancelable iff the multF of IT is left-cancelable ); :: deftheorem defines right-cancelable MONOID_0:def 18 : for IT being non empty multMagma holds ( IT is right-cancelable iff the multF of IT is right-cancelable ); :: deftheorem defines cancelable MONOID_0:def 19 : for IT being non empty multMagma holds ( IT is cancelable iff the multF of IT is cancelable ); :: deftheorem Def20 defines uniquely-decomposable MONOID_0:def 20 : for IT being non empty multMagma holds ( IT is uniquely-decomposable iff the multF of IT is uniquely-decomposable ); registration existence ex b1 being non empty multMagma st ( b1 is unital & b1 is commutative & b1 is associative & b1 is cancelable & b1 is idempotent & b1 is invertible & b1 is uniquely-decomposable & b1 is constituted-Functions & b1 is constituted-FinSeqs & b1 is strict ) proof end; end; theorem Th4: :: MONOID_0:4 for G being non empty multMagma st G is unital holds the_unity_wrt the multF of G is_a_unity_wrt the multF of G proof end; theorem :: MONOID_0:5 for G being non empty multMagma holds ( G is unital iff for a being Element of G holds ( (the_unity_wrt the multF of G) * a = a & a * (the_unity_wrt the multF of G) = a ) ) proof end; theorem Th6: :: MONOID_0:6 for G being non empty multMagma holds ( G is unital iff ex a being Element of G st for b being Element of G holds ( a * b = b & b * a = b ) ) ; Lm1: for G being non empty multMagma holds ( G is associative iff for a, b, c being Element of G holds (a * b) * c = a * (b * c) ) ; theorem Th7: :: MONOID_0:7 for G being non empty multMagma holds ( G is idempotent iff for a being Element of G holds a * a = a ) proof end; theorem :: MONOID_0:8 for G being non empty multMagma holds ( G is left-invertible iff for a, b being Element of G ex l being Element of G st l * a = b ) proof end; theorem :: MONOID_0:9 for G being non empty multMagma holds ( G is right-invertible iff for a, b being Element of G ex r being Element of G st a * r = b ) proof end; theorem Th10: :: MONOID_0:10 for G being non empty multMagma holds ( G is invertible iff for a, b being Element of G ex r, l being Element of G st ( a * r = b & l * a = b ) ) proof end; theorem :: MONOID_0:11 for G being non empty multMagma holds ( G is left-cancelable iff for a, b, c being Element of G st a * b = a * c holds b = c ) proof end; theorem :: MONOID_0:12 for G being non empty multMagma holds ( G is right-cancelable iff for a, b, c being Element of G st b * a = c * a holds b = c ) proof end; theorem Th13: :: MONOID_0:13 for G being non empty multMagma holds ( G is cancelable iff for a, b, c being Element of G st ( a * b = a * c or b * a = c * a ) holds b = c ) proof end; theorem Th14: :: MONOID_0:14 for G being non empty multMagma holds ( 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 end; theorem Th15: :: MONOID_0:15 for G being non empty multMagma st G is associative holds ( G is invertible iff ( G is unital & the multF of G is having_an_inverseOp ) ) proof end; Lm2: for G being non empty multMagma holds ( G is invertible iff ( G is left-invertible & G is right-invertible ) ) by Th1; Lm3: for G being non empty multMagma holds ( G is cancelable iff ( G is left-cancelable & G is right-cancelable ) ) proof end; Lm4: for G being non empty multMagma st G is associative & G is invertible holds G is Group-like proof end; registration coherence for b1 being non empty multMagma st b1 is associative & b1 is Group-like holds b1 is invertible by Th15; coherence for b1 being non empty multMagma st b1 is associative & b1 is invertible holds b1 is Group-like by Lm4; end; registration coherence for b1 being non empty multMagma st b1 is invertible holds ( b1 is left-invertible & b1 is right-invertible ) by Lm2; coherence for b1 being non empty multMagma st b1 is left-invertible & b1 is right-invertible holds b1 is invertible by Lm2; coherence for b1 being non empty multMagma st b1 is cancelable holds ( b1 is left-cancelable & b1 is right-cancelable ) by Lm3; coherence for b1 being non empty multMagma st b1 is left-cancelable & b1 is right-cancelable holds b1 is cancelable by Lm3; coherence for b1 being non empty multMagma st b1 is associative & b1 is invertible holds ( b1 is unital & b1 is cancelable ) proof end; end; deffunc H3( multLoopStr ) -> Element of the carrier of$1 = 1. \$1;

definition
let IT be non empty multLoopStr ;
redefine attr IT is well-unital means :Def21: :: MONOID_0:def 21
1. IT is_a_unity_wrt the multF of IT;
compatibility
( IT is well-unital iff 1. IT is_a_unity_wrt the multF of IT )
proof end;
end;

:: deftheorem Def21 defines well-unital MONOID_0:def 21 :
for IT being non empty multLoopStr holds
( IT is well-unital iff 1. IT is_a_unity_wrt the multF of IT );

theorem Th16: :: MONOID_0:16
for M being non empty multLoopStr holds
( M is well-unital iff for a being Element of M holds
( (1. M) * a = a & a * (1. M) = a ) ) ;

theorem Th17: :: MONOID_0:17
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
existence
ex b1 being non empty multLoopStr st
( b1 is well-unital & b1 is commutative & b1 is associative & b1 is cancelable & b1 is idempotent & b1 is invertible & b1 is uniquely-decomposable & b1 is unital & b1 is constituted-Functions & b1 is constituted-FinSeqs & b1 is strict )
proof end;
end;

definition end;

definition
let G be multMagma ;
mode MonoidalExtension of G -> multLoopStr means :Def22: :: MONOID_0:def 22
multMagma(# the carrier of it, the multF of it #) = multMagma(# the carrier of G, the multF of G #);
existence
ex b1 being multLoopStr st multMagma(# the carrier of b1, the multF of b1 #) = multMagma(# the carrier of G, the multF of G #)
proof end;
end;

:: deftheorem Def22 defines MonoidalExtension MONOID_0:def 22 :
for G being multMagma
for b2 being multLoopStr holds
( b2 is MonoidalExtension of G iff multMagma(# the carrier of b2, the multF of b2 #) = multMagma(# the carrier of G, the multF of G #) );

registration
let G be non empty multMagma ;
cluster -> non empty for MonoidalExtension of G;
coherence
for b1 being MonoidalExtension of G holds not b1 is empty
proof end;
end;

theorem Th18: :: MONOID_0:18
for G being non empty multMagma
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
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9 ) )
proof end;

registration
let G be multMagma ;
existence
ex b1 being MonoidalExtension of G st b1 is strict
proof end;
end;

theorem Th19: :: MONOID_0:19
for G being non empty multMagma
for 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 end;

registration
let G be constituted-Functions multMagma ;
coherence
for b1 being MonoidalExtension of G holds b1 is constituted-Functions
proof end;
end;

registration
let G be constituted-FinSeqs multMagma ;
coherence
for b1 being MonoidalExtension of G holds b1 is constituted-FinSeqs
proof end;
end;

registration
let G be non empty unital multMagma ;
cluster -> unital for MonoidalExtension of G;
coherence
for b1 being MonoidalExtension of G holds b1 is unital
by Th19;
end;

registration
let G be non empty associative multMagma ;
cluster -> associative for MonoidalExtension of G;
coherence
for b1 being MonoidalExtension of G holds b1 is associative
by Th19;
end;

registration
let G be non empty commutative multMagma ;
cluster -> commutative for MonoidalExtension of G;
coherence
for b1 being MonoidalExtension of G holds b1 is commutative
by Th19;
end;

registration
let G be non empty invertible multMagma ;
cluster -> invertible for MonoidalExtension of G;
coherence
for b1 being MonoidalExtension of G holds b1 is invertible
by Th19;
end;

registration
let G be non empty cancelable multMagma ;
cluster -> cancelable for MonoidalExtension of G;
coherence
for b1 being MonoidalExtension of G holds b1 is cancelable
by Th19;
end;

registration
let G be non empty uniquely-decomposable multMagma ;
coherence
for b1 being MonoidalExtension of G holds b1 is uniquely-decomposable
by Th19;
end;

registration
let G be non empty unital multMagma ;
existence
ex b1 being MonoidalExtension of G st
( b1 is well-unital & b1 is strict )
proof end;
end;

theorem Th20: :: MONOID_0:20
for G being non empty unital multMagma
for M1, M2 being strict well-unital MonoidalExtension of G holds M1 = M2
proof end;

definition
let G be multMagma ;
mode SubStr of G -> multMagma means :Def23: :: MONOID_0:def 23
the multF of it c= the multF of G;
existence
ex b1 being multMagma st the multF of b1 c= the multF of G
;
end;

:: deftheorem Def23 defines SubStr MONOID_0:def 23 :
for G, b2 being multMagma holds
( b2 is SubStr of G iff the multF of b2 c= the multF of G );

registration
let G be multMagma ;
cluster strict for SubStr of G;
existence
ex b1 being SubStr of G st b1 is strict
proof end;
end;

registration
let G be non empty multMagma ;
cluster non empty strict for SubStr of G;
existence
ex b1 being SubStr of G st
( b1 is strict & not b1 is empty )
proof end;
end;

registration
let G be non empty unital multMagma ;
existence
ex b1 being non empty SubStr of G st
( b1 is unital & b1 is associative & b1 is commutative & b1 is cancelable & b1 is idempotent & b1 is invertible & b1 is uniquely-decomposable & b1 is strict )
proof end;
end;

definition
let G be multMagma ;
mode MonoidalSubStr of G -> multLoopStr means :Def24: :: MONOID_0:def 24
( the multF of it c= the multF of G & ( for M being multLoopStr st G = M holds
1. it = 1. M ) );
existence
ex b1 being multLoopStr st
( the multF of b1 c= the multF of G & ( for M being multLoopStr st G = M holds
1. b1 = 1. M ) )
proof end;
end;

:: deftheorem Def24 defines MonoidalSubStr MONOID_0:def 24 :
for G being multMagma
for b2 being multLoopStr holds
( b2 is MonoidalSubStr of G iff ( the multF of b2 c= the multF of G & ( for M being multLoopStr st G = M holds
1. b2 = 1. M ) ) );

registration
let G be multMagma ;
cluster strict for MonoidalSubStr of G;
existence
ex b1 being MonoidalSubStr of G st b1 is strict
proof end;
end;

registration
let G be non empty multMagma ;
cluster non empty strict for MonoidalSubStr of G;
existence
ex b1 being MonoidalSubStr of G st
( b1 is strict & not b1 is empty )
proof end;
end;

definition
let M be multLoopStr ;
redefine mode MonoidalSubStr of M means :Def25: :: MONOID_0:def 25
( the multF of it c= the multF of M & 1. it = 1. M );
compatibility
for b1 being multLoopStr holds
( b1 is MonoidalSubStr of M iff ( the multF of b1 c= the multF of M & 1. b1 = 1. M ) )
proof end;
end;

:: deftheorem Def25 defines MonoidalSubStr MONOID_0:def 25 :
for M, b2 being multLoopStr holds
( b2 is MonoidalSubStr of M iff ( the multF of b2 c= the multF of M & 1. b2 = 1. M ) );

registration
let G be non empty well-unital multLoopStr ;
existence
ex b1 being non empty MonoidalSubStr of G st
( b1 is well-unital & b1 is associative & b1 is commutative & b1 is cancelable & b1 is idempotent & b1 is invertible & b1 is uniquely-decomposable & b1 is strict )
proof end;
end;

theorem Th21: :: MONOID_0:21
for G being multMagma
for M being MonoidalSubStr of G holds M is SubStr of G
proof end;

definition
let G be multMagma ;
let M be MonoidalExtension of G;
:: original: SubStr
redefine mode SubStr of M -> SubStr of G;
coherence
for b1 being SubStr of M holds b1 is SubStr of G
proof end;
end;

definition
let G1 be multMagma ;
let G2 be SubStr of G1;
:: original: SubStr
redefine mode SubStr of G2 -> SubStr of G1;
coherence
for b1 being SubStr of G2 holds b1 is SubStr of G1
proof end;
end;

definition
let G1 be multMagma ;
let G2 be MonoidalSubStr of G1;
:: original: SubStr
redefine mode SubStr of G2 -> SubStr of G1;
coherence
for b1 being SubStr of G2 holds b1 is SubStr of G1
proof end;
end;

definition
let G be multMagma ;
let M be MonoidalSubStr of G;
:: original: MonoidalSubStr
redefine mode MonoidalSubStr of M -> MonoidalSubStr of G;
coherence
for b1 being MonoidalSubStr of M holds b1 is MonoidalSubStr of G
proof end;
end;

theorem :: MONOID_0:22
for G being non empty multMagma
for M being non empty multLoopStr holds
( G is SubStr of G & M is MonoidalSubStr of M )
proof end;

theorem Th23: :: MONOID_0:23
for G being non empty multMagma
for H being non empty SubStr of G
for N being non empty MonoidalSubStr of G holds
( the carrier of H c= the carrier of G & the carrier of N c= the carrier of G )
proof end;

theorem Th24: :: MONOID_0:24
for G being non empty multMagma
for H being non empty SubStr of G holds the multF of H = the multF of G || the carrier of H
proof end;

theorem Th25: :: MONOID_0:25
for G being non empty multMagma
for H being non empty SubStr of G
for a, b being Element of H
for a9, b9 being Element of G st a = a9 & b = b9 holds
a * b = a9 * b9
proof end;

theorem Th26: :: MONOID_0:26
for G being non empty multMagma
for H1, H2 being non empty SubStr of G st the carrier of H1 = the carrier of H2 holds
multMagma(# the carrier of H1, the multF of H1 #) = multMagma(# the carrier of H2, the multF of H2 #)
proof end;

theorem :: MONOID_0:27
for M being non empty multLoopStr
for H1, H2 being non empty MonoidalSubStr of M st the carrier of H1 = the carrier of H2 holds
multLoopStr(# the carrier of H1, the multF of H1, the OneF of H1 #) = multLoopStr(# the carrier of H2, the multF of H2, the OneF of H2 #)
proof end;

theorem Th28: :: MONOID_0:28
for G being non empty multMagma
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 end;

theorem :: MONOID_0:29
for M being non empty multLoopStr
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 end;

theorem Th30: :: MONOID_0:30
for G being non empty multMagma
for H being non empty SubStr of G st G is unital & the_unity_wrt the multF of G in the carrier of H holds
( H is unital & the_unity_wrt the multF of G = the_unity_wrt the multF of H )
proof end;

theorem Th31: :: MONOID_0:31
for M being non empty well-unital multLoopStr
for N being non empty MonoidalSubStr of M holds N is well-unital
proof end;

theorem Th32: :: MONOID_0:32
for G being non empty multMagma
for H being non empty SubStr of G st G is commutative holds
H is commutative
proof end;

theorem Th33: :: MONOID_0:33
for G being non empty multMagma
for H being non empty SubStr of G st G is associative holds
H is associative
proof end;

theorem Th34: :: MONOID_0:34
for G being non empty multMagma
for H being non empty SubStr of G st G is idempotent holds
H is idempotent
proof end;

theorem Th35: :: MONOID_0:35
for G being non empty multMagma
for H being non empty SubStr of G st G is cancelable holds
H is cancelable
proof end;

theorem Th36: :: MONOID_0:36
for G being non empty multMagma
for H being non empty SubStr of G st the_unity_wrt the multF of G in the carrier of H & G is uniquely-decomposable holds
H is uniquely-decomposable
proof end;

theorem Th37: :: MONOID_0:37
for M being non empty well-unital uniquely-decomposable multLoopStr
for N being non empty MonoidalSubStr of M holds N is uniquely-decomposable
proof end;

registration
let G be non empty constituted-Functions multMagma ;
cluster non empty -> non empty constituted-Functions for SubStr of G;
coherence
for b1 being non empty SubStr of G holds b1 is constituted-Functions
proof end;
cluster non empty -> non empty constituted-Functions for MonoidalSubStr of G;
coherence
for b1 being non empty MonoidalSubStr of G holds b1 is constituted-Functions
proof end;
end;

registration
let G be non empty constituted-FinSeqs multMagma ;
cluster non empty -> non empty constituted-FinSeqs for SubStr of G;
coherence
for b1 being non empty SubStr of G holds b1 is constituted-FinSeqs
proof end;
cluster non empty -> non empty constituted-FinSeqs for MonoidalSubStr of G;
coherence
for b1 being non empty MonoidalSubStr of G holds b1 is constituted-FinSeqs
proof end;
end;

registration
let M be non empty well-unital multLoopStr ;
cluster non empty -> non empty well-unital for MonoidalSubStr of M;
coherence
for b1 being non empty MonoidalSubStr of M holds b1 is well-unital
by Th31;
end;

registration
let G be non empty commutative multMagma ;
cluster non empty -> non empty commutative for SubStr of G;
coherence
for b1 being non empty SubStr of G holds b1 is commutative
by Th32;
cluster non empty -> non empty commutative for MonoidalSubStr of G;
coherence
for b1 being non empty MonoidalSubStr of G holds b1 is commutative
proof end;
end;

registration
let G be non empty associative multMagma ;
cluster non empty -> non empty associative for SubStr of G;
coherence
for b1 being non empty SubStr of G holds b1 is associative
by Th33;
cluster non empty -> non empty associative for MonoidalSubStr of G;
coherence
for b1 being non empty MonoidalSubStr of G holds b1 is associative
proof end;
end;

registration
let G be non empty idempotent multMagma ;
cluster non empty -> non empty idempotent for SubStr of G;
coherence
for b1 being non empty SubStr of G holds b1 is idempotent
by Th34;
cluster non empty -> non empty idempotent for MonoidalSubStr of G;
coherence
for b1 being non empty MonoidalSubStr of G holds b1 is idempotent
proof end;
end;

registration
let G be non empty cancelable multMagma ;
cluster non empty -> non empty cancelable for SubStr of G;
coherence
for b1 being non empty SubStr of G holds b1 is cancelable
by Th35;
cluster non empty -> non empty cancelable for MonoidalSubStr of G;
coherence
for b1 being non empty MonoidalSubStr of G holds b1 is cancelable
proof end;
end;

registration
let M be non empty well-unital uniquely-decomposable multLoopStr ;
cluster non empty -> non empty uniquely-decomposable for MonoidalSubStr of M;
coherence
for b1 being non empty MonoidalSubStr of M holds b1 is uniquely-decomposable
by Th37;
end;

Lm5: now :: thesis: for G being non empty multMagma
for D being non empty Subset of G st ( for x, y being Element of D holds x * y in D ) holds
ex H being non empty strict SubStr of G st the carrier of H = D
let G be non empty multMagma ; :: thesis: for D being non empty Subset of G st ( for x, y being Element of D holds x * y in D ) holds
ex H being non empty strict SubStr of G st the carrier of H = D

let D be non empty Subset of G; :: thesis: ( ( for x, y being Element of D holds x * y in D ) implies ex H being non empty strict SubStr of G st the carrier of H = D )
assume A1: for x, y being Element of D holds x * y in D ; :: thesis: ex H being non empty strict SubStr of G st the carrier of H = D
thus ex H being non empty strict SubStr of G st the carrier of H = D :: thesis: verum
proof
set op = the multF of G;
set carr = the carrier of G;
A2: dom the multF of G = [: the carrier of G, the carrier of G:] by FUNCT_2:def 1;
A3: rng ( the multF of G || D) c= D
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ( the multF of G || D) or x in D )
assume x in rng ( the multF of G || D) ; :: thesis: x in D
then consider y being object such that
A4: y in dom ( the multF of G || D) and
A5: x = ( the multF of G || D) . y by FUNCT_1:def 3;
reconsider y = y as Element of [:D,D:] by ;
reconsider y1 = y 1 , y2 = y 2 as Element of D ;
y = [y1,y2] by MCART_1:21;
then x = y1 * y2 by ;
hence x in D by A1; :: thesis: verum
end;
dom ( the multF of G || D) = [:D,D:] by ;
then reconsider f = the multF of G || D as BinOp of D by ;
f c= the multF of G by RELAT_1:59;
then reconsider H = multMagma(# D,f #) as non empty strict SubStr of G by Def23;
take H ; :: thesis: the carrier of H = D
thus the carrier of H = D ; :: thesis: verum
end;
end;

scheme :: MONOID_0:sch 1
SubStrEx2{ F1() -> non empty multMagma , P1[ object ] } :
ex H being non empty strict SubStr of F1() st
for x being Element of F1() holds
( x in the carrier of H iff P1[x] )
provided
A1: for x, y being Element of F1() st P1[x] & P1[y] holds
P1[x * y] and
A2: ex x being Element of F1() st P1[x]
proof end;

scheme :: MONOID_0:sch 2
MonoidalSubStrEx2{ F1() -> non empty multLoopStr , P1[ set ] } :
ex M being non empty strict MonoidalSubStr of F1() st
for x being Element of F1() holds
( x in the carrier of M iff P1[x] )
provided
A1: for x, y being Element of F1() st P1[x] & P1[y] holds
P1[x * y] and
A2: P1[ 1. F1()]
proof end;

notation
let G be multMagma ;
let a, b be Element of G;
synonym a [*] b for a * b;
end;

definition
func <REAL,+> -> non empty multMagma equals :: MONOID_0:def 26
coherence
multMagma(# REAL,addreal #) is non empty multMagma
;
end;

:: deftheorem defines <REAL,+> MONOID_0:def 26 :

registration
coherence by GROUP_1:46;
end;

theorem :: MONOID_0:38
for x being set holds
( x is Element of <REAL,+> iff x is Element of REAL ) ;

theorem Th39: :: MONOID_0:39
for N being non empty SubStr of <REAL,+>
for a, b being Element of N
for x, y being Real st a = x & b = y holds
a * b = x + y
proof end;

theorem Th40: :: MONOID_0:40
for N being non empty unital SubStr of <REAL,+> holds the_unity_wrt the multF of N = 0
proof end;

registration
let G be non empty unital multMagma ;
coherence
for b1 being non empty SubStr of G st b1 is associative & b1 is invertible holds
( b1 is unital & b1 is cancelable & b1 is Group-like )
;
end;

definition
:: original: INT.Group
redefine func INT.Group -> non empty strict SubStr of <REAL,+> ;
coherence
INT.Group is non empty strict SubStr of <REAL,+>
proof end;
end;

:: corollary
:: INT.Group is unital commutative associative cancelable invertible;
theorem :: MONOID_0:41
for G being non empty strict SubStr of <REAL,+> holds
( G = INT.Group iff the carrier of G = INT ) by ;

theorem :: MONOID_0:42
for x being set holds
( x is Element of INT.Group iff x is Integer ) by ;

definition
func <NAT,+> -> non empty strict unital uniquely-decomposable SubStr of INT.Group means :Def27: :: MONOID_0:def 27
the carrier of it = NAT ;
existence
ex b1 being non empty strict unital uniquely-decomposable SubStr of INT.Group st the carrier of b1 = NAT
proof end;
uniqueness
for b1, b2 being non empty strict unital uniquely-decomposable SubStr of INT.Group st the carrier of b1 = NAT & the carrier of b2 = NAT holds
b1 = b2
by Th26;
end;

:: deftheorem Def27 defines <NAT,+> MONOID_0:def 27 :
for b1 being non empty strict unital uniquely-decomposable SubStr of INT.Group holds
( b1 = <NAT,+> iff the carrier of b1 = NAT );

:: corollary
:: <NAT,+> is unital commutative associative cancelable uniquely-decomposable;
definition
existence
ex b1 being non empty strict well-unital MonoidalExtension of <NAT,+> st verum
;
uniqueness
for b1, b2 being non empty strict well-unital MonoidalExtension of <NAT,+> holds b1 = b2
by Th20;
end;

:: deftheorem defines <NAT,+,0> MONOID_0:def 28 :
for b1 being non empty strict well-unital MonoidalExtension of <NAT,+> holds
( b1 = <NAT,+,0> iff verum );

:: corollary
:: <NAT,+,0> is
:: well-unital commutative associative cancelable uniquely-decomposable;
definition
redefine func addnat equals :: MONOID_0:def 29
the multF of <NAT,+>;
compatibility
for b1 being Element of bool holds
( b1 = addnat iff b1 = the multF of <NAT,+> )
proof end;
end;

:: deftheorem defines addnat MONOID_0:def 29 :
addnat = the multF of <NAT,+>;

theorem Th43: :: MONOID_0:43
<NAT,+> = multMagma(# NAT,addnat #) by Def27;

theorem :: MONOID_0:44
for x being set holds
( x is Element of <NAT,+,0> iff x is Element of NAT )
proof end;

theorem :: MONOID_0:45
for n1, n2 being Element of NAT
for m1, m2 being Element of <NAT,+,0> st n1 = m1 & n2 = m2 holds
m1 * m2 = n1 + n2
proof end;

theorem :: MONOID_0:46
proof end;

theorem :: MONOID_0:47
proof end;

theorem :: MONOID_0:48
proof end;

definition
coherence by ;
end;

:: deftheorem defines <REAL,*> MONOID_0:def 30 :

theorem :: MONOID_0:49
for x being set holds
( x is Element of <REAL,*> iff x is Element of REAL ) ;

theorem Th50: :: MONOID_0:50
for N being non empty SubStr of <REAL,*>
for a, b being Element of N
for x, y being Real st a = x & b = y holds
a * b = x * y
proof end;

theorem :: MONOID_0:51
for N being non empty unital SubStr of <REAL,*> holds
( the_unity_wrt the multF of N = 0 or the_unity_wrt the multF of N = 1 )
proof end;

definition
func <NAT,*> -> non empty strict unital uniquely-decomposable SubStr of <REAL,*> means :Def31: :: MONOID_0:def 31
the carrier of it = NAT ;
existence
ex b1 being non empty strict unital uniquely-decomposable SubStr of <REAL,*> st the carrier of b1 = NAT
proof end;
uniqueness
for b1, b2 being non empty strict unital uniquely-decomposable SubStr of <REAL,*> st the carrier of b1 = NAT & the carrier of b2 = NAT holds
b1 = b2
by Th26;
end;

:: deftheorem Def31 defines <NAT,*> MONOID_0:def 31 :
for b1 being non empty strict unital uniquely-decomposable SubStr of <REAL,*> holds
( b1 = <NAT,*> iff the carrier of b1 = NAT );

:: corollary
:: <NAT,*> is unital commutative associative uniquely-decomposable;
definition
uniqueness
for b1, b2 being non empty strict well-unital MonoidalExtension of <NAT,*> holds b1 = b2
by Th20;
existence
ex b1 being non empty strict well-unital MonoidalExtension of <NAT,*> st verum
;
end;

:: deftheorem defines <NAT,*,1> MONOID_0:def 32 :
for b1 being non empty strict well-unital MonoidalExtension of <NAT,*> holds
( b1 = <NAT,*,1> iff verum );

:: corollary
:: <NAT,*,1> is well-unital commutative associative uniquely-decomposable;
definition
redefine func multnat equals :: MONOID_0:def 33
the multF of <NAT,*>;
compatibility
for b1 being Element of bool holds
( b1 = multnat iff b1 = the multF of <NAT,*> )
proof end;
end;

:: deftheorem defines multnat MONOID_0:def 33 :
multnat = the multF of <NAT,*>;

theorem Th52: :: MONOID_0:52
<NAT,*> = multMagma(# NAT,multnat #) by Def31;

theorem :: MONOID_0:53
for n1, n2 being Element of NAT
for m1, m2 being Element of <NAT,*> st n1 = m1 & n2 = m2 holds
m1 * m2 = n1 * n2 by Th50;

theorem Th54: :: MONOID_0:54
proof end;

theorem :: MONOID_0:55
for n1, n2 being Element of NAT
for m1, m2 being Element of <NAT,*,1> st n1 = m1 & n2 = m2 holds
m1 * m2 = n1 * n2
proof end;

theorem :: MONOID_0:56
<NAT,*,1> = multLoopStr(# NAT,multnat,1 #)
proof end;

theorem :: MONOID_0:57

theorem :: MONOID_0:58
proof end;

definition
let D be non empty set ;
func D *+^ -> non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma means :Def34: :: MONOID_0:def 34
( the carrier of it = D * & ( for p, q being Element of it holds p [*] q = p ^ q ) );
existence
ex b1 being non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma st
( the carrier of b1 = D * & ( for p, q being Element of b1 holds p [*] q = p ^ q ) )
proof end;
uniqueness
for b1, b2 being non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma st the carrier of b1 = D * & ( for p, q being Element of b1 holds p [*] q = p ^ q ) & the carrier of b2 = D * & ( for p, q being Element of b2 holds p [*] q = p ^ q ) holds
b1 = b2
proof end;
end;

:: deftheorem Def34 defines *+^ MONOID_0:def 34 :
for D being non empty set
for b2 being non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable multMagma holds
( b2 = D *+^ iff ( the carrier of b2 = D * & ( for p, q being Element of b2 holds p [*] q = p ^ q ) ) );

definition
let D be non empty set ;
func D *+^+<0> -> non empty strict well-unital MonoidalExtension of D *+^ means :: MONOID_0:def 35
verum;
correctness
existence
ex b1 being non empty strict well-unital MonoidalExtension of D *+^ st verum
;
uniqueness
for b1, b2 being non empty strict well-unital MonoidalExtension of D *+^ holds b1 = b2
;
by Th20;
func D -concatenation -> BinOp of (D *) equals :: MONOID_0:def 36
the multF of (D *+^);
correctness
coherence
the multF of (D *+^) is BinOp of (D *)
;
proof end;
end;

:: deftheorem defines *+^+<0> MONOID_0:def 35 :
for D being non empty set
for b2 being non empty strict well-unital MonoidalExtension of D *+^ holds
( b2 = D *+^+<0> iff verum );

:: deftheorem defines -concatenation MONOID_0:def 36 :
for D being non empty set holds D -concatenation = the multF of (D *+^);

theorem :: MONOID_0:59
for D being non empty set holds D *+^ = multMagma(# (D *),() #) by Def34;

theorem Th60: :: MONOID_0:60
for D being non empty set holds the_unity_wrt the multF of (D *+^) = {}
proof end;

theorem :: MONOID_0:61
for D being non empty set holds
( the carrier of () = D * & the multF of () = D -concatenation & 1. () = {} )
proof end;

theorem :: MONOID_0:62
for D being non empty set
for a, b being Element of () holds a [*] b = a ^ b
proof end;

theorem Th63: :: MONOID_0:63
for D being non empty set
for F being non empty SubStr of D *+^
for p, q being Element of F holds p [*] q = p ^ q
proof end;

theorem :: MONOID_0:64
for D being non empty set
for F being non empty unital SubStr of D *+^ holds the_unity_wrt the multF of F = {}
proof end;

theorem :: MONOID_0:65
for D being non empty set
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 end;

theorem :: MONOID_0:66
for A, B being non empty set st A c= B holds
A *+^ is SubStr of B *+^
proof end;

theorem :: MONOID_0:67
for D being non empty set holds
( D -concatenation is having_a_unity & the_unity_wrt () = {} & D -concatenation is associative )
proof end;

definition
let X be set ;
func GPFuncs X -> strict constituted-Functions multMagma means :Def37: :: MONOID_0:def 37
( the carrier of it = PFuncs (X,X) & ( for f, g being Element of it holds f [*] g = g (*) f ) );
existence
ex b1 being strict constituted-Functions multMagma st
( the carrier of b1 = PFuncs (X,X) & ( for f, g being Element of b1 holds f [*] g = g (*) f ) )
proof end;
uniqueness
for b1, b2 being strict constituted-Functions multMagma st the carrier of b1 = PFuncs (X,X) & ( for f, g being Element of b1 holds f [*] g = g (*) f ) & the carrier of b2 = PFuncs (X,X) & ( for f, g being Element of b2 holds f [*] g = g (*) f ) holds
b1 = b2
proof end;
end;

:: deftheorem Def37 defines GPFuncs MONOID_0:def 37 :
for X being set
for b2 being strict constituted-Functions multMagma holds
( b2 = GPFuncs X iff ( the carrier of b2 = PFuncs (X,X) & ( for f, g being Element of b2 holds f [*] g = g (*) f ) ) );

registration
let X be set ;
coherence
( GPFuncs X is unital & GPFuncs X is associative & not GPFuncs X is empty )
proof end;
end;

definition
let X be set ;
func MPFuncs X -> non empty strict well-unital MonoidalExtension of GPFuncs X means :: MONOID_0:def 38
verum;
existence
ex b1 being non empty strict well-unital MonoidalExtension of GPFuncs X st verum
;
uniqueness
for b1, b2 being non empty strict well-unital MonoidalExtension of GPFuncs X holds b1 = b2
by Th20;
func X -composition -> BinOp of (PFuncs (X,X)) equals :: MONOID_0:def 39
the multF of ();
correctness
coherence
the multF of () is BinOp of (PFuncs (X,X))
;
proof end;
end;

:: deftheorem defines MPFuncs MONOID_0:def 38 :
for X being set
for b2 being non empty strict well-unital MonoidalExtension of GPFuncs X holds
( b2 = MPFuncs X iff verum );

:: deftheorem defines -composition MONOID_0:def 39 :
for X being set holds X -composition = the multF of ();

:: corollary
:: MPFuncs X is constituted-Functions strict Monoid;
theorem :: MONOID_0:68
for x, X being set holds
( x is Element of () iff x is PartFunc of X,X )
proof end;

theorem Th69: :: MONOID_0:69
for X being set holds the_unity_wrt the multF of () = id X
proof end;

theorem Th70: :: MONOID_0:70
for X being set
for F being non empty SubStr of GPFuncs X
for f, g being Element of F holds f [*] g = g (*) f
proof end;

theorem Th71: :: MONOID_0:71
for X being set
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 end;

theorem :: MONOID_0:72
for X, Y being set st Y c= X holds
GPFuncs Y is SubStr of GPFuncs X
proof end;

definition
let X be set ;
func GFuncs X -> strict SubStr of GPFuncs X means :Def40: :: MONOID_0:def 40
the carrier of it = Funcs (X,X);
existence
ex b1 being strict SubStr of GPFuncs X st the carrier of b1 = Funcs (X,X)
proof end;
uniqueness
for b1, b2 being strict SubStr of GPFuncs X st the carrier of b1 = Funcs (X,X) & the carrier of b2 = Funcs (X,X) holds
b1 = b2
by Th26;
end;

:: deftheorem Def40 defines GFuncs MONOID_0:def 40 :
for X being set
for b2 being strict SubStr of GPFuncs X holds
( b2 = GFuncs X iff the carrier of b2 = Funcs (X,X) );

registration
let X be set ;
coherence
( GFuncs X is unital & not GFuncs X is empty )
proof end;
end;

:: corollary
:: GFuncs X is unital associative constituted-Functions;
definition
let X be set ;
func MFuncs X -> strict well-unital MonoidalExtension of GFuncs X means :: MONOID_0:def 41
verum;
correctness
existence
ex b1 being strict well-unital MonoidalExtension of GFuncs X st verum
;
uniqueness
for b1, b2 being strict well-unital MonoidalExtension of GFuncs X holds b1 = b2
;
by Th20;
end;

:: deftheorem defines MFuncs MONOID_0:def 41 :
for X being set
for b2 being strict well-unital MonoidalExtension of GFuncs X holds
( b2 = MFuncs X iff verum );

:: corollary
:: GFuncs X is constituted-Functions Monoid;
theorem :: MONOID_0:73
for x, X being set holds
( x is Element of () iff x is Function of X,X )
proof end;

theorem Th74: :: MONOID_0:74
for X being set holds the multF of () = () || (Funcs (X,X))
proof end;

theorem Th75: :: MONOID_0:75
for X being set holds the_unity_wrt the multF of () = id X
proof end;

theorem :: MONOID_0:76
for X being set holds
( the carrier of () = Funcs (X,X) & the multF of () = () || (Funcs (X,X)) & 1. () = id X )
proof end;

definition
let X be set ;
func GPerms X -> non empty strict SubStr of GFuncs X means :Def42: :: MONOID_0:def 42
for f being Element of () holds
( f in the carrier of it iff f is Permutation of X );
existence
ex b1 being non empty strict SubStr of GFuncs X st
for f being Element of () holds
( f in the carrier of b1 iff f is Permutation of X )
proof end;
uniqueness
for b1, b2 being non empty strict SubStr of GFuncs X st ( for f being Element of () holds
( f in the carrier of b1 iff f is Permutation of X ) ) & ( for f being Element of () holds
( f in the carrier of b2 iff f is Permutation of X ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def42 defines GPerms MONOID_0:def 42 :
for X being set
for b2 being non empty strict SubStr of GFuncs X holds
( b2 = GPerms X iff for f being Element of () holds
( f in the carrier of b2 iff f is Permutation of X ) );

registration
let X be set ;
coherence
( GPerms X is unital & GPerms X is invertible )
proof end;
end;

:: corollary
:: GPerms X is constituted-Functions Group;
theorem Th77: :: MONOID_0:77
for x, X being set holds
( x is Element of () iff x is Permutation of X )
proof end;

theorem Th78: :: MONOID_0:78
for X being set holds
( the_unity_wrt the multF of () = id X & 1_ () = id X )
proof end;

theorem :: MONOID_0:79
for X being set
for f being Element of () holds f " = f "
proof end;

:: 2005.05.13, A.T.
theorem :: MONOID_0:80
for S being 1-sorted st the carrier of S is functional holds
S is constituted-Functions ;

theorem :: MONOID_0:81
for G being non empty multMagma
for D being non empty Subset of G st ( for x, y being Element of D holds x * y in D ) holds
ex H being non empty strict SubStr of G st the carrier of H = D by Lm5;

theorem :: MONOID_0:82
for G being non empty multLoopStr
for D being non empty Subset of G st ( for x, y being Element of D holds x * y in D ) & 1. G in D holds
ex H being non empty strict MonoidalSubStr of G st the carrier of H = D
proof end;