Definition df-unit

Description: Define the set of units in a ring, that is, all elements with a left and right multiplicative inverse. (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Assertion	df-unit	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` ( oppR ` w ) ) ) " { ( 1r ` w ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cui	|- Unit
1		vw	|- w
2		cvv	|- _V
3		cdsr	|- ||r
4	1	cv	|- w
5	4 3	cfv	|- ( ||r ` w )
6		coppr	|- oppR
7	4 6	cfv	|- ( oppR ` w )
8	7 3	cfv	|- ( ||r ` ( oppR ` w ) )
9	5 8	cin	|- ( ( ||r ` w ) i^i ( ||r ` ( oppR ` w ) ) )
10	9	ccnv	|- `' ( ( ||r ` w ) i^i ( ||r ` ( oppR ` w ) ) )
11		cur	|- 1r
12	4 11	cfv	|- ( 1r ` w )
13	12	csn	|- { ( 1r ` w ) }
14	10 13	cima	|- ( `' ( ( ||r ` w ) i^i ( ||r ` ( oppR ` w ) ) ) " { ( 1r ` w ) } )
15	1 2 14	cmpt	|- ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` ( oppR ` w ) ) ) " { ( 1r ` w ) } ) )
16	0 15	wceq	|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` ( oppR ` w ) ) ) " { ( 1r ` w ) } ) )