This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ALGEBRAIC STRUCTURES Monoids Definition and basic properties of monoids df-mnd
Description: Amonoid is a semigroup, which has a two-sided neutral element.
Definition 2 in BourbakiAlg1 p. 12. In other words (according to the
definition in Lang p. 3), a monoid is a set equipped with an
everywhere defined internal operation (see mndcl ), whose operation is
associative (see mndass ) and has a two-sided neutral element (see
mndid ), see also ismnd . (Contributed by Mario Carneiro , 6-Jan-2015) (Revised by AV , 1-Feb-2020)
Ref
Expression
Assertion
df-mnd |- Mnd = { g e. Smgrp | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x ) }
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cmnd |- Mnd
1
vg |- g
2
csgrp |- Smgrp
3
cbs |- Base
4
1
cv |- g
5
4 3
cfv |- ( Base ` g )
6
vb |- b
7
cplusg |- +g
8
4 7
cfv |- ( +g ` g )
9
vp |- p
10
ve |- e
11
6
cv |- b
12
vx |- x
13
10
cv |- e
14
9
cv |- p
15
12
cv |- x
16
13 15 14
co |- ( e p x )
17
16 15
wceq |- ( e p x ) = x
18
15 13 14
co |- ( x p e )
19
18 15
wceq |- ( x p e ) = x
20
17 19
wa |- ( ( e p x ) = x /\ ( x p e ) = x )
21
20 12 11
wral |- A. x e. b ( ( e p x ) = x /\ ( x p e ) = x )
22
21 10 11
wrex |- E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x )
23
22 9 8
wsbc |- [. ( +g ` g ) / p ]. E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x )
24
23 6 5
wsbc |- [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x )
25
24 1 2
crab |- { g e. Smgrp | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x ) }
26
0 25
wceq |- Mnd = { g e. Smgrp | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. E. e e. b A. x e. b ( ( e p x ) = x /\ ( x p e ) = x ) }