:: MONOID_1 semantic presentation

deffunc H₁( HGrStr ) -> M6([:the carrier of $1,the carrier of $1:],the carrier of $1) = the mult of $1;

deffunc H₂( multLoopStr ) -> Element of the carrier of $1 = the unity of $1;

definition

let D1, D2, D be non empty set ;
mode Function of D1,D2,D is Function of [:D1,D2:],D;

end;

definition

let f be Function;
let x1, x2, y be set ;
func f .. x1,x2,y -> set equals :: MONOID_1:def 1
f .. [x1,x2],y;
correctness ;

end;

:: deftheorem defines .. MONOID_1:def 1 :

theorem Th1: :: MONOID_1:1

for f, g being Function
for x1, x2, x being set st [x1,x2] in dom f & g = f . x1,x2 & x in dom g holds
f .. x1,x2,x = g . x by FUNCT_6:44;

definition

let A, D1, D2, D be non empty set ;
let f be Function of D1,D2, Funcs A,D;
let x1 be Element of D1;
let x2 be Element of D2;
let x be Element of A;
:: original: ..
redefine func f .. x1,x2,x -> Element of D;
coherence

proof end;

end;

definition

let A be set ;
let D1, D2, D be non empty set ;
let f be Function of D1,D2,D;
let g1 be Function of A,D1;
let g2 be Function of A,D2;
:: original: .:
redefine func f .: g1,g2 -> Element of Funcs A,D;
coherence

proof end;

end;

notation

let A be non empty set ;
let n be Nat;
let x be Element of A;
synonym n .--> x for A |-> n;

end;

definition

let A be non empty set ;
let n be Nat;
let x be Element of A;
:: original: .-->
redefine func n .--> x -> FinSequence of A;
coherence by FINSEQ_2:77;

end;

definition

let D be non empty set ;
let A be set ;
let d be Element of D;
:: original: -->
redefine func A --> d -> Element of Funcs A,D;
coherence

proof end;

end;

definition

let A be set ;
let D1, D2, D be non empty set ;
let f be Function of D1,D2,D;
let d be Element of D1;
let g be Function of A,D2;
:: original: [;]
redefine func f [;] d,g -> Element of Funcs A,D;
coherence

proof end;

end;

definition

let A be set ;
let D1, D2, D be non empty set ;
let f be Function of D1,D2,D;
let g be Function of A,D1;
let d be Element of D2;
:: original: [:]
redefine func f [:] g,d -> Element of Funcs A,D;
coherence

proof end;

end;

theorem :: MONOID_1:2

for f, g being Function
for X being set holds (f | X) * g = f * (X | g)

proof end;

scheme :: MONOID_1:sch 1
NonUniqFuncDEx{ F₁() -> set , F₂() -> non empty set , P₁[ set , set ] } :

ex f being Function of F₁(),F₂() st
for x being set st x in F₁() holds
P₁[x,f . x]

provided

A1: for x being set st x in F₁() holds
ex y being Element of F₂() st P₁[x,y]

proof end;

definition

let D1, D2, D be non empty set ;
let f be Function of D1,D2,D;
let A be set ;
func f,D .: A -> Function of (Funcs A,D1),(Funcs A,D2), Funcs A,D means :Def2: :: MONOID_1:def 2
for f1 being Element of Funcs A,D1
for f2 being Element of Funcs A,D2 holds it . f1,f2 = f .: f1,f2;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines .: MONOID_1:def 2 :

theorem :: MONOID_1:3

for D1, D2, D being non empty set
for f being Function of D1,D2,D
for A being set
for f1 being Function of A,D1
for f2 being Function of A,D2
for x being set st x in A holds
(f,D .: A) .. f1,f2,x = f . (f1 . x),(f2 . x)

proof end;

theorem Th4: :: MONOID_1:4

for A being set
for D being non empty set
for o being BinOp of D
for f, g being Function of A,D st o is commutative holds
o .: f,g = o .: g,f

proof end;

theorem Th5: :: MONOID_1:5

