MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-unit Unicode version

Definition df-unit 15440
Description: Define the set of units in a ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
Assertion
Ref Expression
df-unit  |- Unit  =  ( w  e.  _V  |->  ( `' ( ( ||r `  w
)  i^i  ( ||r `  (oppr `  w
) ) ) " { ( 1r `  w ) } ) )

Detailed syntax breakdown of Definition df-unit
StepHypRef Expression
1 cui 15437 . 2  class Unit
2 vw . . 3  set  w
3 cvv 2801 . . 3  class  _V
42cv 1631 . . . . . . 7  class  w
5 cdsr 15436 . . . . . . 7  class  ||r
64, 5cfv 5271 . . . . . 6  class  ( ||r `  w
)
7 coppr 15420 . . . . . . . 8  class oppr
84, 7cfv 5271 . . . . . . 7  class  (oppr `  w
)
98, 5cfv 5271 . . . . . 6  class  ( ||r `  (oppr `  w
) )
106, 9cin 3164 . . . . 5  class  ( (
||r `  w )  i^i  ( ||r `  (oppr
`  w ) ) )
1110ccnv 4704 . . . 4  class  `' ( ( ||r `
 w )  i^i  ( ||r `
 (oppr
`  w ) ) )
12 cur 15355 . . . . . 6  class  1r
134, 12cfv 5271 . . . . 5  class  ( 1r
`  w )
1413csn 3653 . . . 4  class  { ( 1r `  w ) }
1511, 14cima 4708 . . 3  class  ( `' ( ( ||r `
 w )  i^i  ( ||r `
 (oppr
`  w ) ) ) " { ( 1r `  w ) } )
162, 3, 15cmpt 4093 . 2  class  ( w  e.  _V  |->  ( `' ( ( ||r `
 w )  i^i  ( ||r `
 (oppr
`  w ) ) ) " { ( 1r `  w ) } ) )
171, 16wceq 1632 1  wff Unit  =  ( w  e.  _V  |->  ( `' ( ( ||r `  w
)  i^i  ( ||r `  (oppr `  w
) ) ) " { ( 1r `  w ) } ) )
Colors of variables: wff set class
This definition is referenced by:  isunit  15455
  Copyright terms: Public domain W3C validator