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

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