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

Definition df-sgrp 18017
Description: A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 17968), whose operation is associative. Definition in section II.1 of [Bruck] p. 23, or of an "associative magma" in definition 5 of [BourbakiAlg1] p. 4 . (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
Assertion
Ref Expression
df-sgrp Smgrp = {𝑔 ∈ Mgm ∣ [(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
Distinct variable group:   𝑔,𝑏,𝑜,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-sgrp
StepHypRef Expression
1 csgrp 18016 . 2 class Smgrp
2 vx . . . . . . . . . . . 12 setvar 𝑥
32cv 1541 . . . . . . . . . . 11 class 𝑥
4 vy . . . . . . . . . . . 12 setvar 𝑦
54cv 1541 . . . . . . . . . . 11 class 𝑦
6 vo . . . . . . . . . . . 12 setvar 𝑜
76cv 1541 . . . . . . . . . . 11 class 𝑜
83, 5, 7co 7170 . . . . . . . . . 10 class (𝑥𝑜𝑦)
9 vz . . . . . . . . . . 11 setvar 𝑧
109cv 1541 . . . . . . . . . 10 class 𝑧
118, 10, 7co 7170 . . . . . . . . 9 class ((𝑥𝑜𝑦)𝑜𝑧)
125, 10, 7co 7170 . . . . . . . . . 10 class (𝑦𝑜𝑧)
133, 12, 7co 7170 . . . . . . . . 9 class (𝑥𝑜(𝑦𝑜𝑧))
1411, 13wceq 1542 . . . . . . . 8 wff ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
15 vb . . . . . . . . 9 setvar 𝑏
1615cv 1541 . . . . . . . 8 class 𝑏
1714, 9, 16wral 3053 . . . . . . 7 wff 𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
1817, 4, 16wral 3053 . . . . . 6 wff 𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
1918, 2, 16wral 3053 . . . . 5 wff 𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
20 vg . . . . . . 7 setvar 𝑔
2120cv 1541 . . . . . 6 class 𝑔
22 cplusg 16668 . . . . . 6 class +g
2321, 22cfv 6339 . . . . 5 class (+g𝑔)
2419, 6, 23wsbc 3680 . . . 4 wff [(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
25 cbs 16586 . . . . 5 class Base
2621, 25cfv 6339 . . . 4 class (Base‘𝑔)
2724, 15, 26wsbc 3680 . . 3 wff [(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
28 cmgm 17966 . . 3 class Mgm
2927, 20, 28crab 3057 . 2 class {𝑔 ∈ Mgm ∣ [(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
301, 29wceq 1542 1 wff Smgrp = {𝑔 ∈ Mgm ∣ [(Base‘𝑔) / 𝑏][(+g𝑔) / 𝑜]𝑥𝑏𝑦𝑏𝑧𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
Colors of variables: wff setvar class
This definition is referenced by:  issgrp  18018  bj-smgrpssmgm  35060
  Copyright terms: Public domain W3C validator