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

Definition df-srng 15446
Description: Define class of all star rings. A star ring is a ring with an involution (conjugation) function. Involution (unlike say the ring zero) is not unique and therefore must be added as a new component to the ring. For example, two possible involutions for complex numbers are the identity function and complex conjugation. Definition of involution in [Holland95] p. 204. (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2015.)
Assertion
Ref Expression
df-srng  |-  *Ring  =  {
f  |  [. (
* r f `  f )  /  i ]. ( i  e.  ( f RingHom  (oppr
`  f ) )  /\  i  =  `' i ) }
Distinct variable group:    f, i

Detailed syntax breakdown of Definition df-srng
StepHypRef Expression
1 csr 15444 . 2  class  *Ring
2 vi . . . . . . 7  set  i
32cv 1618 . . . . . 6  class  i
4 vf . . . . . . . 8  set  f
54cv 1618 . . . . . . 7  class  f
6 coppr 15239 . . . . . . . 8  class oppr
75, 6cfv 4592 . . . . . . 7  class  (oppr `  f
)
8 crh 15329 . . . . . . 7  class RingHom
95, 7, 8co 5710 . . . . . 6  class  ( f RingHom 
(oppr `  f ) )
103, 9wcel 1621 . . . . 5  wff  i  e.  ( f RingHom  (oppr `  f
) )
113ccnv 4579 . . . . . 6  class  `' i
123, 11wceq 1619 . . . . 5  wff  i  =  `' i
1310, 12wa 360 . . . 4  wff  ( i  e.  ( f RingHom  (oppr `  f
) )  /\  i  =  `' i )
14 cstf 15443 . . . . 5  class  * r f
155, 14cfv 4592 . . . 4  class  ( * r f `  f
)
1613, 2, 15wsbc 2921 . . 3  wff  [. (
* r f `  f )  /  i ]. ( i  e.  ( f RingHom  (oppr
`  f ) )  /\  i  =  `' i )
1716, 4cab 2239 . 2  class  { f  |  [. ( * r f `  f
)  /  i ]. ( i  e.  ( f RingHom  (oppr
`  f ) )  /\  i  =  `' i ) }
181, 17wceq 1619 1  wff  *Ring  =  {
f  |  [. (
* r f `  f )  /  i ]. ( i  e.  ( f RingHom  (oppr
`  f ) )  /\  i  =  `' i ) }
Colors of variables: wff set class
This definition is referenced by:  issrng  15450
  Copyright terms: Public domain W3C validator