Definition df-sgrp 13045

Description: A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 12999), 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

Step	Hyp	Ref	Expression
1		csgrp 13044	. 2 class Smgrp
2		vx	. . . . . . . . . . . 12 setvar 𝑥
3	2	cv 1363	. . . . . . . . . . 11 class 𝑥
4		vy	. . . . . . . . . . . 12 setvar 𝑦
5	4	cv 1363	. . . . . . . . . . 11 class 𝑦
6		vo	. . . . . . . . . . . 12 setvar 𝑜
7	6	cv 1363	. . . . . . . . . . 11 class 𝑜
8	3, 5, 7	co 5922	. . . . . . . . . 10 class (𝑥𝑜𝑦)
9		vz	. . . . . . . . . . 11 setvar 𝑧
10	9	cv 1363	. . . . . . . . . 10 class 𝑧
11	8, 10, 7	co 5922	. . . . . . . . 9 class ((𝑥𝑜𝑦)𝑜𝑧)
12	5, 10, 7	co 5922	. . . . . . . . . 10 class (𝑦𝑜𝑧)
13	3, 12, 7	co 5922	. . . . . . . . 9 class (𝑥𝑜(𝑦𝑜𝑧))
14	11, 13	wceq 1364	. . . . . . . 8 wff ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
15		vb	. . . . . . . . 9 setvar 𝑏
16	15	cv 1363	. . . . . . . 8 class 𝑏
17	14, 9, 16	wral 2475	. . . . . . 7 wff ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
18	17, 4, 16	wral 2475	. . . . . 6 wff ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
19	18, 2, 16	wral 2475	. . . . 5 wff ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
20		vg	. . . . . . 7 setvar 𝑔
21	20	cv 1363	. . . . . 6 class 𝑔
22		cplusg 12755	. . . . . 6 class +g
23	21, 22	cfv 5258	. . . . 5 class (+g‘𝑔)
24	19, 6, 23	wsbc 2989	. . . 4 wff [(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
25		cbs 12678	. . . . 5 class Base
26	21, 25	cfv 5258	. . . 4 class (Base‘𝑔)
27	24, 15, 26	wsbc 2989	. . 3 wff [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))
28		cmgm 12997	. . 3 class Mgm
29	27, 20, 28	crab 2479	. 2 class {𝑔 ∈ Mgm ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
30	1, 29	wceq 1364	1 wff Smgrp = {𝑔 ∈ Mgm ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}

This definition is referenced by:  issgrp  13046