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

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