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

Definition df-srng 18611
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 18609 . 2 class *-Ring
2 vi . . . . . . 7 setvar 𝑖
32cv 1473 . . . . . 6 class 𝑖
4 vf . . . . . . . 8 setvar 𝑓
54cv 1473 . . . . . . 7 class 𝑓
6 coppr 18387 . . . . . . . 8 class oppr
75, 6cfv 5786 . . . . . . 7 class (oppr𝑓)
8 crh 18477 . . . . . . 7 class RingHom
95, 7, 8co 6523 . . . . . 6 class (𝑓 RingHom (oppr𝑓))
103, 9wcel 1975 . . . . 5 wff 𝑖 ∈ (𝑓 RingHom (oppr𝑓))
113ccnv 5023 . . . . . 6 class 𝑖
123, 11wceq 1474 . . . . 5 wff 𝑖 = 𝑖
1310, 12wa 382 . . . 4 wff (𝑖 ∈ (𝑓 RingHom (oppr𝑓)) ∧ 𝑖 = 𝑖)
14 cstf 18608 . . . . 5 class *rf
155, 14cfv 5786 . . . 4 class (*rf𝑓)
1613, 2, 15wsbc 3397 . . 3 wff [(*rf𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr𝑓)) ∧ 𝑖 = 𝑖)
1716, 4cab 2591 . 2 class {𝑓[(*rf𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr𝑓)) ∧ 𝑖 = 𝑖)}
181, 17wceq 1474 1 wff *-Ring = {𝑓[(*rf𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr𝑓)) ∧ 𝑖 = 𝑖)}
Colors of variables: wff setvar class
This definition is referenced by:  issrng  18615
  Copyright terms: Public domain W3C validator