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