:: MONOID_0 semantic presentation

deffunc H₁( 1-sorted ) -> set = the carrier of a₁;

deffunc H₂( HGrStr ) -> Relation of [:the carrier of a₁,the carrier of a₁:],the carrier of a₁ = the mult of a₁;

definition

let c₁ be 1-sorted ;
mode BinOp of a₁ is BinOp of the carrier of a₁;

end;

definition

let c₁ be 1-sorted ;
attr a₁ is constituted-Functions means :Def1: :: MONOID_0:def 1
for b₁ being Element of a₁ holds b₁ is Function;
attr a₁ is constituted-FinSeqs means :Def2: :: MONOID_0:def 2
for b₁ being Element of a₁ holds b₁ is FinSequence;

end;

:: deftheorem Def1 defines constituted-Functions MONOID_0:def 1 :

:: deftheorem Def2 defines constituted-FinSeqs MONOID_0:def 2 :

registration

cluster constituted-Functions 1-sorted ;
existence

proof end;

cluster constituted-FinSeqs 1-sorted ;
existence

proof end;

end;

registration

let c₁ be constituted-Functions 1-sorted ;
cluster -> Relation-like Function-like Element of the carrier of a₁;
coherence by Def1;

end;

registration

cluster constituted-FinSeqs -> constituted-Functions 1-sorted ;
coherence

proof end;

end;

registration

cluster constituted-FinSeqs -> constituted-Functions HGrStr ;
coherence

proof end;

end;

registration

let c₁ be constituted-FinSeqs 1-sorted ;
cluster -> Relation-like Function-like FinSequence-like Element of the carrier of a₁;
coherence by Def2;

end;

definition

let c₁ be set ;
let c₂, c₃ be FinSequence of c₁;
redefine func ^ as c₂ ^ c₃ -> Element of a₁ * ;
coherence

proof end;

end;

Lemma3: ( ( for b₁ being set
for b₂, b₃ being Function of b₁,b₁ holds b₂ * b₃ is Function of b₁,b₁ ) & ( for b₁ being set
for b₂, b₃ being Permutation of b₁ holds b₂ * b₃ is Permutation of b₁ ) & ( for b₁, b₂, b₃ being set
for b₄ being PartFunc of b₁,b₂
for b₅ being PartFunc of b₂,b₃ holds b₅ * b₄ is PartFunc of b₁,b₃ ) & ( for b₁ being set
for b₂, b₃ being non empty set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ holds b₅ * b₄ is Function of b₁,b₃ ) )
;

notation

let c₁, c₂ be Function;
synonym c₂ (*) c₁ for c₂ * c₁;

end;

definition

let c₁ be set ;
let c₂, c₃ be Function of c₁,c₁;
redefine func (*) as c₃ * c₂ -> Function of a₁,a₁;
coherence by Lemma3;

end;

definition

let c₁ be set ;
let c₂, c₃ be Permutation of c₁;
redefine func (*) as c₃ * c₂ -> Permutation of a₁;
coherence by Lemma3;

end;

definition

let c₁ be non empty set ;
let c₂ be BinOp of c₁;
attr a₂ is left-invertible means :: MONOID_0:def 3
for b₁, b₂ being Element of a₁ ex b₃ being Element of a₁ st a₂ . b₃,b₁ = b₂;
attr a₂ is right-invertible means :: MONOID_0:def 4
for b₁, b₂ being Element of a₁ ex b₃ being Element of a₁ st a₂ . b₁,b₃ = b₂;
attr a₂ is invertible means :Def5: :: MONOID_0:def 5
for b₁, b₂ being Element of a₁ ex b₃, b₄ being Element of a₁ st
( a₂ . b₁,b₃ = b₂ & a₂ . b₄,b₁ = b₂ );
attr a₂ is left-cancelable means :: MONOID_0:def 6
for b₁, b₂, b₃ being Element of a₁ st a₂ . b₁,b₂ = a₂ . b₁,b₃ holds
b₂ = b₃;
attr a₂ is right-cancelable means :: MONOID_0:def 7
for b₁, b₂, b₃ being Element of a₁ st a₂ . b₂,b₁ = a₂ . b₃,b₁ holds
b₂ = b₃;
attr a₂ is cancelable means :: MONOID_0:def 8
for b₁, b₂, b₃ being Element of a₁ st ( a₂ . b₁,b₂ = a₂ . b₁,b₃ or a₂ . b₂,b₁ = a₂ . b₃,b₁ ) holds
b₂ = b₃;
attr a₂ is uniquely-decomposable means :: MONOID_0:def 9
( a₂ has_a_unity & ( for b₁, b₂ being Element of a₁ st a₂ . b₁,b₂ = the_unity_wrt a₂ holds
( b₁ = b₂ & b₂ = the_unity_wrt a₂ ) ) );

end;

:: deftheorem Def3 defines left-invertible MONOID_0:def 3 :

:: deftheorem Def4 defines right-invertible MONOID_0:def 4 :

:: deftheorem Def5 defines invertible MONOID_0:def 5 :

:: deftheorem Def6 defines left-cancelable MONOID_0:def 6 :

:: deftheorem Def7 defines right-cancelable MONOID_0:def 7 :

:: deftheorem Def8 defines cancelable MONOID_0:def 8 :

:: deftheorem Def9 defines uniquely-decomposable MONOID_0:def 9 :

theorem Th1: :: MONOID_0:1

for b₁ being non empty set
for b₂ being BinOp of b₁ holds
( b₂ is invertible iff ( b₂ is left-invertible & b₂ is right-invertible ) )

proof end;

