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, 22Sep2011) (Revised by Mario Carneiro, 6Oct2015)
Ref  Expression  

Assertion  dfsrng   *Ring = { f  [. ( *rf ` f ) / i ]. ( i e. ( f RingHom ( oppR ` f ) ) /\ i = `' i ) } 
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 ) } 