Definition df-srng 20446

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 = {𝑓 ∣ [(*rf‘𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr‘𝑓)) ∧ 𝑖 = ◡𝑖)}

Distinct variable group:   𝑓,𝑖

Detailed syntax breakdown of Definition df-srng

Step	Hyp	Ref	Expression
1		csr 20444	. 2 class *-Ring
2		vi	. . . . . . 7 setvar 𝑖
3	2	cv 1540	. . . . . 6 class 𝑖
4		vf	. . . . . . . 8 setvar 𝑓
5	4	cv 1540	. . . . . . 7 class 𝑓
6		coppr 20141	. . . . . . . 8 class oppr
7	5, 6	cfv 6540	. . . . . . 7 class (oppr‘𝑓)
8		crh 20240	. . . . . . 7 class RingHom
9	5, 7, 8	co 7405	. . . . . 6 class (𝑓 RingHom (oppr‘𝑓))
10	3, 9	wcel 2106	. . . . 5 wff 𝑖 ∈ (𝑓 RingHom (oppr‘𝑓))
11	3	ccnv 5674	. . . . . 6 class ◡𝑖
12	3, 11	wceq 1541	. . . . 5 wff 𝑖 = ◡𝑖
13	10, 12	wa 396	. . . 4 wff (𝑖 ∈ (𝑓 RingHom (oppr‘𝑓)) ∧ 𝑖 = ◡𝑖)
14		cstf 20443	. . . . 5 class *rf
15	5, 14	cfv 6540	. . . 4 class (*rf‘𝑓)
16	13, 2, 15	wsbc 3776	. . 3 wff [(*rf‘𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr‘𝑓)) ∧ 𝑖 = ◡𝑖)
17	16, 4	cab 2709	. 2 class {𝑓 ∣ [(*rf‘𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr‘𝑓)) ∧ 𝑖 = ◡𝑖)}
18	1, 17	wceq 1541	1 wff *-Ring = {𝑓 ∣ [(*rf‘𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr‘𝑓)) ∧ 𝑖 = ◡𝑖)}

This definition is referenced by:  issrng  20450