Metamath Proof Explorer

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 
|- 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 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 csgrp 
 |-  Smgrp
1 vg 
 |-  g
2 cmgm 
 |-  Mgm
3 cbs 
 |-  Base
4 1 cv 
 |-  g
5 4 3 cfv 
 |-  ( Base ` g )
6 vb 
 |-  b
7 cplusg 
 |-  +g
8 4 7 cfv 
 |-  ( +g ` g )
9 vo 
 |-  o
10 vx 
 |-  x
11 6 cv 
 |-  b
12 vy 
 |-  y
13 vz 
 |-  z
14 10 cv 
 |-  x
15 9 cv 
 |-  o
16 12 cv 
 |-  y
17 14 16 15 co 
 |-  ( x o y )
18 13 cv 
 |-  z
19 17 18 15 co 
 |-  ( ( x o y ) o z )
20 16 18 15 co 
 |-  ( y o z )
21 14 20 15 co 
 |-  ( x o ( y o z ) )
22 19 21 wceq 
 |-  ( ( x o y ) o z ) = ( x o ( y o z ) )
23 22 13 11 wral 
 |-  A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) )
24 23 12 11 wral 
 |-  A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) )
25 24 10 11 wral 
 |-  A. x e. b A. y e. b A. z e. b ( ( x o y ) o z ) = ( x o ( y o z ) )
26 25 9 8 wsbc 
 |-  [. ( +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 ) )
27 26 6 5 wsbc 
 |-  [. ( 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 27 1 2 crab 
 |-  { 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 ) ) }
29 0 28 wceq 
 |-  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 ) ) }