This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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