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