Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-srng Structured version   Visualization version   GIF version

Definition df-srng 18669
 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
StepHypRef Expression
1 csr 18667 . 2 class *-Ring
2 vi . . . . . . 7 setvar 𝑖
32cv 1474 . . . . . 6 class 𝑖
4 vf . . . . . . . 8 setvar 𝑓
54cv 1474 . . . . . . 7 class 𝑓
6 coppr 18445 . . . . . . . 8 class oppr
75, 6cfv 5804 . . . . . . 7 class (oppr𝑓)
8 crh 18535 . . . . . . 7 class RingHom
95, 7, 8co 6549 . . . . . 6 class (𝑓 RingHom (oppr𝑓))
103, 9wcel 1977 . . . . 5 wff 𝑖 ∈ (𝑓 RingHom (oppr𝑓))
113ccnv 5037 . . . . . 6 class 𝑖
123, 11wceq 1475 . . . . 5 wff 𝑖 = 𝑖
1310, 12wa 383 . . . 4 wff (𝑖 ∈ (𝑓 RingHom (oppr𝑓)) ∧ 𝑖 = 𝑖)
14 cstf 18666 . . . . 5 class *rf
155, 14cfv 5804 . . . 4 class (*rf𝑓)
1613, 2, 15wsbc 3402 . . 3 wff [(*rf𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr𝑓)) ∧ 𝑖 = 𝑖)
1716, 4cab 2596 . 2 class {𝑓[(*rf𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr𝑓)) ∧ 𝑖 = 𝑖)}
181, 17wceq 1475 1 wff *-Ring = {𝑓[(*rf𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr𝑓)) ∧ 𝑖 = 𝑖)}
 Colors of variables: wff setvar class This definition is referenced by:  issrng  18673
 Copyright terms: Public domain W3C validator