theorem Th2: :: MONOID_0:2

for b₁ being non empty set
for b₂ being BinOp of b₁ holds
( b₂ is cancelable iff ( b₂ is left-cancelable & b₂ is right-cancelable ) )

proof end;

theorem Th3: :: MONOID_0:3

for b₁ being set
for b₂ being BinOp of {b₁} holds
( b₂ = {[b₁,b₁]} --> b₁ & b₂ has_a_unity & b₂ is commutative & b₂ is associative & b₂ is idempotent & b₂ is invertible & b₂ is cancelable & b₂ is uniquely-decomposable )

proof end;

definition

let c₁ be non empty HGrStr ;
redefine attr a₁ is unital means :Def10: :: MONOID_0:def 10
the mult of a₁ has_a_unity ;
compatibility

proof end;

end;

:: deftheorem Def10 defines unital MONOID_0:def 10 :

definition

let c₁ be non empty HGrStr ;
redefine attr a₁ is commutative means :: MONOID_0:def 11
the mult of a₁ is commutative;
compatibility

proof end;

redefine attr a₁ is associative means :Def12: :: MONOID_0:def 12
the mult of a₁ is associative;
compatibility

proof end;

end;

:: deftheorem Def11 defines commutative MONOID_0:def 11 :

:: deftheorem Def12 defines associative MONOID_0:def 12 :

definition

let c₁ be non empty HGrStr ;
attr a₁ is idempotent means :: MONOID_0:def 13
the mult of a₁ is idempotent;
attr a₁ is left-invertible means :: MONOID_0:def 14
the mult of a₁ is left-invertible;
attr a₁ is right-invertible means :: MONOID_0:def 15
the mult of a₁ is right-invertible;
attr a₁ is invertible means :Def16: :: MONOID_0:def 16
the mult of a₁ is invertible;
attr a₁ is left-cancelable means :: MONOID_0:def 17
the mult of a₁ is left-cancelable;
attr a₁ is right-cancelable means :: MONOID_0:def 18
the mult of a₁ is right-cancelable;
attr a₁ is cancelable means :: MONOID_0:def 19
the mult of a₁ is cancelable;
attr a₁ is uniquely-decomposable means :Def20: :: MONOID_0:def 20
the mult of a₁ is uniquely-decomposable;

end;

:: deftheorem Def13 defines idempotent MONOID_0:def 13 :

:: deftheorem Def14 defines left-invertible MONOID_0:def 14 :

:: deftheorem Def15 defines right-invertible MONOID_0:def 15 :

:: deftheorem Def16 defines invertible MONOID_0:def 16 :

:: deftheorem Def17 defines left-cancelable MONOID_0:def 17 :

:: deftheorem Def18 defines right-cancelable MONOID_0:def 18 :

:: deftheorem Def19 defines cancelable MONOID_0:def 19 :

:: deftheorem Def20 defines uniquely-decomposable MONOID_0:def 20 :

registration

cluster non empty strict unital associative commutative constituted-Functions constituted-FinSeqs idempotent invertible cancelable uniquely-decomposable HGrStr ;
existence

proof end;

end;

theorem Th4: :: MONOID_0:4

for b₁ being non empty HGrStr st b₁ is unital holds
the_unity_wrt the mult of b₁ is_a_unity_wrt the mult of b₁

proof end;

theorem Th5: :: MONOID_0:5

for b₁ being non empty HGrStr holds
( b₁ is unital iff for b₂ being Element of b₁ holds
( (the_unity_wrt the mult of b₁) * b₂ = b₂ & b₂ * (the_unity_wrt the mult of b₁) = b₂ ) )

proof end;

theorem Th6: :: MONOID_0:6

for b₁ being non empty HGrStr holds
( b₁ is unital iff ex b₂ being Element of b₁ st
for b₃ being Element of b₁ holds
( b₂ * b₃ = b₃ & b₃ * b₂ = b₃ ) )

proof end;

Lemma14: for b₁ being non empty HGrStr holds
( b₁ is commutative iff for b₂, b₃ being Element of b₁ holds b₂ * b₃ = b₃ * b₂ )

proof end;

Lemma15: for b₁ being non empty HGrStr holds
( b₁ is associative iff for b₂, b₃, b₄ being Element of b₁ holds (b₂ * b₃) * b₄ = b₂ * (b₃ * b₄) )

proof end;

theorem Th7: :: MONOID_0:7

canceled;

theorem Th8: :: MONOID_0:8

canceled;

theorem Th9: :: MONOID_0:9

for b₁ being non empty HGrStr holds
( b₁ is idempotent iff for b₂ being Element of b₁ holds b₂ * b₂ = b₂ )

proof end;

theorem Th10: :: MONOID_0:10

for b₁ being non empty HGrStr holds
( b₁ is left-invertible iff for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st b₄ * b₂ = b₃ )

proof end;

theorem Th11: :: MONOID_0:11

for b₁ being non empty HGrStr holds
( b₁ is right-invertible iff for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st b₂ * b₄ = b₃ )

proof end;

theorem Th12: :: MONOID_0:12

for b₁ being non empty HGrStr holds
( b₁ is invertible iff for b₂, b₃ being Element of b₁ ex b₄, b₅ being Element of b₁ st
( b₂ * b₄ = b₃ & b₅ * b₂ = b₃ ) )

proof end;

theorem Th13: :: MONOID_0:13

for b₁ being non empty HGrStr holds
( b₁ is left-cancelable iff for b₂, b₃, b₄ being Element of b₁ st b₂ * b₃ = b₂ * b₄ holds
b₃ = b₄ )

proof end;