for A being set
for D being non empty set
for o being BinOp of D
for f, g, h being Function of A,D st o is associative holds
o .: (o .: f,g),h = o .: f,(o .: g,h)

proof end;

theorem Th6: :: MONOID_1:6

for A being set
for D being non empty set
for a being Element of D
for o being BinOp of D
for f being Function of A,D st a is_a_unity_wrt o holds
( o [;] a,f = f & o [:] f,a = f )

proof end;

theorem Th7: :: MONOID_1:7

for A being set
for D being non empty set
for o being BinOp of D
for f being Function of A,D st o is idempotent holds
o .: f,f = f

proof end;

theorem Th8: :: MONOID_1:8

for A being set
for D being non empty set
for o being BinOp of D st o is commutative holds
o,D .: A is commutative

proof end;

theorem Th9: :: MONOID_1:9

for A being set
for D being non empty set
for o being BinOp of D st o is associative holds
o,D .: A is associative

proof end;

theorem Th10: :: MONOID_1:10

for A being set
for D being non empty set
for a being Element of D
for o being BinOp of D st a is_a_unity_wrt o holds
A --> a is_a_unity_wrt o,D .: A

proof end;

theorem Th11: :: MONOID_1:11

for A being set
for D being non empty set
for o being BinOp of D st o has_a_unity holds
( the_unity_wrt (o,D .: A) = A --> (the_unity_wrt o) & o,D .: A has_a_unity )

proof end;

theorem Th12: :: MONOID_1:12

for A being set
for D being non empty set
for o being BinOp of D st o is idempotent holds
o,D .: A is idempotent

proof end;

theorem Th13: :: MONOID_1:13

for A being set
for D being non empty set
for o being BinOp of D st o is invertible holds
o,D .: A is invertible

proof end;

theorem Th14: :: MONOID_1:14

for A being set
for D being non empty set
for o being BinOp of D st o is cancelable holds
o,D .: A is cancelable

proof end;

theorem Th15: :: MONOID_1:15

for A being set
for D being non empty set
for o being BinOp of D st o is uniquely-decomposable holds
o,D .: A is uniquely-decomposable

proof end;

theorem :: MONOID_1:16

for A being set
for D being non empty set
for o, o' being BinOp of D st o absorbs o' holds
o,D .: A absorbs o',D .: A

proof end;

theorem Th17: :: MONOID_1:17

for A being set
for D1, D2, D, E1, E2, E being non empty set
for o1 being Function of D1,D2,D
for o2 being Function of E1,E2,E st o1 <= o2 holds
o1,D .: A <= o2,E .: A

proof end;

definition

