Definition df-sgrp 17284

Description: A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 17242), 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	|- SGrp = { g e. Mgm | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) ) }

Distinct variable group:   g, b, o, x, y, z

Detailed syntax breakdown of Definition df-sgrp

Step	Hyp	Ref	Expression
1		csgrp 17283	. 2 class SGrp
2		vx	. . . . . . . . . . . 12 setvar x
3	2	cv 1482	. . . . . . . . . . 11 class x
4		vy	. . . . . . . . . . . 12 setvar y
5	4	cv 1482	. . . . . . . . . . 11 class y
6		vo	. . . . . . . . . . . 12 setvar o
7	6	cv 1482	. . . . . . . . . . 11 class o
8	3, 5, 7	co 6650	. . . . . . . . . 10 class ( x o y )
9		vz	. . . . . . . . . . 11 setvar z
10	9	cv 1482	. . . . . . . . . 10 class z
11	8, 10, 7	co 6650	. . . . . . . . 9 class ( ( x o y ) o z )
12	5, 10, 7	co 6650	. . . . . . . . . 10 class ( y o z )
13	3, 12, 7	co 6650	. . . . . . . . 9 class ( x o ( y o z ) )
14	11, 13	wceq 1483	. . . . . . . 8 wff ( ( x o y ) o z ) = ( x o ( y o z ) )
15		vb	. . . . . . . . 9 setvar b
16	15	cv 1482	. . . . . . . 8 class b
17	14, 9, 16	wral 2912	. . . . . . 7 wff A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) )
18	17, 4, 16	wral 2912	. . . . . 6 wff A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) )
19	18, 2, 16	wral 2912	. . . . 5 wff A. x e. b A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) )
20		vg	. . . . . . 7 setvar g
21	20	cv 1482	. . . . . 6 class g
22		cplusg 15941	. . . . . 6 class +g
23	21, 22	cfv 5888	. . . . 5 class ( +g ` g )
24	19, 6, 23	wsbc 3435	. . . 4 wff [. ( +g ` g ) / o ]. A. x e. b A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) )
25		cbs 15857	. . . . 5 class Base
26	21, 25	cfv 5888	. . . 4 class ( Base ` g )
27	24, 15, 26	wsbc 3435	. . 3 wff [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) )
28		cmgm 17240	. . 3 class Mgm
29	27, 20, 28	crab 2916	. 2 class { g e. Mgm | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) ) }
30	1, 29	wceq 1483	1 wff SGrp = { g e. Mgm | [. ( Base ` g ) / b ]. [. ( +g ` g ) / o ]. A. x e. b A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) ) }

This definition is referenced by:  issgrp  17285