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 19729
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 19727 . 2 class *-Ring
2 vi . . . . . . 7 setvar 𝑖
32cv 1541 . . . . . 6 class 𝑖
4 vf . . . . . . . 8 setvar 𝑓
54cv 1541 . . . . . . 7 class 𝑓
6 coppr 19487 . . . . . . . 8 class oppr
75, 6cfv 6333 . . . . . . 7 class (oppr𝑓)
8 crh 19579 . . . . . . 7 class RingHom
95, 7, 8co 7164 . . . . . 6 class (𝑓 RingHom (oppr𝑓))
103, 9wcel 2113 . . . . 5 wff 𝑖 ∈ (𝑓 RingHom (oppr𝑓))
113ccnv 5518 . . . . . 6 class 𝑖
123, 11wceq 1542 . . . . 5 wff 𝑖 = 𝑖
1310, 12wa 399 . . . 4 wff (𝑖 ∈ (𝑓 RingHom (oppr𝑓)) ∧ 𝑖 = 𝑖)
14 cstf 19726 . . . . 5 class *rf
155, 14cfv 6333 . . . 4 class (*rf𝑓)
1613, 2, 15wsbc 3679 . . 3 wff [(*rf𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr𝑓)) ∧ 𝑖 = 𝑖)
1716, 4cab 2716 . 2 class {𝑓[(*rf𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr𝑓)) ∧ 𝑖 = 𝑖)}
181, 17wceq 1542 1 wff *-Ring = {𝑓[(*rf𝑓) / 𝑖](𝑖 ∈ (𝑓 RingHom (oppr𝑓)) ∧ 𝑖 = 𝑖)}
Colors of variables: wff setvar class
This definition is referenced by:  issrng  19733
  Copyright terms: Public domain W3C validator