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 20077
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. Like with rings (df-ring 20125), the additive identity is an absorbing element of the multiplicative law, but in the case of semirings, this has to be part of the definition, as it 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 20076 . 2 class SRing
2 vf . . . . . . 7 setvar 𝑓
32cv 1532 . . . . . 6 class 𝑓
4 cmgp 20024 . . . . . 6 class mulGrp
53, 4cfv 6533 . . . . 5 class (mulGrp‘𝑓)
6 cmnd 18654 . . . . 5 class Mnd
75, 6wcel 2098 . . . 4 wff (mulGrp‘𝑓) ∈ Mnd
8 vx . . . . . . . . . . . . . . . 16 setvar 𝑥
98cv 1532 . . . . . . . . . . . . . . 15 class 𝑥
10 vy . . . . . . . . . . . . . . . . 17 setvar 𝑦
1110cv 1532 . . . . . . . . . . . . . . . 16 class 𝑦
12 vz . . . . . . . . . . . . . . . . 17 setvar 𝑧
1312cv 1532 . . . . . . . . . . . . . . . 16 class 𝑧
14 vp . . . . . . . . . . . . . . . . 17 setvar 𝑝
1514cv 1532 . . . . . . . . . . . . . . . 16 class 𝑝
1611, 13, 15co 7401 . . . . . . . . . . . . . . 15 class (𝑦𝑝𝑧)
17 vt . . . . . . . . . . . . . . . 16 setvar 𝑡
1817cv 1532 . . . . . . . . . . . . . . 15 class 𝑡
199, 16, 18co 7401 . . . . . . . . . . . . . 14 class (𝑥𝑡(𝑦𝑝𝑧))
209, 11, 18co 7401 . . . . . . . . . . . . . . 15 class (𝑥𝑡𝑦)
219, 13, 18co 7401 . . . . . . . . . . . . . . 15 class (𝑥𝑡𝑧)
2220, 21, 15co 7401 . . . . . . . . . . . . . 14 class ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
2319, 22wceq 1533 . . . . . . . . . . . . 13 wff (𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
249, 11, 15co 7401 . . . . . . . . . . . . . . 15 class (𝑥𝑝𝑦)
2524, 13, 18co 7401 . . . . . . . . . . . . . 14 class ((𝑥𝑝𝑦)𝑡𝑧)
2611, 13, 18co 7401 . . . . . . . . . . . . . . 15 class (𝑦𝑡𝑧)
2721, 26, 15co 7401 . . . . . . . . . . . . . 14 class ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
2825, 27wceq 1533 . . . . . . . . . . . . 13 wff ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
2923, 28wa 395 . . . . . . . . . . . 12 wff ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
30 vr . . . . . . . . . . . . 13 setvar 𝑟
3130cv 1532 . . . . . . . . . . . 12 class 𝑟
3229, 12, 31wral 3053 . . . . . . . . . . 11 wff 𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
3332, 10, 31wral 3053 . . . . . . . . . 10 wff 𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
34 vn . . . . . . . . . . . . . 14 setvar 𝑛
3534cv 1532 . . . . . . . . . . . . 13 class 𝑛
3635, 9, 18co 7401 . . . . . . . . . . . 12 class (𝑛𝑡𝑥)
3736, 35wceq 1533 . . . . . . . . . . 11 wff (𝑛𝑡𝑥) = 𝑛
389, 35, 18co 7401 . . . . . . . . . . . 12 class (𝑥𝑡𝑛)
3938, 35wceq 1533 . . . . . . . . . . 11 wff (𝑥𝑡𝑛) = 𝑛
4037, 39wa 395 . . . . . . . . . 10 wff ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)
4133, 40wa 395 . . . . . . . . 9 wff (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
4241, 8, 31wral 3053 . . . . . . . 8 wff 𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
43 c0g 17381 . . . . . . . . 9 class 0g
443, 43cfv 6533 . . . . . . . 8 class (0g𝑓)
4542, 34, 44wsbc 3769 . . . . . . 7 wff [(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
46 cmulr 17194 . . . . . . . 8 class .r
473, 46cfv 6533 . . . . . . 7 class (.r𝑓)
4845, 17, 47wsbc 3769 . . . . . 6 wff [(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
49 cplusg 17193 . . . . . . 7 class +g
503, 49cfv 6533 . . . . . 6 class (+g𝑓)
5148, 14, 50wsbc 3769 . . . . 5 wff [(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
52 cbs 17140 . . . . . 6 class Base
533, 52cfv 6533 . . . . 5 class (Base‘𝑓)
5451, 30, 53wsbc 3769 . . . 4 wff [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
557, 54wa 395 . . 3 wff ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))
56 ccmn 19685 . . 3 class CMnd
5755, 2, 56crab 3424 . 2 class {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
581, 57wceq 1533 1 wff SRing = {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
Colors of variables: wff setvar class
This definition is referenced by:  issrg  20078
  Copyright terms: Public domain W3C validator