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

Definition df-srng 15922
 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 RingHom oppr
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-srng
StepHypRef Expression
1 csr 15920 . 2
2 vi . . . . . . 7
32cv 1651 . . . . . 6
4 vf . . . . . . . 8
54cv 1651 . . . . . . 7
6 coppr 15715 . . . . . . . 8 oppr
75, 6cfv 5445 . . . . . . 7 oppr
8 crh 15805 . . . . . . 7 RingHom
95, 7, 8co 6072 . . . . . 6 RingHom oppr
103, 9wcel 1725 . . . . 5 RingHom oppr
113ccnv 4868 . . . . . 6
123, 11wceq 1652 . . . . 5
1310, 12wa 359 . . . 4 RingHom oppr
14 cstf 15919 . . . . 5
155, 14cfv 5445 . . . 4
1613, 2, 15wsbc 3153 . . 3 RingHom oppr
1716, 4cab 2421 . 2 RingHom oppr
181, 17wceq 1652 1 RingHom oppr
 Colors of variables: wff set class This definition is referenced by:  issrng  15926
 Copyright terms: Public domain W3C validator