Metamath Proof Explorer

Definition df-srg

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 ), 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)

Ref Expression
Assertion df-srg ⊢ SRing = f ∈ CMnd | mulGrp f ∈ Mnd ∧ [˙Base f / r]˙ [˙+ f / p]˙ [˙⋅ f / t]˙ [˙0 f / n]˙ ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z ∧ n t x = n ∧ x t n = n

Detailed syntax breakdown

Step Hyp Ref Expression
0 csrg class SRing
1 vf setvar f
2 ccmn class CMnd
3 cmgp class mulGrp
4 1 cv setvar f
5 4 3 cfv class mulGrp f
6 cmnd class Mnd
7 5 6 wcel wff mulGrp f ∈ Mnd
8 cbs class Base
9 4 8 cfv class Base f
10 vr setvar r
11 cplusg class + 𝑔
12 4 11 cfv class + f
13 vp setvar p
14 cmulr class ⋅ 𝑟
15 4 14 cfv class ⋅ f
16 vt setvar t
17 c0g class 0 𝑔
18 4 17 cfv class 0 f
19 vn setvar n
20 vx setvar x
21 10 cv setvar r
22 vy setvar y
23 vz setvar z
24 20 cv setvar x
25 16 cv setvar t
26 22 cv setvar y
27 13 cv setvar p
28 23 cv setvar z
29 26 28 27 co class y p z
30 24 29 25 co class x t y p z
31 24 26 25 co class x t y
32 24 28 25 co class x t z
33 31 32 27 co class x t y p x t z
34 30 33 wceq wff x t y p z = x t y p x t z
35 24 26 27 co class x p y
36 35 28 25 co class x p y t z
37 26 28 25 co class y t z
38 32 37 27 co class x t z p y t z
39 36 38 wceq wff x p y t z = x t z p y t z
40 34 39 wa wff x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
41 40 23 21 wral wff ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
42 41 22 21 wral wff ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
43 19 cv setvar n
44 43 24 25 co class n t x
45 44 43 wceq wff n t x = n
46 24 43 25 co class x t n
47 46 43 wceq wff x t n = n
48 45 47 wa wff n t x = n ∧ x t n = n
49 42 48 wa wff ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z ∧ n t x = n ∧ x t n = n
50 49 20 21 wral wff ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z ∧ n t x = n ∧ x t n = n
51 50 19 18 wsbc wff [˙0 f / n]˙ ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z ∧ n t x = n ∧ x t n = n
52 51 16 15 wsbc wff [˙⋅ f / t]˙ [˙0 f / n]˙ ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z ∧ n t x = n ∧ x t n = n
53 52 13 12 wsbc wff [˙+ f / p]˙ [˙⋅ f / t]˙ [˙0 f / n]˙ ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z ∧ n t x = n ∧ x t n = n
54 53 10 9 wsbc wff [˙Base f / r]˙ [˙+ f / p]˙ [˙⋅ f / t]˙ [˙0 f / n]˙ ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z ∧ n t x = n ∧ x t n = n
55 7 54 wa wff mulGrp f ∈ Mnd ∧ [˙Base f / r]˙ [˙+ f / p]˙ [˙⋅ f / t]˙ [˙0 f / n]˙ ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z ∧ n t x = n ∧ x t n = n
56 55 1 2 crab class f ∈ CMnd | mulGrp f ∈ Mnd ∧ [˙Base f / r]˙ [˙+ f / p]˙ [˙⋅ f / t]˙ [˙0 f / n]˙ ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z ∧ n t x = n ∧ x t n = n
57 0 56 wceq wff SRing = f ∈ CMnd | mulGrp f ∈ Mnd ∧ [˙Base f / r]˙ [˙+ f / p]˙ [˙⋅ f / t]˙ [˙0 f / n]˙ ∀ x ∈ r ∀ y ∈ r ∀ z ∈ r x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z ∧ n t x = n ∧ x t n = n