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

Definition df-srg 19187
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‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
Distinct variable group:   𝑓,𝑛,𝑝,𝑟,𝑡,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-srg
StepHypRef Expression
1 csrg 19186 . 2 class SRing
2 vf . . . . . . 7 setvar 𝑓
32cv 1527 . . . . . 6 class 𝑓
4 cmgp 19170 . . . . . 6 class mulGrp
53, 4cfv 6349 . . . . 5 class (mulGrp‘𝑓)
6 cmnd 17901 . . . . 5 class Mnd
75, 6wcel 2105 . . . 4 wff (mulGrp‘𝑓) ∈ Mnd
8 vx . . . . . . . . . . . . . . . 16 setvar 𝑥
98cv 1527 . . . . . . . . . . . . . . 15 class 𝑥
10 vy . . . . . . . . . . . . . . . . 17 setvar 𝑦
1110cv 1527 . . . . . . . . . . . . . . . 16 class 𝑦
12 vz . . . . . . . . . . . . . . . . 17 setvar 𝑧
1312cv 1527 . . . . . . . . . . . . . . . 16 class 𝑧
14 vp . . . . . . . . . . . . . . . . 17 setvar 𝑝
1514cv 1527 . . . . . . . . . . . . . . . 16 class 𝑝
1611, 13, 15co 7145 . . . . . . . . . . . . . . 15 class (𝑦𝑝𝑧)
17 vt . . . . . . . . . . . . . . . 16 setvar 𝑡
1817cv 1527 . . . . . . . . . . . . . . 15 class 𝑡
199, 16, 18co 7145 . . . . . . . . . . . . . 14 class (𝑥𝑡(𝑦𝑝𝑧))
209, 11, 18co 7145 . . . . . . . . . . . . . . 15 class (𝑥𝑡𝑦)
219, 13, 18co 7145 . . . . . . . . . . . . . . 15 class (𝑥𝑡𝑧)
2220, 21, 15co 7145 . . . . . . . . . . . . . 14 class ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
2319, 22wceq 1528 . . . . . . . . . . . . 13 wff (𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
249, 11, 15co 7145 . . . . . . . . . . . . . . 15 class (𝑥𝑝𝑦)
2524, 13, 18co 7145 . . . . . . . . . . . . . 14 class ((𝑥𝑝𝑦)𝑡𝑧)
2611, 13, 18co 7145 . . . . . . . . . . . . . . 15 class (𝑦𝑡𝑧)
2721, 26, 15co 7145 . . . . . . . . . . . . . 14 class ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
2825, 27wceq 1528 . . . . . . . . . . . . 13 wff ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
2923, 28wa 396 . . . . . . . . . . . 12 wff ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
30 vr . . . . . . . . . . . . 13 setvar 𝑟
3130cv 1527 . . . . . . . . . . . 12 class 𝑟
3229, 12, 31wral 3138 . . . . . . . . . . 11 wff 𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
3332, 10, 31wral 3138 . . . . . . . . . 10 wff 𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
34 vn . . . . . . . . . . . . . 14 setvar 𝑛
3534cv 1527 . . . . . . . . . . . . 13 class 𝑛
3635, 9, 18co 7145 . . . . . . . . . . . 12 class (𝑛𝑡𝑥)
3736, 35wceq 1528 . . . . . . . . . . 11 wff (𝑛𝑡𝑥) = 𝑛
389, 35, 18co 7145 . . . . . . . . . . . 12 class (𝑥𝑡𝑛)
3938, 35wceq 1528 . . . . . . . . . . 11 wff (𝑥𝑡𝑛) = 𝑛
4037, 39wa 396 . . . . . . . . . 10 wff ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)
4133, 40wa 396 . . . . . . . . 9 wff (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
4241, 8, 31wral 3138 . . . . . . . 8 wff 𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
43 c0g 16703 . . . . . . . . 9 class 0g
443, 43cfv 6349 . . . . . . . 8 class (0g𝑓)
4542, 34, 44wsbc 3771 . . . . . . 7 wff [(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
46 cmulr 16556 . . . . . . . 8 class .r
473, 46cfv 6349 . . . . . . 7 class (.r𝑓)
4845, 17, 47wsbc 3771 . . . . . 6 wff [(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
49 cplusg 16555 . . . . . . 7 class +g
503, 49cfv 6349 . . . . . 6 class (+g𝑓)
5148, 14, 50wsbc 3771 . . . . 5 wff [(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
52 cbs 16473 . . . . . 6 class Base
533, 52cfv 6349 . . . . 5 class (Base‘𝑓)
5451, 30, 53wsbc 3771 . . . 4 wff [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
557, 54wa 396 . . 3 wff ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))
56 ccmn 18837 . . 3 class CMnd
5755, 2, 56crab 3142 . 2 class {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
581, 57wceq 1528 1 wff SRing = {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
Colors of variables: wff setvar class
This definition is referenced by:  issrg  19188
  Copyright terms: Public domain W3C validator