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 ‘ 𝑔 ) / 𝑜 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( ( 𝑥 𝑜 𝑦 ) 𝑜 𝑧 ) = ( 𝑥 𝑜 ( 𝑦 𝑜 𝑧 ) ) }