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

Definition df-srg 17740
 Description: Define class of all semirings. A semiring is a set equipped with two everywhere-defined internal operations, whose first one is an additive commutative monoid structure and the second one is a multiplicative monoid structure, and where multiplication is (left- and right-) distributive over addition. Compared to the definition of a ring, this definition also adds that the additive identity is an absorbing element of the multiplicative law, as this cannot be deduced from distributivity alone. Definition of [Golan] p. 1. Note that our semirings are unital. Such semirings are sometimes called "rigs", being "rings without negatives". (Contributed by Thierry Arnoux, 21-Mar-2018.)
Assertion
Ref Expression
df-srg SRing CMnd mulGrp
Distinct variable group:   ,,,,,,,

Detailed syntax breakdown of Definition df-srg
StepHypRef Expression
1 csrg 17739 . 2 SRing
2 vf . . . . . . 7
32cv 1443 . . . . . 6
4 cmgp 17723 . . . . . 6 mulGrp
53, 4cfv 5582 . . . . 5 mulGrp
6 cmnd 16535 . . . . 5
75, 6wcel 1887 . . . 4 mulGrp
8 vx . . . . . . . . . . . . . . . 16
98cv 1443 . . . . . . . . . . . . . . 15
10 vy . . . . . . . . . . . . . . . . 17
1110cv 1443 . . . . . . . . . . . . . . . 16
12 vz . . . . . . . . . . . . . . . . 17
1312cv 1443 . . . . . . . . . . . . . . . 16
14 vp . . . . . . . . . . . . . . . . 17
1514cv 1443 . . . . . . . . . . . . . . . 16
1611, 13, 15co 6290 . . . . . . . . . . . . . . 15
17 vt . . . . . . . . . . . . . . . 16
1817cv 1443 . . . . . . . . . . . . . . 15
199, 16, 18co 6290 . . . . . . . . . . . . . 14
209, 11, 18co 6290 . . . . . . . . . . . . . . 15
219, 13, 18co 6290 . . . . . . . . . . . . . . 15
2220, 21, 15co 6290 . . . . . . . . . . . . . 14
2319, 22wceq 1444 . . . . . . . . . . . . 13
249, 11, 15co 6290 . . . . . . . . . . . . . . 15
2524, 13, 18co 6290 . . . . . . . . . . . . . 14
2611, 13, 18co 6290 . . . . . . . . . . . . . . 15
2721, 26, 15co 6290 . . . . . . . . . . . . . 14
2825, 27wceq 1444 . . . . . . . . . . . . 13
2923, 28wa 371 . . . . . . . . . . . 12
30 vr . . . . . . . . . . . . 13
3130cv 1443 . . . . . . . . . . . 12
3229, 12, 31wral 2737 . . . . . . . . . . 11
3332, 10, 31wral 2737 . . . . . . . . . 10
34 vn . . . . . . . . . . . . . 14
3534cv 1443 . . . . . . . . . . . . 13
3635, 9, 18co 6290 . . . . . . . . . . . 12
3736, 35wceq 1444 . . . . . . . . . . 11
389, 35, 18co 6290 . . . . . . . . . . . 12
3938, 35wceq 1444 . . . . . . . . . . 11
4037, 39wa 371 . . . . . . . . . 10
4133, 40wa 371 . . . . . . . . 9
4241, 8, 31wral 2737 . . . . . . . 8
43 c0g 15338 . . . . . . . . 9
443, 43cfv 5582 . . . . . . . 8
4542, 34, 44wsbc 3267 . . . . . . 7
46 cmulr 15191 . . . . . . . 8
473, 46cfv 5582 . . . . . . 7
4845, 17, 47wsbc 3267 . . . . . 6
49 cplusg 15190 . . . . . . 7
503, 49cfv 5582 . . . . . 6
5148, 14, 50wsbc 3267 . . . . 5
52 cbs 15121 . . . . . 6
533, 52cfv 5582 . . . . 5
5451, 30, 53wsbc 3267 . . . 4
557, 54wa 371 . . 3 mulGrp
56 ccmn 17430 . . 3 CMnd
5755, 2, 56crab 2741 . 2 CMnd mulGrp
581, 57wceq 1444 1 SRing CMnd mulGrp
 Colors of variables: wff setvar class This definition is referenced by:  issrg  17741
 Copyright terms: Public domain W3C validator