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

Metamath Proof Explorer

Definition df-mgp

Description: Define a structure that puts the multiplication operation of a ring in the addition slot. Note that this will not actually be a group for the average ring, or even for a field, but it will be a monoid, and unitgrp shows that we get a group if we restrict to the elements that have inverses. This allows to formalize such notions as "the multiplication operation of a ring is a monoid" ( ringmgp ) or "the multiplicative identity" in terms of the identity of a monoid ( df-ur ). (Contributed by Mario Carneiro, 21-Dec-2014)

Ref Expression
Assertion df-mgp mulGrp = ( 𝑤 ∈ V ↦ ( 𝑤 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmgp ⊢ mulGrp
1 vw ⊢ 𝑤
2 cvv ⊢ V
3 1 cv ⊢ 𝑤
4 csts ⊢ sSet
5 cplusg ⊢ +g
6 cnx ⊢ ndx
7 6 5 cfv ⊢ ( +g ‘ ndx )
8 cmulr ⊢ .r
9 3 8 cfv ⊢ ( .r ‘ 𝑤 )
10 7 9 cop ⊢ ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩
11 3 10 4 co ⊢ ( 𝑤 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ )
12 1 2 11 cmpt ⊢ ( 𝑤 ∈ V ↦ ( 𝑤 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) )
13 0 12 wceq ⊢ mulGrp = ( 𝑤 ∈ V ↦ ( 𝑤 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) )