Definition df-sgrp

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

	Ref	Expression
Assertion	df-sgrp	Could not format assertion : No typesetting found for |- Smgrp = { 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 ) ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csgrp	Could not format Smgrp : No typesetting found for class Smgrp with typecode class
1		vg	$$setvarg$$
2		cmgm	$$class\mathrm{Mgm}$$
3		cbs	$$class\mathrm{Base}$$
4	1	cv	$$setvarg$$
5	4 3	cfv	$$class{\mathrm{Base}}_g$$
6		vb	$$setvarb$$
7		cplusg	$$class{+}_{𝑔}$$
8	4 7	cfv	$$class{+}_g$$
9		vo	$$setvaro$$
10		vx	$$setvarx$$
11	6	cv	$$setvarb$$
12		vy	$$setvary$$
13		vz	$$setvarz$$
14	10	cv	$$setvarx$$
15	9	cv	$$setvaro$$
16	12	cv	$$setvary$$
17	14 16 15	co	$$class\left(xoy\right)$$
18	13	cv	$$setvarz$$
19	17 18 15	co	$$class\left(\left(xoy\right)oz\right)$$
20	16 18 15	co	$$class\left(yoz\right)$$
21	14 20 15	co	$$class\left(xo\left(yoz\right)\right)$$
22	19 21	wceq	$$wff\left(xoy\right)oz=xo\left(yoz\right)$$
23	22 13 11	wral	$$wff\forall z\in b\left(xoy\right)oz=xo\left(yoz\right)$$
24	23 12 11	wral	$$wff\forall y\in b\forall z\in b\left(xoy\right)oz=xo\left(yoz\right)$$
25	24 10 11	wral	$$wff\forall x\in b\forall y\in b\forall z\in b\left(xoy\right)oz=xo\left(yoz\right)$$
26	25 9 8	wsbc	$$wff\underset{\dot{}}{[}{+}_g/o\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in b\left(xoy\right)oz=xo\left(yoz\right)$$
27	26 6 5	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_g/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/o\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in b\left(xoy\right)oz=xo\left(yoz\right)$$
28	27 1 2	crab	$$class\left\{g\in \mathrm{Mgm}|\underset{\dot{}}{[}{\mathrm{Base}}_g/b\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/o\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in b\left(xoy\right)oz=xo\left(yoz\right)\right\}$$
29	0 28	wceq	Could not format Smgrp = { 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 ) ) } : No typesetting found for wff Smgrp = { 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 ) ) } with typecode wff