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	|- 1r = ( 0g o. mulGrp )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cur	|- 1r
1		c0g	|- 0g
2		cmgp	|- mulGrp
3	1 2	ccom	|- ( 0g o. mulGrp )
4	0 3	wceq	|- 1r = ( 0g o. mulGrp )