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

Definition df-unit 15735
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 15732 . 2  class Unit
2 vw . . 3  set  w
3 cvv 2948 . . 3  class  _V
42cv 1651 . . . . . . 7  class  w
5 cdsr 15731 . . . . . . 7  class  ||r
64, 5cfv 5445 . . . . . 6  class  ( ||r `  w
)
7 coppr 15715 . . . . . . . 8  class oppr
84, 7cfv 5445 . . . . . . 7  class  (oppr `  w
)
98, 5cfv 5445 . . . . . 6  class  ( ||r `  (oppr `  w
) )
106, 9cin 3311 . . . . 5  class  ( (
||r `  w )  i^i  ( ||r `  (oppr
`  w ) ) )
1110ccnv 4868 . . . 4  class  `' ( ( ||r `
 w )  i^i  ( ||r `
 (oppr
`  w ) ) )
12 cur 15650 . . . . . 6  class  1r
134, 12cfv 5445 . . . . 5  class  ( 1r
`  w )
1413csn 3806 . . . 4  class  { ( 1r `  w ) }
1511, 14cima 4872 . . 3  class  ( `' ( ( ||r `
 w )  i^i  ( ||r `
 (oppr
`  w ) ) ) " { ( 1r `  w ) } )
162, 3, 15cmpt 4258 . 2  class  ( w  e.  _V  |->  ( `' ( ( ||r `
 w )  i^i  ( ||r `
 (oppr
`  w ) ) ) " { ( 1r `  w ) } ) )
171, 16wceq 1652 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  15750
  Copyright terms: Public domain W3C validator