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	|- 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 ) >. ) )