This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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