# 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 us 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-1r ). (Contributed by Mario Carneiro, 21-Dec-2014)

Ref Expression
Assertion df-mgp ${⊢}\mathrm{mulGrp}=\left({w}\in \mathrm{V}⟼{w}\mathrm{sSet}⟨{+}_{\mathrm{ndx}},{\cdot }_{{w}}⟩\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cmgp ${class}\mathrm{mulGrp}$
1 vw ${setvar}{w}$
2 cvv ${class}\mathrm{V}$
3 1 cv ${setvar}{w}$
4 csts ${class}\mathrm{sSet}$
5 cplusg ${class}{+}_{𝑔}$
6 cnx ${class}\mathrm{ndx}$
7 6 5 cfv ${class}{+}_{\mathrm{ndx}}$
8 cmulr ${class}{\cdot }_{𝑟}$
9 3 8 cfv ${class}{\cdot }_{{w}}$
10 7 9 cop ${class}⟨{+}_{\mathrm{ndx}},{\cdot }_{{w}}⟩$
11 3 10 4 co ${class}\left({w}\mathrm{sSet}⟨{+}_{\mathrm{ndx}},{\cdot }_{{w}}⟩\right)$
12 1 2 11 cmpt ${class}\left({w}\in \mathrm{V}⟼{w}\mathrm{sSet}⟨{+}_{\mathrm{ndx}},{\cdot }_{{w}}⟩\right)$
13 0 12 wceq ${wff}\mathrm{mulGrp}=\left({w}\in \mathrm{V}⟼{w}\mathrm{sSet}⟨{+}_{\mathrm{ndx}},{\cdot }_{{w}}⟩\right)$