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 ∈ Mgm | [˙Base g / b]˙ [˙+ g / o]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x o y o z = x o y o z

Detailed syntax breakdown

Step Hyp Ref Expression
0 csgrp class Smgrp
1 vg setvar g
2 cmgm class Mgm
3 cbs class Base
4 1 cv setvar g
5 4 3 cfv class Base g
6 vb setvar b
7 cplusg class + 𝑔
8 4 7 cfv class + g
9 vo setvar o
10 vx setvar x
11 6 cv setvar b
12 vy setvar y
13 vz setvar z
14 10 cv setvar x
15 9 cv setvar o
16 12 cv setvar y
17 14 16 15 co class x o y
18 13 cv setvar z
19 17 18 15 co class x o y o z
20 16 18 15 co class y o z
21 14 20 15 co class x o y o z
22 19 21 wceq wff x o y o z = x o y o z
23 22 13 11 wral wff ∀ z ∈ b x o y o z = x o y o z
24 23 12 11 wral wff ∀ y ∈ b ∀ z ∈ b x o y o z = x o y o z
25 24 10 11 wral wff ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x o y o z = x o y o z
26 25 9 8 wsbc wff [˙+ g / o]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x o y o z = x o y o z
27 26 6 5 wsbc wff [˙Base g / b]˙ [˙+ g / o]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x o y o z = x o y o z
28 27 1 2 crab class g ∈ Mgm | [˙Base g / b]˙ [˙+ g / o]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x o y o z = x o y o z
29 0 28 wceq wff Smgrp = g ∈ Mgm | [˙Base g / b]˙ [˙+ g / o]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x o y o z = x o y o z