Definition 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 ) }