let G be non empty HGrStr ;
let A be set ;
func .: G,A -> HGrStr equals :Def3: :: MONOID_1:def 3
multLoopStr(# (Funcs A,the carrier of G),(the mult of G,the carrier of G .: A),(A --> (the_unity_wrt the mult of G)) #) if G is unital
otherwise HGrStr(# (Funcs A,the carrier of G),(the mult of G,the carrier of G .: A) #);
correctness ;

end;

:: deftheorem Def3 defines .: MONOID_1:def 3 :

registration

let G be non empty HGrStr ;
let A be set ;
cluster .: G,A -> non empty ;
coherence

proof end;

end;

deffunc H₃( non empty HGrStr ) -> set = the carrier of $1;

theorem Th18: :: MONOID_1:18

for X being set
for G being non empty HGrStr holds
( the carrier of (.: G,X) = Funcs X,the carrier of G & the mult of (.: G,X) = the mult of G,the carrier of G .: X )

proof end;

theorem :: MONOID_1:19

for x, X being set
for G being non empty HGrStr holds
( x is Element of (.: G,X) iff x is Function of X,the carrier of G )

proof end;

Lm1: for X being set
for G being non empty HGrStr holds .: G,X is constituted-Functions

proof end;

registration

let G be non empty HGrStr ;
let A be set ;
cluster .: G,A -> non empty constituted-Functions ;
coherence by Lm1;

end;

theorem Th20: :: MONOID_1:20

for X being set
for G being non empty HGrStr
for f being Element of (.: G,X) holds
( dom f = X & rng f c= the carrier of G )

proof end;

theorem Th21: :: MONOID_1:21

for X being set
for G being non empty HGrStr
for f, g being Element of (.: G,X) st ( for x being set st x in X holds
f . x = g . x ) holds
f = g

proof end;

definition

let G be non empty HGrStr ;
let A be non empty set ;
let f be Element of (.: G,A);
let a be Element of A;
:: original: .
redefine func f . a -> Element of G;
coherence

proof end;

end;

registration

let G be non empty HGrStr ;
let A be non empty set ;
let f be Element of (.: G,A);
cluster rng f -> non empty ;
coherence

proof end;

end;

theorem Th22: :: MONOID_1:22

for D being non empty set
for G being non empty HGrStr
for f1, f2 being Element of (.: G,D)
for a being Element of D holds (f1 * f2) . a = (f1 . a) * (f2 . a)

proof end;

definition

let G be non empty unital HGrStr ;
let A be set ;
:: original: .:
redefine func .: G,A -> non empty strict well-unital constituted-Functions multLoopStr ;
coherence

proof end;

end;

theorem Th23: :: MONOID_1:23

for X being set
for G being non empty unital HGrStr holds the unity of (.: G,X) = X --> (the_unity_wrt the mult of G)

proof end;

theorem Th24: :: MONOID_1:24

for G being non empty HGrStr
for A being set holds
( ( G is commutative implies .: G,A is commutative ) & ( G is associative implies .: G,A is associative ) & ( G is idempotent implies .: G,A is idempotent ) & ( G is invertible implies .: G,A is invertible ) & ( G is cancelable implies .: G,A is cancelable ) & ( G is uniquely-decomposable implies .: G,A is uniquely-decomposable ) )

proof end;

theorem :: MONOID_1:25

for X being set
for G being non empty HGrStr
for H being non empty SubStr of G holds .: H,X is SubStr of .: G,X

proof end;

theorem :: MONOID_1:26

for X being set
for G being non empty unital HGrStr
for H being non empty SubStr of G st the_unity_wrt the mult of G in the carrier of H holds
.: H,X is MonoidalSubStr of .: G,X

proof end;

definition

let G be non empty unital associative commutative cancelable uniquely-decomposable HGrStr ;
let A be set ;
:: original: .:
redefine func .: G,A -> commutative strict constituted-Functions cancelable uniquely-decomposable Monoid;
coherence

proof end;

end;

definition

let A be set ;
func MultiSet_over A -> commutative strict constituted-Functions cancelable uniquely-decomposable Monoid equals :: MONOID_1:def 4
.: <NAT,+,0> ,A;
correctness ;

end;

:: deftheorem defines MultiSet_over MONOID_1:def 4 :

theorem Th27: :: MONOID_1:27

for X being set holds
( the carrier of (MultiSet_over X) = Funcs X,NAT & the mult of (MultiSet_over X) = addnat ,NAT .: X & the unity of (MultiSet_over X) = X --> 0 )

proof end;

definition

let A be set ;
mode Multiset of A is Element of (MultiSet_over A);

end;

theorem Th28: :: MONOID_1:28

for x, X being set holds
( x is Multiset of X iff x is Function of X, NAT )

proof end;

theorem Th29: :: MONOID_1:29

for X being set
for m being Multiset of X holds
( dom m = X & rng m c= NAT )

proof end;

definition

let A be non empty set ;
let m be Multiset of A;
:: original: rng
redefine func rng m -> non empty Subset of NAT ;
coherence

proof end;

let a be Element of A;
:: original: .
redefine func m . a -> Nat;
coherence

proof end;

end;

theorem Th30: :: MONOID_1:30

for D being non empty set
for m1, m2 being Multiset of D
for a being Element of D holds (m1 [*] m2) . a = (m1 . a) + (m2 . a)

proof end;

theorem Th31: :: MONOID_1:31

for Y, X being set holds chi Y,X is Multiset of X

proof end;

definition

let Y, X be set ;
:: original: chi
redefine func chi Y,X -> Multiset of X;
coherence by Th31;

end;

definition

let X be set ;
let n be Nat;
:: original: -->
redefine func X --> n -> Multiset of X;
coherence

proof end;

end;

definition

let A be non empty set ;
let a be Element of A;
func chi a -> Multiset of A equals :: MONOID_1:def 5
chi {a},A;
coherence ;

end;

:: deftheorem defines chi MONOID_1:def 5 :

theorem Th32: :: MONOID_1:32

for A being non empty set
for a, b being Element of A holds
( (chi a) . a = 1 & ( b <> a implies (chi a) . b = 0 ) )

proof end;

theorem Th33: :: MONOID_1:33

for A being non empty set
for m1, m2 being Multiset of A st ( for a being Element of A holds m1 . a = m2 . a ) holds
m1 = m2

proof end;

definition

let A be set ;
func finite-MultiSet_over A -> non empty strict MonoidalSubStr of MultiSet_over A means :Def6: :: MONOID_1:def 6
for f being Multiset of A holds
( f in the carrier of it iff f " (NAT \ {0}) is finite );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines finite-MultiSet_over MONOID_1:def 6 :

theorem Th34: :: MONOID_1:34

for A being non empty set
for a being Element of A holds chi a is Element of (finite-MultiSet_over A)

proof end;

theorem Th35: :: MONOID_1:35

for x being set
for A being non empty set
for p being FinSequence of A holds dom ({x} | (p ^ <*x*>)) = (dom ({x} | p)) \/ {((len p) + 1)}

proof end;

theorem Th36: :: MONOID_1:36

for x, y being set
for A being non empty set
for p being FinSequence of A st x <> y holds
dom ({x} | (p ^ <*y*>)) = dom ({x} | p)

proof end;

registration

let A be set ;
let F be finite Relation;
cluster A | F -> finite ;
coherence

proof end;

end;

definition

let A be non empty set ;
let p be FinSequence of A;
func |.p.| -> Multiset of A means :Def7: :: MONOID_1:def 7
for a being Element of A holds it . a = card (dom ({a} | p));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines |. MONOID_1:def 7 :

theorem :: MONOID_1:37

for A being non empty set
for a being Element of A holds |.(<*> A).| . a = 0

proof end;

theorem Th38: :: MONOID_1:38

for A being non empty set holds |.(<*> A).| = A --> 0

proof end;

theorem :: MONOID_1:39

for A being non empty set
for a being Element of A holds |.<*a*>.| = chi a

proof end;

theorem Th40: :: MONOID_1:40

for A being non empty set
for a being Element of A
for p being FinSequence of A holds |.(p ^ <*a*>).| = |.p.| [*] (chi a)

proof end;

theorem Th41: :: MONOID_1:41

for A being non empty set
for p, q being FinSequence of A holds |.(p ^ q).| = |.p.| [*] |.q.|

proof end;

theorem Th42: :: MONOID_1:42

for n being Nat
for A being non empty set
for a being Element of A holds
( |.(n .--> a).| . a = n & ( for b being Element of A st b <> a holds
|.(n .--> a).| . b = 0 ) )

proof end;

theorem :: MONOID_1:43

for A being non empty set
for p being FinSequence of A holds |.p.| is Element of (finite-MultiSet_over A)

proof end;

theorem :: MONOID_1:44

for x being set
for A being non empty set st x is Element of (finite-MultiSet_over A) holds
ex p being FinSequence of A st x = |.p.|

proof end;

definition

let D1, D2, D be non empty set ;
let f be Function of D1,D2,D;
func f .:^2 -> Function of (bool D1),(bool D2), bool D means :Def8: :: MONOID_1:def 8
for x being Element of [:(bool D1),(bool D2):] holds it . x = f .: [:(x `1 ),(x `2 ):];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines .:^2 MONOID_1:def 8 :

theorem Th45: :: MONOID_1:45

for D1, D2, D being non empty set
for f being Function of D1,D2,D
for X1 being Subset of D1
for X2 being Subset of D2 holds (f .:^2 ) . X1,X2 = f .: [:X1,X2:]

proof end;

theorem Th46: :: MONOID_1:46

for D1, D2, D being non empty set
for f being Function of D1,D2,D
for X1 being Subset of D1
for X2 being Subset of D2
for x1, x2 being set st x1 in X1 & x2 in X2 holds
f . x1,x2 in (f .:^2 ) . X1,X2

proof end;

theorem :: MONOID_1:47

for D1, D2, D being non empty set
for f being Function of D1,D2,D
for X1 being Subset of D1
for X2 being Subset of D2 holds (f .:^2 ) . X1,X2 = { (f . a,b) where a is Element of D1, b is Element of D2 : ( a in X1 & b in X2 ) }

proof end;

theorem Th48: :: MONOID_1:48

for X, Y being set
for D being non empty set
for o being BinOp of D st o is commutative holds
o .: [:X,Y:] = o .: [:Y,X:]

proof end;

theorem Th49: :: MONOID_1:49

for X, Y, Z being set
for D being non empty set
for o being BinOp of D st o is associative holds
o .: [:(o .: [:X,Y:]),Z:] = o .: [:X,(o .: [:Y,Z:]):]

proof end;

theorem Th50: :: MONOID_1:50

for D being non empty set
for o being BinOp of D st o is commutative holds
o .:^2 is commutative

proof end;

theorem Th51: :: MONOID_1:51

for D being non empty set
for o being BinOp of D st o is associative holds
o .:^2 is associative

proof end;

theorem Th52: :: MONOID_1:52

for X being set
for D being non empty set
for o being BinOp of D
for a being Element of D st a is_a_unity_wrt o holds
( o .: [:{a},X:] = D /\ X & o .: [:X,{a}:] = D /\ X )

proof end;

theorem Th53: :: MONOID_1:53

for D being non empty set
for o being BinOp of D
for a being Element of D st a is_a_unity_wrt o holds
( {a} is_a_unity_wrt o .:^2 & o .:^2 has_a_unity & the_unity_wrt (o .:^2 ) = {a} )

proof end;

theorem Th54: :: MONOID_1:54

for D being non empty set
for o being BinOp of D st o has_a_unity holds
( o .:^2 has_a_unity & {(the_unity_wrt o)} is_a_unity_wrt o .:^2 & the_unity_wrt (o .:^2 ) = {(the_unity_wrt o)} )

proof end;

theorem Th55: :: MONOID_1:55

for D being non empty set
for o being BinOp of D st o is uniquely-decomposable holds
o .:^2 is uniquely-decomposable

proof end;

definition

let G be non empty HGrStr ;
func bool G -> HGrStr equals :Def9: :: MONOID_1:def 9
multLoopStr(# (bool the carrier of G),(the mult of G .:^2 ),{(the_unity_wrt the mult of G)} #) if G is unital
otherwise HGrStr(# (bool the carrier of G),(the mult of G .:^2 ) #);
correctness ;

end;

:: deftheorem Def9 defines bool MONOID_1:def 9 :

registration

let G be non empty HGrStr ;
cluster bool G -> non empty ;
coherence

proof end;

end;

definition

let G be non empty unital HGrStr ;
:: original: bool
redefine func bool G -> non empty strict well-unital multLoopStr ;
coherence

proof end;

end;

theorem Th56: :: MONOID_1:56

for G being non empty HGrStr holds
( the carrier of (bool G) = bool the carrier of G & the mult of (bool G) = the mult of G .:^2 )

proof end;

theorem :: MONOID_1:57

for G being non empty unital HGrStr holds the unity of (bool G) = {(the_unity_wrt the mult of G)}

proof end;

theorem :: MONOID_1:58

for G being non empty HGrStr holds
( ( G is commutative implies bool G is commutative ) & ( G is associative implies bool G is associative ) & ( G is uniquely-decomposable implies bool G is uniquely-decomposable ) )

proof end;