MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mnd Structured version   Visualization version   GIF version

Definition df-mnd 17060
Description: A monoid 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 17066), whose operation is associative (see mndass 17067) and has a two-sided neutral element (see mndid 17068), see also ismnd 17062. (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.)
Assertion
Ref Expression
df-mnd Mnd = {𝑔 ∈ SGrp ∣ [(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑝]𝑒𝑏𝑥𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)}
Distinct variable group:   𝑒,𝑏,𝑔,𝑝,𝑥

Detailed syntax breakdown of Definition df-mnd
StepHypRef Expression
1 cmnd 17059 . 2 class Mnd
2 ve . . . . . . . . . . 11 setvar 𝑒
32cv 1473 . . . . . . . . . 10 class 𝑒
4 vx . . . . . . . . . . 11 setvar 𝑥
54cv 1473 . . . . . . . . . 10 class 𝑥
6 vp . . . . . . . . . . 11 setvar 𝑝
76cv 1473 . . . . . . . . . 10 class 𝑝
83, 5, 7co 6523 . . . . . . . . 9 class (𝑒𝑝𝑥)
98, 5wceq 1474 . . . . . . . 8 wff (𝑒𝑝𝑥) = 𝑥
105, 3, 7co 6523 . . . . . . . . 9 class (𝑥𝑝𝑒)
1110, 5wceq 1474 . . . . . . . 8 wff (𝑥𝑝𝑒) = 𝑥
129, 11wa 382 . . . . . . 7 wff ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)
13 vb . . . . . . . 8 setvar 𝑏
1413cv 1473 . . . . . . 7 class 𝑏
1512, 4, 14wral 2891 . . . . . 6 wff 𝑥𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)
1615, 2, 14wrex 2892 . . . . 5 wff 𝑒𝑏𝑥𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)
17 vg . . . . . . 7 setvar 𝑔
1817cv 1473 . . . . . 6 class 𝑔
19 cplusg 15710 . . . . . 6 class +g
2018, 19cfv 5786 . . . . 5 class (+g𝑔)
2116, 6, 20wsbc 3397 . . . 4 wff [(+g𝑔) / 𝑝]𝑒𝑏𝑥𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)
22 cbs 15637 . . . . 5 class Base
2318, 22cfv 5786 . . . 4 class (Base‘𝑔)
2421, 13, 23wsbc 3397 . . 3 wff [(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑝]𝑒𝑏𝑥𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)
25 csgrp 17048 . . 3 class SGrp
2624, 17, 25crab 2895 . 2 class {𝑔 ∈ SGrp ∣ [(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑝]𝑒𝑏𝑥𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)}
271, 26wceq 1474 1 wff Mnd = {𝑔 ∈ SGrp ∣ [(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑝]𝑒𝑏𝑥𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)}
Colors of variables: wff setvar class
This definition is referenced by:  ismnddef  17061
  Copyright terms: Public domain W3C validator