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 = { 𝑔 ∈ Smgrp ∣ [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g ‘ 𝑔 ) / 𝑝 ] ∃ 𝑒 ∈ 𝑏 ∀ 𝑥 ∈ 𝑏 ( ( 𝑒 𝑝 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑝 𝑒 ) = 𝑥 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmnd	⊢ Mnd
1		vg	⊢ 𝑔
2		csgrp	⊢ Smgrp
3		cbs	⊢ Base
4	1	cv	⊢ 𝑔
5	4 3	cfv	⊢ ( Base ‘ 𝑔 )
6		vb	⊢ 𝑏
7		cplusg	⊢ +g
8	4 7	cfv	⊢ ( +g ‘ 𝑔 )
9		vp	⊢ 𝑝
10		ve	⊢ 𝑒
11	6	cv	⊢ 𝑏
12		vx	⊢ 𝑥
13	10	cv	⊢ 𝑒
14	9	cv	⊢ 𝑝
15	12	cv	⊢ 𝑥
16	13 15 14	co	⊢ ( 𝑒 𝑝 𝑥 )
17	16 15	wceq	⊢ ( 𝑒 𝑝 𝑥 ) = 𝑥
18	15 13 14	co	⊢ ( 𝑥 𝑝 𝑒 )
19	18 15	wceq	⊢ ( 𝑥 𝑝 𝑒 ) = 𝑥
20	17 19	wa	⊢ ( ( 𝑒 𝑝 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑝 𝑒 ) = 𝑥 )
21	20 12 11	wral	⊢ ∀ 𝑥 ∈ 𝑏 ( ( 𝑒 𝑝 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑝 𝑒 ) = 𝑥 )
22	21 10 11	wrex	⊢ ∃ 𝑒 ∈ 𝑏 ∀ 𝑥 ∈ 𝑏 ( ( 𝑒 𝑝 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑝 𝑒 ) = 𝑥 )
23	22 9 8	wsbc	⊢ [ ( +g ‘ 𝑔 ) / 𝑝 ] ∃ 𝑒 ∈ 𝑏 ∀ 𝑥 ∈ 𝑏 ( ( 𝑒 𝑝 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑝 𝑒 ) = 𝑥 )
24	23 6 5	wsbc	⊢ [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g ‘ 𝑔 ) / 𝑝 ] ∃ 𝑒 ∈ 𝑏 ∀ 𝑥 ∈ 𝑏 ( ( 𝑒 𝑝 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑝 𝑒 ) = 𝑥 )
25	24 1 2	crab	⊢ { 𝑔 ∈ Smgrp ∣ [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g ‘ 𝑔 ) / 𝑝 ] ∃ 𝑒 ∈ 𝑏 ∀ 𝑥 ∈ 𝑏 ( ( 𝑒 𝑝 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑝 𝑒 ) = 𝑥 ) }
26	0 25	wceq	⊢ Mnd = { 𝑔 ∈ Smgrp ∣ [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g ‘ 𝑔 ) / 𝑝 ] ∃ 𝑒 ∈ 𝑏 ∀ 𝑥 ∈ 𝑏 ( ( 𝑒 𝑝 𝑥 ) = 𝑥 ∧ ( 𝑥 𝑝 𝑒 ) = 𝑥 ) }