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	$$⊢\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	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarw$$
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)$$