theorem Th14: :: MONOID_0:14

for b₁ being non empty HGrStr holds
( b₁ is right-cancelable iff for b₂, b₃, b₄ being Element of b₁ st b₃ * b₂ = b₄ * b₂ holds
b₃ = b₄ )

proof end;

theorem Th15: :: MONOID_0:15

for b₁ being non empty HGrStr holds
( b₁ is cancelable iff for b₂, b₃, b₄ being Element of b₁ st ( b₂ * b₃ = b₂ * b₄ or b₃ * b₂ = b₄ * b₂ ) holds
b₃ = b₄ )

proof end;

theorem Th16: :: MONOID_0:16

for b₁ being non empty HGrStr holds
( b₁ is uniquely-decomposable iff ( the mult of b₁ has_a_unity & ( for b₂, b₃ being Element of b₁ st b₂ * b₃ = the_unity_wrt the mult of b₁ holds
( b₂ = b₃ & b₃ = the_unity_wrt the mult of b₁ ) ) ) )

proof end;

theorem Th17: :: MONOID_0:17

for b₁ being non empty HGrStr st b₁ is associative holds
( b₁ is invertible iff ( b₁ is unital & the mult of b₁ has_an_inverseOp ) )

proof end;

Lemma21: for b₁ being non empty HGrStr holds
( b₁ is invertible iff ( b₁ is left-invertible & b₁ is right-invertible ) )

proof end;

Lemma22: for b₁ being non empty HGrStr holds
( b₁ is cancelable iff ( b₁ is left-cancelable & b₁ is right-cancelable ) )

proof end;

Lemma23: for b₁ being non empty HGrStr st b₁ is associative & b₁ is invertible holds
b₁ is Group-like

proof end;

registration

cluster non empty Group-like associative -> non empty invertible HGrStr ;
coherence

proof end;

cluster non empty associative invertible -> non empty Group-like HGrStr ;
coherence by Lemma23;

end;

registration

cluster non empty invertible -> non empty left-invertible right-invertible HGrStr ;
coherence by Lemma21;
cluster non empty left-invertible right-invertible -> non empty invertible HGrStr ;
coherence by Lemma21;
cluster non empty cancelable -> non empty left-cancelable right-cancelable HGrStr ;
coherence by Lemma22;
cluster non empty left-cancelable right-cancelable -> non empty cancelable HGrStr ;
coherence by Lemma22;
cluster non empty associative invertible -> non empty unital cancelable HGrStr ;
coherence

proof end;

end;

deffunc H₃( multLoopStr ) -> Element of the carrier of a₁ = the unity of a₁;

definition

let c₁ be non empty multLoopStr ;
redefine attr a₁ is well-unital means :Def21: :: MONOID_0:def 21
the unity of a₁ is_a_unity_wrt the mult of a₁;
compatibility

proof end;

end;

:: deftheorem Def21 defines well-unital MONOID_0:def 21 :

theorem Th18: :: MONOID_0:18

for b₁ being non empty multLoopStr holds
( b₁ is well-unital iff for b₂ being Element of b₁ holds
( the unity of b₁ * b₂ = b₂ & b₂ * the unity of b₁ = b₂ ) )

proof end;

Lemma26: for b₁ being non empty multLoopStr st b₁ is well-unital holds
b₁ is unital

proof end;

registration

cluster non empty well-unital -> non empty unital multLoopStr ;
coherence by Lemma26;

end;

theorem Th19: :: MONOID_0:19

for b₁ being non empty multLoopStr st b₁ is well-unital holds
the unity of b₁ = the_unity_wrt the mult of b₁

proof end;

registration

