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 = { 𝑔 ∈ Mgm ∣ [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g𝑔 ) / 𝑜 ]𝑥𝑏𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 csgrp Smgrp
1 vg 𝑔
2 cmgm Mgm
3 cbs Base
4 1 cv 𝑔
5 4 3 cfv ( Base ‘ 𝑔 )
6 vb 𝑏
7 cplusg +g
8 4 7 cfv ( +g𝑔 )
9 vo 𝑜
10 vx 𝑥
11 6 cv 𝑏
12 vy 𝑦
13 vz 𝑧
14 10 cv 𝑥
15 9 cv 𝑜
16 12 cv 𝑦
17 14 16 15 co ( 𝑥 𝑜 𝑦 )
18 13 cv 𝑧
19 17 18 15 co ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 )
20 16 18 15 co ( 𝑦 𝑜 𝑧 )
21 14 20 15 co ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) )
22 19 21 wceq ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) )
23 22 13 11 wral 𝑧𝑏 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) )
24 23 12 11 wral 𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) )
25 24 10 11 wral 𝑥𝑏𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) )
26 25 9 8 wsbc [ ( +g𝑔 ) / 𝑜 ]𝑥𝑏𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) )
27 26 6 5 wsbc [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g𝑔 ) / 𝑜 ]𝑥𝑏𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) )
28 27 1 2 crab { 𝑔 ∈ Mgm ∣ [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g𝑔 ) / 𝑜 ]𝑥𝑏𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) }
29 0 28 wceq Smgrp = { 𝑔 ∈ Mgm ∣ [ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g𝑔 ) / 𝑜 ]𝑥𝑏𝑦𝑏𝑧𝑏 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) }