Definition df-srng 18846

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

Step	Hyp	Ref	Expression
1		csr 18844	. 2 class *Ring
2		vi	. . . . . . 7 setvar i
3	2	cv 1482	. . . . . 6 class i
4		vf	. . . . . . . 8 setvar f
5	4	cv 1482	. . . . . . 7 class f
6		coppr 18622	. . . . . . . 8 class oppr
7	5, 6	cfv 5888	. . . . . . 7 class (oppr ` f )
8		crh 18712	. . . . . . 7 class RingHom
9	5, 7, 8	co 6650	. . . . . 6 class ( f RingHom (oppr ` f ) )
10	3, 9	wcel 1990	. . . . 5 wff i e. ( f RingHom (oppr ` f ) )
11	3	ccnv 5113	. . . . . 6 class `' i
12	3, 11	wceq 1483	. . . . 5 wff i = `' i
13	10, 12	wa 384	. . . 4 wff ( i e. ( f RingHom (oppr ` f ) ) /\ i = `' i )
14		cstf 18843	. . . . 5 class *rf
15	5, 14	cfv 5888	. . . 4 class ( *rf ` f )
16	13, 2, 15	wsbc 3435	. . 3 wff [. ( *rf ` f ) / i ]. ( i e. ( f RingHom (oppr ` f ) ) /\ i = `' i )
17	16, 4	cab 2608	. 2 class { f | [. ( *rf ` f ) / i ]. ( i e. ( f RingHom (oppr ` f ) ) /\ i = `' i ) }
18	1, 17	wceq 1483	1 wff *Ring = { f | [. ( *rf ` f ) / i ]. ( i e. ( f RingHom (oppr ` f ) ) /\ i = `' i ) }

This definition is referenced by:  issrng  18850