let c₁ be non empty set ;
let c₂ be BinOp of c₁;
let c₃ be Element of c₁;
cluster multLoopStr(# a₁,a₂,a₃ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

registration

cluster non empty unital Group-like associative commutative strict well-unital constituted-Functions constituted-FinSeqs idempotent left-invertible right-invertible invertible left-cancelable right-cancelable cancelable uniquely-decomposable multLoopStr ;
existence

proof end;

end;

definition

mode Monoid is non empty associative well-unital multLoopStr ;

end;

definition

let c₁ be HGrStr ;
mode MonoidalExtension of c₁ -> multLoopStr means :Def22: :: MONOID_0:def 22
HGrStr(# the carrier of a₂,the mult of a₂ #) = HGrStr(# the carrier of a₁,the mult of a₁ #);
existence

proof end;

end;

:: deftheorem Def22 defines MonoidalExtension MONOID_0:def 22 :

registration

let c₁ be non empty HGrStr ;
cluster -> non empty MonoidalExtension of a₁;
coherence

proof end;

end;

theorem Th20: :: MONOID_0:20

for b₁ being non empty HGrStr
for b₂ being MonoidalExtension of b₁ holds
( the carrier of b₂ = the carrier of b₁ & the mult of b₂ = the mult of b₁ & ( for b₃, b₄ being Element of b₂
for b₅, b₆ being Element of b₁ st b₃ = b₅ & b₄ = b₆ holds
b₃ * b₄ = b₅ * b₆ ) )

proof end;

registration

let c₁ be HGrStr ;
cluster strict MonoidalExtension of a₁;
existence

proof end;

end;

theorem Th21: :: MONOID_0:21

for b₁ being non empty HGrStr
for b₂ being MonoidalExtension of b₁ holds
( ( b₁ is unital implies b₂ is unital ) & ( b₁ is commutative implies b₂ is commutative ) & ( b₁ is associative implies b₂ is associative ) & ( b₁ is invertible implies b₂ is invertible ) & ( b₁ is uniquely-decomposable implies b₂ is uniquely-decomposable ) & ( b₁ is cancelable implies b₂ is cancelable ) )

proof end;

registration

let c₁ be constituted-Functions HGrStr ;
cluster -> constituted-Functions MonoidalExtension of a₁;
coherence

proof end;

end;

registration

let c₁ be constituted-FinSeqs HGrStr ;
cluster -> constituted-Functions constituted-FinSeqs MonoidalExtension of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty unital HGrStr ;
cluster -> non empty unital MonoidalExtension of a₁;
coherence by Th21;

end;

registration

let c₁ be non empty associative HGrStr ;
cluster -> non empty associative MonoidalExtension of a₁;
coherence by Th21;

end;

registration

let c₁ be non empty commutative HGrStr ;
cluster -> non empty commutative MonoidalExtension of a₁;
coherence by Th21;

end;

registration

let c₁ be non empty invertible HGrStr ;
cluster -> non empty left-invertible right-invertible invertible MonoidalExtension of a₁;
coherence by Th21;

end;

registration

let c₁ be non empty cancelable HGrStr ;
cluster -> non empty left-cancelable right-cancelable cancelable MonoidalExtension of a₁;
coherence by Th21;

end;

registration

let c₁ be non empty uniquely-decomposable HGrStr ;
cluster -> non empty uniquely-decomposable MonoidalExtension of a₁;
coherence by Th21;

end;

registration

let c₁ be non empty unital HGrStr ;
cluster non empty unital strict well-unital MonoidalExtension of a₁;
existence

proof end;

end;

theorem Th22: :: MONOID_0:22

for b₁ being non empty unital HGrStr
for b₂, b₃ being strict well-unital MonoidalExtension of b₁ holds b₂ = b₃

proof end;

definition

let c₁ be HGrStr ;
mode SubStr of c₁ -> HGrStr means :Def23: :: MONOID_0:def 23
the mult of a₂ <= the mult of a₁;
existence ;

end;

:: deftheorem Def23 defines SubStr MONOID_0:def 23 :

registration

let c₁ be HGrStr ;
cluster strict SubStr of a₁;
existence

proof end;

end;

registration

let c₁ be non empty HGrStr ;
cluster non empty strict SubStr of a₁;
existence

proof end;

end;

registration

let c₁ be non empty unital HGrStr ;
cluster non empty strict unital Group-like associative commutative idempotent left-invertible right-invertible invertible left-cancelable right-cancelable cancelable uniquely-decomposable SubStr of a₁;
existence

proof end;

end;

definition

let c₁ be HGrStr ;
mode MonoidalSubStr of c₁ -> multLoopStr means :Def24: :: MONOID_0:def 24
( the mult of a₂ <= the mult of a₁ & ( for b₁ being multLoopStr st a₁ = b₁ holds
the unity of a₂ = the unity of b₁ ) );
existence

proof end;

end;

:: deftheorem Def24 defines MonoidalSubStr MONOID_0:def 24 :

registration

let c₁ be HGrStr ;
cluster strict MonoidalSubStr of a₁;
existence

proof end;

end;

registration

let c₁ be non empty HGrStr ;
cluster non empty strict MonoidalSubStr of a₁;
existence

proof end;

end;

definition

let c₁ be multLoopStr ;
redefine mode MonoidalSubStr of c₁ -> multLoopStr means :Def25: :: MONOID_0:def 25
( the mult of a₂ <= the mult of a₁ & the unity of a₂ = the unity of a₁ );
compatibility

proof end;

end;

:: deftheorem Def25 defines MonoidalSubStr MONOID_0:def 25 :

registration

let c₁ be non empty well-unital multLoopStr ;
cluster non empty unital Group-like associative commutative strict well-unital idempotent left-invertible right-invertible invertible left-cancelable right-cancelable cancelable uniquely-decomposable MonoidalSubStr of a₁;
existence

proof end;

end;

theorem Th23: :: MONOID_0:23

for b₁ being HGrStr
for b₂ being MonoidalSubStr of b₁ holds b₂ is SubStr of b₁

proof end;

definition

let c₁ be HGrStr ;
let c₂ be MonoidalExtension of c₁;
redefine mode SubStr as SubStr of c₂ -> SubStr of a₁;
coherence

proof end;

end;

definition

let c₁ be HGrStr ;
let c₂ be SubStr of c₁;
redefine mode SubStr as SubStr of c₂ -> SubStr of a₁;
coherence

proof end;

end;

definition

let c₁ be HGrStr ;
let c₂ be MonoidalSubStr of c₁;
redefine mode SubStr as SubStr of c₂ -> SubStr of a₁;
coherence

proof end;

end;

definition

let c₁ be HGrStr ;
let c₂ be MonoidalSubStr of c₁;
redefine mode MonoidalSubStr as MonoidalSubStr of c₂ -> MonoidalSubStr of a₁;
coherence

proof end;

end;

theorem Th24: :: MONOID_0:24

for b₁ being non empty HGrStr
for b₂ being non empty multLoopStr holds
( b₁ is SubStr of b₁ & b₂ is MonoidalSubStr of b₂ )

proof end;

theorem Th25: :: MONOID_0:25

for b₁ being non empty HGrStr
for b₂ being non empty SubStr of b₁
for b₃ being non empty MonoidalSubStr of b₁ holds
( the carrier of b₂ c= the carrier of b₁ & the carrier of b₃ c= the carrier of b₁ )

proof end;

theorem Th26: :: MONOID_0:26

for b₁ being non empty HGrStr
for b₂ being non empty SubStr of b₁ holds the mult of b₂ = the mult of b₁ || the carrier of b₂

proof end;

theorem Th27: :: MONOID_0:27

for b₁ being non empty HGrStr
for b₂ being non empty SubStr of b₁
for b₃, b₄ being Element of b₂
for b₅, b₆ being Element of b₁ st b₃ = b₅ & b₄ = b₆ holds
b₃ * b₄ = b₅ * b₆

proof end;

theorem Th28: :: MONOID_0:28

for b₁ being non empty HGrStr
for b₂, b₃ being non empty SubStr of b₁ st the carrier of b₂ = the carrier of b₃ holds
HGrStr(# the carrier of b₂,the mult of b₂ #) = HGrStr(# the carrier of b₃,the mult of b₃ #)

proof end;

theorem Th29: :: MONOID_0:29

for b₁ being non empty multLoopStr
for b₂, b₃ being non empty MonoidalSubStr of b₁ st the carrier of b₂ = the carrier of b₃ holds
multLoopStr(# the carrier of b₂,the mult of b₂,the unity of b₂ #) = multLoopStr(# the carrier of b₃,the mult of b₃,the unity of b₃ #)

proof end;

theorem Th30: :: MONOID_0:30

for b₁ being non empty HGrStr
for b₂, b₃ being non empty SubStr of b₁ st the carrier of b₂ c= the carrier of b₃ holds
b₂ is SubStr of b₃

proof end;

theorem Th31: :: MONOID_0:31

for b₁ being non empty multLoopStr
for b₂, b₃ being non empty MonoidalSubStr of b₁ st the carrier of b₂ c= the carrier of b₃ holds
b₂ is MonoidalSubStr of b₃

proof end;

theorem Th32: :: MONOID_0:32

for b₁ being non empty HGrStr
for b₂ being non empty SubStr of b₁ st b₁ is unital & the_unity_wrt the mult of b₁ in the carrier of b₂ holds
( b₂ is unital & the_unity_wrt the mult of b₁ = the_unity_wrt the mult of b₂ )

proof end;

theorem Th33: :: MONOID_0:33

for b₁ being non empty well-unital multLoopStr
for b₂ being non empty MonoidalSubStr of b₁ holds b₂ is well-unital

proof end;

theorem Th34: :: MONOID_0:34

for b₁ being non empty HGrStr
for b₂ being non empty SubStr of b₁ st b₁ is commutative holds
b₂ is commutative

proof end;

theorem Th35: :: MONOID_0:35

for b₁ being non empty HGrStr
for b₂ being non empty SubStr of b₁ st b₁ is associative holds
b₂ is associative

proof end;

theorem Th36: :: MONOID_0:36

for b₁ being non empty HGrStr
for b₂ being non empty SubStr of b₁ st b₁ is idempotent holds
b₂ is idempotent

proof end;

theorem Th37: :: MONOID_0:37

for b₁ being non empty HGrStr
for b₂ being non empty SubStr of b₁ st b₁ is cancelable holds
b₂ is cancelable

proof end;

theorem Th38: :: MONOID_0:38

for b₁ being non empty HGrStr
for b₂ being non empty SubStr of b₁ st the_unity_wrt the mult of b₁ in the carrier of b₂ & b₁ is uniquely-decomposable holds
b₂ is uniquely-decomposable

proof end;

theorem Th39: :: MONOID_0:39

for b₁ being non empty well-unital uniquely-decomposable multLoopStr
for b₂ being non empty MonoidalSubStr of b₁ holds b₂ is uniquely-decomposable

proof end;

registration

let c₁ be non empty constituted-Functions HGrStr ;
cluster non empty -> non empty constituted-Functions SubStr of a₁;
coherence

proof end;

cluster non empty -> non empty constituted-Functions MonoidalSubStr of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty constituted-FinSeqs HGrStr ;
cluster non empty -> non empty constituted-Functions constituted-FinSeqs SubStr of a₁;
coherence

proof end;

cluster non empty -> non empty constituted-Functions constituted-FinSeqs MonoidalSubStr of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty well-unital multLoopStr ;
cluster non empty -> non empty unital well-unital MonoidalSubStr of a₁;
coherence by Th33;

end;

registration

let c₁ be non empty commutative HGrStr ;
cluster non empty -> non empty commutative SubStr of a₁;
coherence by Th34;
cluster non empty -> non empty commutative MonoidalSubStr of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty associative HGrStr ;
cluster non empty -> non empty associative SubStr of a₁;
coherence by Th35;
cluster non empty -> non empty associative MonoidalSubStr of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty idempotent HGrStr ;
cluster non empty -> non empty idempotent SubStr of a₁;
coherence by Th36;
cluster non empty -> non empty idempotent MonoidalSubStr of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty cancelable HGrStr ;
cluster non empty -> non empty left-cancelable right-cancelable cancelable SubStr of a₁;
coherence by Th37;
cluster non empty -> non empty left-cancelable right-cancelable cancelable MonoidalSubStr of a₁;
coherence

proof end;

end;

registration

let c₁ be non empty well-unital uniquely-decomposable multLoopStr ;
cluster non empty -> non empty unital well-unital uniquely-decomposable MonoidalSubStr of a₁;
coherence by Th39;

end;

scheme :: MONOID_0:sch 1
s1{ F₁() -> non empty HGrStr , F₂() -> non empty Subset of F₁() } :

ex b₁ being non empty strict SubStr of F₁() st the carrier of b₁ = F₂()

provided

E49: for b₁, b₂ being Element of F₂() holds b₁ * b₂ in F₂()

proof end;

scheme :: MONOID_0:sch 2
s2{ F₁() -> non empty HGrStr , P₁[ set ] } :

ex b₁ being non empty strict SubStr of F₁() st
for b₂ being Element of F₁() holds
( b₂ in the carrier of b₁ iff P₁[b₂] )

provided

E49: for b₁, b₂ being Element of F₁() st P₁[b₁] & P₁[b₂] holds
P₁[b₁ * b₂] and
E50: ex b₁ being Element of F₁() st P₁[b₁]

proof end;

scheme :: MONOID_0:sch 3
s3{ F₁() -> non empty multLoopStr , F₂() -> non empty Subset of F₁() } :

ex b₁ being non empty strict MonoidalSubStr of F₁() st the carrier of b₁ = F₂()

provided

E49: for b₁, b₂ being Element of F₂() holds b₁ * b₂ in F₂() and
E50: the unity of F₁() in F₂()

proof end;

scheme :: MONOID_0:sch 4
s4{ F₁() -> non empty multLoopStr , P₁[ set ] } :

ex b₁ being non empty strict MonoidalSubStr of F₁() st
for b₂ being Element of F₁() holds
( b₂ in the carrier of b₁ iff P₁[b₂] )

provided

E49: for b₁, b₂ being Element of F₁() st P₁[b₁] & P₁[b₂] holds
P₁[b₁ * b₂] and
E50: P₁[the unity of F₁()]

proof end;

notation

let c₁ be non empty HGrStr ;
let c₂, c₃ be Element of c₁;
synonym c₂ [*] c₃ for c₂ * c₃;

end;

definition

let c₁ be non empty HGrStr ;
let c₂, c₃ be Element of c₁;
redefine func [*] as c₂ [*] c₃ -> Element of a₁;
coherence ;

end;

definition

func <REAL,+> -> non empty strict unital associative commutative invertible cancelable HGrStr equals :: MONOID_0:def 26
HGrStr(# REAL ,addreal #);
coherence

proof end;

end;

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

theorem Th40: :: MONOID_0:40

( the carrier of <REAL,+> = REAL & the mult of <REAL,+> = addreal & ( for b₁, b₂ being Element of <REAL,+>
for b₃, b₄ being Real st b₁ = b₃ & b₂ = b₄ holds
b₁ * b₂ = b₃ + b₄ ) ) by BINOP_2:def 9;

theorem Th41: :: MONOID_0:41

for b₁ being set holds
( b₁ is Element of <REAL,+> iff b₁ is Real ) ;

theorem Th42: :: MONOID_0:42

the_unity_wrt the mult of <REAL,+> = 0 by BINOP_2:2;

theorem Th43: :: MONOID_0:43

for b₁ being non empty SubStr of <REAL,+>
for b₂, b₃ being Element of b₁
for b₄, b₅ being Real st b₂ = b₄ & b₃ = b₅ holds
b₂ * b₃ = b₄ + b₅

proof end;

theorem Th44: :: MONOID_0:44

for b₁ being non empty unital SubStr of <REAL,+> holds the_unity_wrt the mult of b₁ = 0

proof end;

registration

let c₁ be non empty unital HGrStr ;
cluster non empty associative invertible -> non empty unital Group-like left-cancelable right-cancelable cancelable SubStr of a₁;
coherence

proof end;

end;

definition

redefine func INT.Group as INT.Group -> non empty strict unital invertible SubStr of <REAL,+> ;
coherence

proof end;

end;

theorem Th45: :: MONOID_0:45

canceled;

theorem Th46: :: MONOID_0:46

for b₁ being non empty strict SubStr of <REAL,+> holds
( b₁ = INT.Group iff the carrier of b₁ = INT ) by Th28, GR_CY_1:def 4;

theorem Th47: :: MONOID_0:47

for b₁ being set holds
( b₁ is Element of INT.Group iff b₁ is Integer ) by GR_CY_1:def 4, INT_1:def 2;

definition

func <NAT,+> -> non empty strict unital uniquely-decomposable SubStr of INT.Group means :Def27: :: MONOID_0:def 27
the carrier of a₁ = NAT ;
existence

proof end;

uniqueness by Th28;

end;

:: deftheorem Def27 defines <NAT,+> MONOID_0:def 27 :

definition

func <NAT,+,0> -> non empty strict well-unital MonoidalExtension of <NAT,+> means :: MONOID_0:def 28
verum;
existence ;
uniqueness by Th22;

end;

:: deftheorem Def28 defines <NAT,+,0> MONOID_0:def 28 :

definition

redefine func addnat -> Relation of [:NAT ,NAT :], NAT equals :Def29: :: MONOID_0:def 29
the mult of <NAT,+> ;
compatibility

proof end;

end;

:: deftheorem Def29 defines addnat MONOID_0:def 29 :

theorem Th48: :: MONOID_0:48

canceled;

theorem Th49: :: MONOID_0:49

<NAT,+> = HGrStr(# NAT ,addnat #) by Def27, Def29;

theorem Th50: :: MONOID_0:50

for b₁ being set holds
( b₁ is Element of <NAT,+,0> iff b₁ is Nat )

proof end;

theorem Th51: :: MONOID_0:51

for b₁, b₂ being Nat
for b₃, b₄ being Element of <NAT,+,0> st b₁ = b₃ & b₂ = b₄ holds
b₃ * b₄ = b₁ + b₂

proof end;

theorem Th52: :: MONOID_0:52

<NAT,+,0> = multLoopStr(# NAT ,addnat ,0 #)

proof end;

theorem Th53: :: MONOID_0:53

( addnat = addreal || NAT & addnat = addint || NAT )

proof end;

theorem Th54: :: MONOID_0:54

( 0 is_a_unity_wrt addnat & addnat is uniquely-decomposable )

proof end;

definition

func <REAL,*> -> non empty strict unital associative commutative HGrStr equals :: MONOID_0:def 30
HGrStr(# REAL ,multreal #);
coherence

proof end;

end;

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

theorem Th55: :: MONOID_0:55

( the carrier of <REAL,*> = REAL & the mult of <REAL,*> = multreal & ( for b₁, b₂ being Element of <REAL,*>
for b₃, b₄ being Real st b₁ = b₃ & b₂ = b₄ holds
b₁ * b₂ = b₃ * b₄ ) ) by BINOP_2:def 11;

theorem Th56: :: MONOID_0:56

for b₁ being set holds
( b₁ is Element of <REAL,*> iff b₁ is Real ) ;

theorem Th57: :: MONOID_0:57

the_unity_wrt the mult of <REAL,*> = 1 by BINOP_2:7;

theorem Th58: :: MONOID_0:58

for b₁ being non empty SubStr of <REAL,*>
for b₂, b₃ being Element of b₁
for b₄, b₅ being Real st b₂ = b₄ & b₃ = b₅ holds
b₂ * b₃ = b₄ * b₅

proof end;

theorem Th59: :: MONOID_0:59

canceled;

theorem Th60: :: MONOID_0:60

for b₁ being non empty unital SubStr of <REAL,*> holds
( the_unity_wrt the mult of b₁ = 0 or the_unity_wrt the mult of b₁ = 1 )

proof end;

definition

func <NAT,*> -> non empty strict unital uniquely-decomposable SubStr of <REAL,*> means :Def31: :: MONOID_0:def 31
the carrier of a₁ = NAT ;
existence

proof end;

uniqueness by Th28;

end;

:: deftheorem Def31 defines <NAT,*> MONOID_0:def 31 :

definition

func <NAT,*,1> -> non empty strict well-unital MonoidalExtension of <NAT,*> means :: MONOID_0:def 32
verum;
uniqueness by Th22;
existence ;

end;

:: deftheorem Def32 defines <NAT,*,1> MONOID_0:def 32 :

definition

redefine func multnat -> Relation of [:NAT ,NAT :], NAT equals :Def33: :: MONOID_0:def 33
the mult of <NAT,*> ;
compatibility

proof end;

end;

:: deftheorem Def33 defines multnat MONOID_0:def 33 :

theorem Th61: :: MONOID_0:61

<NAT,*> = HGrStr(# NAT ,multnat #) by Def31, Def33;

theorem Th62: :: MONOID_0:62

for b₁, b₂ being Nat
for b₃, b₄ being Element of <NAT,*> st b₁ = b₃ & b₂ = b₄ holds
b₃ * b₄ = b₁ * b₂ by Th58;

theorem Th63: :: MONOID_0:63

the_unity_wrt the mult of <NAT,*> = 1

proof end;

theorem Th64: :: MONOID_0:64

for b₁, b₂ being Nat
for b₃, b₄ being Element of <NAT,*,1> st b₁ = b₃ & b₂ = b₄ holds
b₃ * b₄ = b₁ * b₂

proof end;

theorem Th65: :: MONOID_0:65

<NAT,*,1> = multLoopStr(# NAT ,multnat ,1 #)

proof end;

theorem Th66: :: MONOID_0:66

multnat = multreal || NAT by Th26, Th61;

theorem Th67: :: MONOID_0:67

( 1 is_a_unity_wrt multnat & multnat is uniquely-decomposable )

proof end;

definition

let c₁ be non empty set ;
func c₁ *+^ -> non empty strict unital associative constituted-FinSeqs cancelable uniquely-decomposable HGrStr means :Def34: :: MONOID_0:def 34
( the carrier of a₂ = a₁ * & ( for b₁, b₂ being Element of a₂ holds b₁ [*] b₂ = b₁ ^ b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def34 defines *+^ MONOID_0:def 34 :

definition

let c₁ be non empty set ;
func c₁ *+^+<0> -> non empty strict well-unital MonoidalExtension of a₁ *+^ means :: MONOID_0:def 35
verum;
correctness by Th22;
func c₁ -concatenation -> BinOp of a₁ * equals :: MONOID_0:def 36
the mult of (a₁ *+^ );
correctness

proof end;

end;

:: deftheorem Def35 defines *+^+<0> MONOID_0:def 35 :

:: deftheorem Def36 defines -concatenation MONOID_0:def 36 :

theorem Th68: :: MONOID_0:68

for b₁ being non empty set holds b₁ *+^ = HGrStr(# (b₁ * ),(b₁ -concatenation ) #) by Def34;

theorem Th69: :: MONOID_0:69

for b₁ being non empty set holds the_unity_wrt the mult of (b₁ *+^ ) = {}

proof end;

theorem Th70: :: MONOID_0:70

for b₁ being non empty set holds
( the carrier of (b₁ *+^+<0> ) = b₁ * & the mult of (b₁ *+^+<0> ) = b₁ -concatenation & the unity of (b₁ *+^+<0> ) = {} )

proof end;

theorem Th71: :: MONOID_0:71

for b₁ being non empty set
for b₂, b₃ being Element of (b₁ *+^+<0> ) holds b₂ [*] b₃ = b₂ ^ b₃

proof end;

theorem Th72: :: MONOID_0:72

for b₁ being non empty set
for b₂ being non empty SubStr of b₁ *+^
for b₃, b₄ being Element of b₂ holds b₃ [*] b₄ = b₃ ^ b₄

proof end;

theorem Th73: :: MONOID_0:73

for b₁ being non empty set
for b₂ being non empty unital SubStr of b₁ *+^ holds the_unity_wrt the mult of b₂ = {}

proof end;

theorem Th74: :: MONOID_0:74

for b₁ being non empty set
for b₂ being non empty SubStr of b₁ *+^ st {} is Element of b₂ holds
( b₂ is unital & the_unity_wrt the mult of b₂ = {} )

proof end;

theorem Th75: :: MONOID_0:75

for b₁, b₂ being non empty set st b₁ c= b₂ holds
b₁ *+^ is SubStr of b₂ *+^

proof end;

theorem Th76: :: MONOID_0:76

for b₁ being non empty set holds
( b₁ -concatenation has_a_unity & the_unity_wrt (b₁ -concatenation ) = {} & b₁ -concatenation is associative )

proof end;

definition

let c₁ be set ;
func GPFuncs c₁ -> non empty strict unital associative constituted-Functions HGrStr means :Def37: :: MONOID_0:def 37
( the carrier of a₂ = PFuncs a₁,a₁ & ( for b₁, b₂ being Element of a₂ holds b₁ [*] b₂ = b₁ (*) b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def37 defines GPFuncs MONOID_0:def 37 :

definition

let c₁ be set ;
func MPFuncs c₁ -> non empty strict well-unital MonoidalExtension of GPFuncs a₁ means :: MONOID_0:def 38
verum;
existence ;
uniqueness by Th22;
func c₁ -composition -> BinOp of PFuncs a₁,a₁ equals :: MONOID_0:def 39
the mult of (GPFuncs a₁);
correctness

proof end;

end;

:: deftheorem Def38 defines MPFuncs MONOID_0:def 38 :

:: deftheorem Def39 defines -composition MONOID_0:def 39 :

theorem Th77: :: MONOID_0:77

for b₁, b₂ being set holds
( b₁ is Element of (GPFuncs b₂) iff b₁ is PartFunc of b₂,b₂ )

proof end;

theorem Th78: :: MONOID_0:78

for b₁ being set holds the_unity_wrt the mult of (GPFuncs b₁) = id b₁

proof end;

theorem Th79: :: MONOID_0:79

for b₁ being set
for b₂ being non empty SubStr of GPFuncs b₁
for b₃, b₄ being Element of b₂ holds b₃ [*] b₄ = b₃ (*) b₄

proof end;

theorem Th80: :: MONOID_0:80

for b₁ being set
for b₂ being non empty SubStr of GPFuncs b₁ st id b₁ is Element of b₂ holds
( b₂ is unital & the_unity_wrt the mult of b₂ = id b₁ )

proof end;

theorem Th81: :: MONOID_0:81

for b₁, b₂ being set st b₁ c= b₂ holds
GPFuncs b₁ is SubStr of GPFuncs b₂

proof end;

Lemma69: for b₁, b₂ being set st b₁ in Funcs b₂,b₂ holds
b₁ is Function of b₂,b₂

proof end;

definition

let c₁ be set ;
func GFuncs c₁ -> non empty strict unital SubStr of GPFuncs a₁ means :Def40: :: MONOID_0:def 40
the carrier of a₂ = Funcs a₁,a₁;
existence

proof end;

uniqueness by Th28;

end;

:: deftheorem Def40 defines GFuncs MONOID_0:def 40 :

definition

let c₁ be set ;
func MFuncs c₁ -> strict well-unital MonoidalExtension of GFuncs a₁ means :: MONOID_0:def 41
verum;
correctness by Th22;

end;

:: deftheorem Def41 defines MFuncs MONOID_0:def 41 :

theorem Th82: :: MONOID_0:82

for b₁, b₂ being set holds
( b₁ is Element of (GFuncs b₂) iff b₁ is Function of b₂,b₂ )

proof end;

theorem Th83: :: MONOID_0:83

for b₁ being set holds the mult of (GFuncs b₁) = (b₁ -composition ) || (Funcs b₁,b₁)

proof end;

theorem Th84: :: MONOID_0:84

for b₁ being set holds the_unity_wrt the mult of (GFuncs b₁) = id b₁

proof end;

theorem Th85: :: MONOID_0:85

for b₁ being set holds
( the carrier of (MFuncs b₁) = Funcs b₁,b₁ & the mult of (MFuncs b₁) = (b₁ -composition ) || (Funcs b₁,b₁) & the unity of (MFuncs b₁) = id b₁ )

proof end;

definition

let c₁ be set ;
func GPerms c₁ -> non empty strict unital invertible SubStr of GFuncs a₁ means :Def42: :: MONOID_0:def 42
for b₁ being Element of (GFuncs a₁) holds
( b₁ in the carrier of a₂ iff b₁ is Permutation of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def42 defines GPerms MONOID_0:def 42 :

theorem Th86: :: MONOID_0:86

for b₁, b₂ being set holds
( b₁ is Element of (GPerms b₂) iff b₁ is Permutation of b₂ )

proof end;

theorem Th87: :: MONOID_0:87

for b₁ being set holds
( the_unity_wrt the mult of (GPerms b₁) = id b₁ & 1. (GPerms b₁) = id b₁ )

proof end;

theorem Th88: :: MONOID_0:88

for b₁ being set
for b₂ being Element of (GPerms b₁) holds b₂ " = b₂ "

proof end;

theorem Th89: :: MONOID_0:89

for b₁ being 1-sorted st the carrier of b₁ is functional holds
b₁ is constituted-Functions

proof end;