Definition df-ur

Description: Define the multiplicative neutral element of a ring. This definition works by extracting the 0g element, i.e. the neutral element in a group or monoid, and transferring it to the multiplicative monoid via the mulGrp function ( df-mgp ). See also dfur2 , which derives the "traditional" definition as the unique element of a ring which is left- and right-neutral under multiplication. (Contributed by NM, 27-Aug-2011) (Revised by Mario Carneiro, 27-Dec-2014)

	Ref	Expression
Assertion	df-ur	$$⊢1_r=0_{𝑔}\circ \mathrm{mulGrp}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cur	$$class{1}_r$$
1		c0g	$$class{0}_{𝑔}$$
2		cmgp	$$class\mathrm{mulGrp}$$
3	1 2	ccom	$$class\left(0_{𝑔}\circ \mathrm{mulGrp}\right)$$
4	0 3	wceq	$$wff{1}_r=0_{𝑔}\circ \mathrm{mulGrp}$$