ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-srg GIF version

Definition df-srg 13158
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, 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 13157 . 2 class SRing
2 vf . . . . . . 7 setvar 𝑓
32cv 1352 . . . . . 6 class 𝑓
4 cmgp 13141 . . . . . 6 class mulGrp
53, 4cfv 5218 . . . . 5 class (mulGrp‘𝑓)
6 cmnd 12824 . . . . 5 class Mnd
75, 6wcel 2148 . . . 4 wff (mulGrp‘𝑓) ∈ Mnd
8 vx . . . . . . . . . . . . . . . 16 setvar 𝑥
98cv 1352 . . . . . . . . . . . . . . 15 class 𝑥
10 vy . . . . . . . . . . . . . . . . 17 setvar 𝑦
1110cv 1352 . . . . . . . . . . . . . . . 16 class 𝑦
12 vz . . . . . . . . . . . . . . . . 17 setvar 𝑧
1312cv 1352 . . . . . . . . . . . . . . . 16 class 𝑧
14 vp . . . . . . . . . . . . . . . . 17 setvar 𝑝
1514cv 1352 . . . . . . . . . . . . . . . 16 class 𝑝
1611, 13, 15co 5878 . . . . . . . . . . . . . . 15 class (𝑦𝑝𝑧)
17 vt . . . . . . . . . . . . . . . 16 setvar 𝑡
1817cv 1352 . . . . . . . . . . . . . . 15 class 𝑡
199, 16, 18co 5878 . . . . . . . . . . . . . 14 class (𝑥𝑡(𝑦𝑝𝑧))
209, 11, 18co 5878 . . . . . . . . . . . . . . 15 class (𝑥𝑡𝑦)
219, 13, 18co 5878 . . . . . . . . . . . . . . 15 class (𝑥𝑡𝑧)
2220, 21, 15co 5878 . . . . . . . . . . . . . 14 class ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
2319, 22wceq 1353 . . . . . . . . . . . . 13 wff (𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧))
249, 11, 15co 5878 . . . . . . . . . . . . . . 15 class (𝑥𝑝𝑦)
2524, 13, 18co 5878 . . . . . . . . . . . . . 14 class ((𝑥𝑝𝑦)𝑡𝑧)
2611, 13, 18co 5878 . . . . . . . . . . . . . . 15 class (𝑦𝑡𝑧)
2721, 26, 15co 5878 . . . . . . . . . . . . . 14 class ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
2825, 27wceq 1353 . . . . . . . . . . . . 13 wff ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))
2923, 28wa 104 . . . . . . . . . . . 12 wff ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
30 vr . . . . . . . . . . . . 13 setvar 𝑟
3130cv 1352 . . . . . . . . . . . 12 class 𝑟
3229, 12, 31wral 2455 . . . . . . . . . . 11 wff 𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
3332, 10, 31wral 2455 . . . . . . . . . 10 wff 𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧)))
34 vn . . . . . . . . . . . . . 14 setvar 𝑛
3534cv 1352 . . . . . . . . . . . . 13 class 𝑛
3635, 9, 18co 5878 . . . . . . . . . . . 12 class (𝑛𝑡𝑥)
3736, 35wceq 1353 . . . . . . . . . . 11 wff (𝑛𝑡𝑥) = 𝑛
389, 35, 18co 5878 . . . . . . . . . . . 12 class (𝑥𝑡𝑛)
3938, 35wceq 1353 . . . . . . . . . . 11 wff (𝑥𝑡𝑛) = 𝑛
4037, 39wa 104 . . . . . . . . . 10 wff ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)
4133, 40wa 104 . . . . . . . . 9 wff (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
4241, 8, 31wral 2455 . . . . . . . 8 wff 𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
43 c0g 12711 . . . . . . . . 9 class 0g
443, 43cfv 5218 . . . . . . . 8 class (0g𝑓)
4542, 34, 44wsbc 2964 . . . . . . 7 wff [(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
46 cmulr 12540 . . . . . . . 8 class .r
473, 46cfv 5218 . . . . . . 7 class (.r𝑓)
4845, 17, 47wsbc 2964 . . . . . 6 wff [(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
49 cplusg 12539 . . . . . . 7 class +g
503, 49cfv 5218 . . . . . 6 class (+g𝑓)
5148, 14, 50wsbc 2964 . . . . 5 wff [(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
52 cbs 12465 . . . . . 6 class Base
533, 52cfv 5218 . . . . 5 class (Base‘𝑓)
5451, 30, 53wsbc 2964 . . . 4 wff [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛))
557, 54wa 104 . . 3 wff ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))
56 ccmn 13099 . . 3 class CMnd
5755, 2, 56crab 2459 . 2 class {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
581, 57wceq 1353 1 wff SRing = {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g𝑓) / 𝑝][(.r𝑓) / 𝑡][(0g𝑓) / 𝑛]𝑥𝑟 (∀𝑦𝑟𝑧𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))}
Colors of variables: wff set class
This definition is referenced by:  issrg  13159
  Copyright terms: Public domain W3C validator