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

Definition df-srng 17046
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  |  [. (
*rf `  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 17044 . 2  class  *Ring
2 vi . . . . . . 7  setvar  i
32cv 1369 . . . . . 6  class  i
4 vf . . . . . . . 8  setvar  f
54cv 1369 . . . . . . 7  class  f
6 coppr 16829 . . . . . . . 8  class oppr
75, 6cfv 5519 . . . . . . 7  class  (oppr `  f
)
8 crh 16919 . . . . . . 7  class RingHom
95, 7, 8co 6193 . . . . . 6  class  ( f RingHom 
(oppr `  f ) )
103, 9wcel 1758 . . . . 5  wff  i  e.  ( f RingHom  (oppr `  f
) )
113ccnv 4940 . . . . . 6  class  `' i
123, 11wceq 1370 . . . . 5  wff  i  =  `' i
1310, 12wa 369 . . . 4  wff  ( i  e.  ( f RingHom  (oppr `  f
) )  /\  i  =  `' i )
14 cstf 17043 . . . . 5  class  *rf
155, 14cfv 5519 . . . 4  class  ( *rf `  f
)
1613, 2, 15wsbc 3287 . . 3  wff  [. (
*rf `  f )  /  i ]. ( i  e.  ( f RingHom  (oppr
`  f ) )  /\  i  =  `' i )
1716, 4cab 2436 . 2  class  { f  |  [. ( *rf `  f
)  /  i ]. ( i  e.  ( f RingHom  (oppr
`  f ) )  /\  i  =  `' i ) }
181, 17wceq 1370 1  wff  *Ring  =  {
f  |  [. (
*rf `  f )  /  i ]. ( i  e.  ( f RingHom  (oppr
`  f ) )  /\  i  =  `' i ) }
Colors of variables: wff setvar class
This definition is referenced by:  issrng  17050
  Copyright terms: Public domain W3C validator