Metamath Proof Explorer


Definition df-srng

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)

Ref Expression
Assertion df-srng
|- *Ring = { f | [. ( *rf ` f ) / i ]. ( i e. ( f RingHom ( oppR ` f ) ) /\ i = `' i ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 csr
 |-  *Ring
1 vf
 |-  f
2 cstf
 |-  *rf
3 1 cv
 |-  f
4 3 2 cfv
 |-  ( *rf ` f )
5 vi
 |-  i
6 5 cv
 |-  i
7 crh
 |-  RingHom
8 coppr
 |-  oppR
9 3 8 cfv
 |-  ( oppR ` f )
10 3 9 7 co
 |-  ( f RingHom ( oppR ` f ) )
11 6 10 wcel
 |-  i e. ( f RingHom ( oppR ` f ) )
12 6 ccnv
 |-  `' i
13 6 12 wceq
 |-  i = `' i
14 11 13 wa
 |-  ( i e. ( f RingHom ( oppR ` f ) ) /\ i = `' i )
15 14 5 4 wsbc
 |-  [. ( *rf ` f ) / i ]. ( i e. ( f RingHom ( oppR ` f ) ) /\ i = `' i )
16 15 1 cab
 |-  { f | [. ( *rf ` f ) / i ]. ( i e. ( f RingHom ( oppR ` f ) ) /\ i = `' i ) }
17 0 16 wceq
 |-  *Ring = { f | [. ( *rf ` f ) / i ]. ( i e. ( f RingHom ( oppR ` f ) ) /\ i = `' i ) }