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 18422
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 18421 . 2 class SRing
2 vf . . . . . . 7 setvar 𝑓
32cv 1479 . . . . . 6 class 𝑓
4 cmgp 18405 . . . . . 6 class mulGrp
53, 4cfv 5850 . . . . 5 class (mulGrp‘𝑓)
6 cmnd 17210 . . . . 5 class Mnd
75, 6wcel 1992 . . . 4 wff (mulGrp‘𝑓) ∈ Mnd
8 vx . . . . . . . . . . . . . . . 16 setvar 𝑥
98cv 1479 . . . . . . . . . . . . . . 15 class 𝑥
10 vy . . . . . . . . . . . . . . . . 17 setvar 𝑦
1110cv 1479 . . . . . . . . . . . . . . . 16 class 𝑦
12 vz . . . . . . . . . . . . . . . . 17 setvar 𝑧
1312cv 1479 . . . . . . . . . . . . . . . 16 class 𝑧
14 vp . . . . . . . . . . . . . . . . 17 setvar 𝑝
1514cv 1479 . . . . . . . . . . . . . . . 16 class 𝑝
1611, 13, 15co 6605 . . . . . . . . . . . . . . 15 class (𝑦𝑝𝑧)
17 vt . . . . . . . . . . . . . . . 16 setvar 𝑡
1817cv 1479 . . . . . . . . . . . . . . 15 class 𝑡
199, 16, 18co 6605 . . . . . . . . . . . . . 14 class (𝑥𝑡(𝑦𝑝𝑧))
209, 11, 18co 6605 . . . . . . . . . . . . . . 15 class (𝑥𝑡𝑦)
219, 13, 18co 6605 . . . . . . . . . . . . . . 15 class (𝑥𝑡𝑧)
2220, 21, 15co 6605 . . . . . . . . . . . . . 14 class ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
2319, 22wceq 1480 . . . . . . . . . . . . 13 wff (𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
249, 11, 15co 6605 . . . . . . . . . . . . . . 15 class (𝑥𝑝𝑦)
2524, 13, 18co 6605 . . . . . . . . . . . . . 14 class ((𝑥𝑝𝑦)𝑡𝑧)
2611, 13, 18co 6605 . . . . . . . . . . . . . . 15 class (𝑦𝑡𝑧)
2721, 26, 15co 6605 . . . . . . . . . . . . . 14 class ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
2825, 27wceq 1480 . . . . . . . . . . . . 13 wff ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
2923, 28wa 384 . . . . . . . . . . . 12 wff ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
30 vr . . . . . . . . . . . . 13 setvar 𝑟
3130cv 1479 . . . . . . . . . . . 12 class 𝑟
3229, 12, 31wral 2912 . . . . . . . . . . 11 wff 𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
3332, 10, 31wral 2912 . . . . . . . . . 10 wff 𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
34 vn . . . . . . . . . . . . . 14 setvar 𝑛
3534cv 1479 . . . . . . . . . . . . 13 class 𝑛
3635, 9, 18co 6605 . . . . . . . . . . . 12 class (𝑛𝑡𝑥)
3736, 35wceq 1480 . . . . . . . . . . 11 wff (𝑛𝑡𝑥) = 𝑛
389, 35, 18co 6605 . . . . . . . . . . . 12 class (𝑥𝑡𝑛)
3938, 35wceq 1480 . . . . . . . . . . 11 wff (𝑥𝑡𝑛) = 𝑛
4037, 39wa 384 . . . . . . . . . 10 wff ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)
4133, 40wa 384 . . . . . . . . 9 wff (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
4241, 8, 31wral 2912 . . . . . . . 8 wff 𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
43 c0g 16016 . . . . . . . . 9 class 0g
443, 43cfv 5850 . . . . . . . 8 class (0g𝑓)
4542, 34, 44wsbc 3422 . . . . . . 7 wff [(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
46 cmulr 15858 . . . . . . . 8 class .r
473, 46cfv 5850 . . . . . . 7 class (.r𝑓)
4845, 17, 47wsbc 3422 . . . . . 6 wff [(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
49 cplusg 15857 . . . . . . 7 class +g
503, 49cfv 5850 . . . . . 6 class (+g𝑓)
5148, 14, 50wsbc 3422 . . . . 5 wff [(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
52 cbs 15776 . . . . . 6 class Base
533, 52cfv 5850 . . . . 5 class (Base‘𝑓)
5451, 30, 53wsbc 3422 . . . 4 wff [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
557, 54wa 384 . . 3 wff ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))
56 ccmn 18109 . . 3 class CMnd
5755, 2, 56crab 2916 . 2 class {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
581, 57wceq 1480 1 wff SRing = {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
Colors of variables: wff setvar class
This definition is referenced by:  issrg  18423
  Copyright terms: Public domain W3C validator