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 e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmgp
 |-  mulGrp
1 vw
 |-  w
2 cvv
 |-  _V
3 1 cv
 |-  w
4 csts
 |-  sSet
5 cplusg
 |-  +g
6 cnx
 |-  ndx
7 6 5 cfv
 |-  ( +g ` ndx )
8 cmulr
 |-  .r
9 3 8 cfv
 |-  ( .r ` w )
10 7 9 cop
 |-  <. ( +g ` ndx ) , ( .r ` w ) >.
11 3 10 4 co
 |-  ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. )
12 1 2 11 cmpt
 |-  ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )
13 0 12 wceq
 |-  mulGrp = ( w e. _V |-> ( w sSet <. ( +g ` ndx ) , ( .r ` w ) >. ) )