Metamath Proof Explorer

Theorem ringsrg

Description: Any ring is also a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Assertion ringsrg ⊢ R ∈ Ring → R ∈ SRing

Proof

Step Hyp Ref Expression
1 ringcmn ⊢ R ∈ Ring → R ∈ CMnd
2 eqid ⊢ mulGrp R = mulGrp R
3 2 ringmgp ⊢ R ∈ Ring → mulGrp R ∈ Mnd
4 eqid ⊢ Base R = Base R
5 eqid ⊢ + R = + R
6 eqid ⊢ ⋅ R = ⋅ R
7 4 2 5 6 isring ⊢ R ∈ Ring ↔ R ∈ Grp ∧ mulGrp R ∈ Mnd ∧ ∀ x ∈ Base R ∀ y ∈ Base R ∀ z ∈ Base R x ⋅ R y + R z = x ⋅ R y + R x ⋅ R z ∧ x + R y ⋅ R z = x ⋅ R z + R y ⋅ R z
8 7 simp3bi ⊢ R ∈ Ring → ∀ x ∈ Base R ∀ y ∈ Base R ∀ z ∈ Base R x ⋅ R y + R z = x ⋅ R y + R x ⋅ R z ∧ x + R y ⋅ R z = x ⋅ R z + R y ⋅ R z
9 eqid ⊢ 0 R = 0 R
10 4 6 9 ringlz ⊢ R ∈ Ring ∧ x ∈ Base R → 0 R ⋅ R x = 0 R
11 4 6 9 ringrz ⊢ R ∈ Ring ∧ x ∈ Base R → x ⋅ R 0 R = 0 R
12 10 11 jca ⊢ R ∈ Ring ∧ x ∈ Base R → 0 R ⋅ R x = 0 R ∧ x ⋅ R 0 R = 0 R
13 12 ralrimiva ⊢ R ∈ Ring → ∀ x ∈ Base R 0 R ⋅ R x = 0 R ∧ x ⋅ R 0 R = 0 R
14 r19.26 ⊢ ∀ x ∈ Base R ∀ y ∈ Base R ∀ z ∈ Base R x ⋅ R y + R z = x ⋅ R y + R x ⋅ R z ∧ x + R y ⋅ R z = x ⋅ R z + R y ⋅ R z ∧ 0 R ⋅ R x = 0 R ∧ x ⋅ R 0 R = 0 R ↔ ∀ x ∈ Base R ∀ y ∈ Base R ∀ z ∈ Base R x ⋅ R y + R z = x ⋅ R y + R x ⋅ R z ∧ x + R y ⋅ R z = x ⋅ R z + R y ⋅ R z ∧ ∀ x ∈ Base R 0 R ⋅ R x = 0 R ∧ x ⋅ R 0 R = 0 R
15 8 13 14 sylanbrc ⊢ R ∈ Ring → ∀ x ∈ Base R ∀ y ∈ Base R ∀ z ∈ Base R x ⋅ R y + R z = x ⋅ R y + R x ⋅ R z ∧ x + R y ⋅ R z = x ⋅ R z + R y ⋅ R z ∧ 0 R ⋅ R x = 0 R ∧ x ⋅ R 0 R = 0 R
16 4 2 5 6 9 issrg ⊢ R ∈ SRing ↔ R ∈ CMnd ∧ mulGrp R ∈ Mnd ∧ ∀ x ∈ Base R ∀ y ∈ Base R ∀ z ∈ Base R x ⋅ R y + R z = x ⋅ R y + R x ⋅ R z ∧ x + R y ⋅ R z = x ⋅ R z + R y ⋅ R z ∧ 0 R ⋅ R x = 0 R ∧ x ⋅ R 0 R = 0 R
17 1 3 15 16 syl3anbrc ⊢ R ∈ Ring → R ∈ SRing