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-ur ). (Contributed by Mario Carneiro, 21-Dec-2014)

Ref Expression
Assertion df-mgp mulGrp = w V w sSet + ndx w

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmgp class mulGrp
1 vw setvar w
2 cvv class V
3 1 cv setvar w
4 csts class sSet
5 cplusg class + 𝑔
6 cnx class ndx
7 6 5 cfv class + ndx
8 cmulr class 𝑟
9 3 8 cfv class w
10 7 9 cop class + ndx w
11 3 10 4 co class w sSet + ndx w
12 1 2 11 cmpt class w V w sSet + ndx w
13 0 12 wceq wff mulGrp = w V w sSet + ndx w