# Metamath Proof Explorer

## Definition df-mgm

Description: Amagma is a set equipped with an everywhere defined internal operation. Definition 1 in BourbakiAlg1 p. 1, or definition of a groupoid in section I.1 of Bruck p. 1. Note: The term "groupoid" is now widely used to refer to other objects: (small) categories all of whose morphisms are invertible, or groups with a partial function replacing the binary operation. Therefore, we will only use the term "magma" for the present notion in set.mm. (Contributed by FL, 2-Nov-2009) (Revised by AV, 6-Jan-2020)

Ref Expression
Assertion df-mgm Mgm = { 𝑔[ ( Base ‘ 𝑔 ) / 𝑏 ] [ ( +g𝑔 ) / 𝑜 ]𝑥𝑏𝑦𝑏 ( 𝑥 𝑜 𝑦 ) ∈ 𝑏 }

### Detailed syntax breakdown

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