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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csr	⊢ *-Ring
1		vf	⊢ 𝑓
2		cstf	⊢ *rf
3	1	cv	⊢ 𝑓
4	3 2	cfv	⊢ ( *rf ‘ 𝑓 )
5		vi	⊢ 𝑖
6	5	cv	⊢ 𝑖
7		crh	⊢ RingHom
8		coppr	⊢ oppr
9	3 8	cfv	⊢ ( oppr ‘ 𝑓 )
10	3 9 7	co	⊢ ( 𝑓 RingHom ( oppr ‘ 𝑓 ) )
11	6 10	wcel	⊢ 𝑖 ∈ ( 𝑓 RingHom ( oppr ‘ 𝑓 ) )
12	6	ccnv	⊢ ◡ 𝑖
13	6 12	wceq	⊢ 𝑖 = ◡ 𝑖
14	11 13	wa	⊢ ( 𝑖 ∈ ( 𝑓 RingHom ( oppr ‘ 𝑓 ) ) ∧ 𝑖 = ◡ 𝑖 )
15	14 5 4	wsbc	⊢ [ ( *rf ‘ 𝑓 ) / 𝑖 ] ( 𝑖 ∈ ( 𝑓 RingHom ( oppr ‘ 𝑓 ) ) ∧ 𝑖 = ◡ 𝑖 )
16	15 1	cab	⊢ { 𝑓 ∣ [ ( *rf ‘ 𝑓 ) / 𝑖 ] ( 𝑖 ∈ ( 𝑓 RingHom ( oppr ‘ 𝑓 ) ) ∧ 𝑖 = ◡ 𝑖 ) }
17	0 16	wceq	⊢ *-Ring = { 𝑓 ∣ [ ( *rf ‘ 𝑓 ) / 𝑖 ] ( 𝑖 ∈ ( 𝑓 RingHom ( oppr ‘ 𝑓 ) ) ∧ 𝑖 = ◡ 𝑖 ) }