Metamath Proof Explorer

Theorem ringsrg

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

Ref Expression
Assertion ringsrg ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{SRing}$

Proof

Step Hyp Ref Expression
1 ringcmn ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{CMnd}$
2 eqid ${⊢}{\mathrm{mulGrp}}_{{R}}={\mathrm{mulGrp}}_{{R}}$
3 2 ringmgp ${⊢}{R}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{R}}\in \mathrm{Mnd}$
4 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
5 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
6 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
7 4 2 5 6 isring ${⊢}{R}\in \mathrm{Ring}↔\left({R}\in \mathrm{Grp}\wedge {\mathrm{mulGrp}}_{{R}}\in \mathrm{Mnd}\wedge \forall {x}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{R}}\left({y}{+}_{{R}}{z}\right)=\left({x}{\cdot }_{{R}}{y}\right){+}_{{R}}\left({x}{\cdot }_{{R}}{z}\right)\wedge \left({x}{+}_{{R}}{y}\right){\cdot }_{{R}}{z}=\left({x}{\cdot }_{{R}}{z}\right){+}_{{R}}\left({y}{\cdot }_{{R}}{z}\right)\right)\right)$
8 7 simp3bi ${⊢}{R}\in \mathrm{Ring}\to \forall {x}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{R}}\left({y}{+}_{{R}}{z}\right)=\left({x}{\cdot }_{{R}}{y}\right){+}_{{R}}\left({x}{\cdot }_{{R}}{z}\right)\wedge \left({x}{+}_{{R}}{y}\right){\cdot }_{{R}}{z}=\left({x}{\cdot }_{{R}}{z}\right){+}_{{R}}\left({y}{\cdot }_{{R}}{z}\right)\right)$
9 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
10 4 6 9 ringlz ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {\mathrm{Base}}_{{R}}\right)\to {0}_{{R}}{\cdot }_{{R}}{x}={0}_{{R}}$
11 4 6 9 ringrz ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {\mathrm{Base}}_{{R}}\right)\to {x}{\cdot }_{{R}}{0}_{{R}}={0}_{{R}}$
12 10 11 jca ${⊢}\left({R}\in \mathrm{Ring}\wedge {x}\in {\mathrm{Base}}_{{R}}\right)\to \left({0}_{{R}}{\cdot }_{{R}}{x}={0}_{{R}}\wedge {x}{\cdot }_{{R}}{0}_{{R}}={0}_{{R}}\right)$
13 12 ralrimiva ${⊢}{R}\in \mathrm{Ring}\to \forall {x}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left({0}_{{R}}{\cdot }_{{R}}{x}={0}_{{R}}\wedge {x}{\cdot }_{{R}}{0}_{{R}}={0}_{{R}}\right)$
14 r19.26 ${⊢}\forall {x}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{R}}\left({y}{+}_{{R}}{z}\right)=\left({x}{\cdot }_{{R}}{y}\right){+}_{{R}}\left({x}{\cdot }_{{R}}{z}\right)\wedge \left({x}{+}_{{R}}{y}\right){\cdot }_{{R}}{z}=\left({x}{\cdot }_{{R}}{z}\right){+}_{{R}}\left({y}{\cdot }_{{R}}{z}\right)\right)\wedge \left({0}_{{R}}{\cdot }_{{R}}{x}={0}_{{R}}\wedge {x}{\cdot }_{{R}}{0}_{{R}}={0}_{{R}}\right)\right)↔\left(\forall {x}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{R}}\left({y}{+}_{{R}}{z}\right)=\left({x}{\cdot }_{{R}}{y}\right){+}_{{R}}\left({x}{\cdot }_{{R}}{z}\right)\wedge \left({x}{+}_{{R}}{y}\right){\cdot }_{{R}}{z}=\left({x}{\cdot }_{{R}}{z}\right){+}_{{R}}\left({y}{\cdot }_{{R}}{z}\right)\right)\wedge \forall {x}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left({0}_{{R}}{\cdot }_{{R}}{x}={0}_{{R}}\wedge {x}{\cdot }_{{R}}{0}_{{R}}={0}_{{R}}\right)\right)$
15 8 13 14 sylanbrc ${⊢}{R}\in \mathrm{Ring}\to \forall {x}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{R}}\left({y}{+}_{{R}}{z}\right)=\left({x}{\cdot }_{{R}}{y}\right){+}_{{R}}\left({x}{\cdot }_{{R}}{z}\right)\wedge \left({x}{+}_{{R}}{y}\right){\cdot }_{{R}}{z}=\left({x}{\cdot }_{{R}}{z}\right){+}_{{R}}\left({y}{\cdot }_{{R}}{z}\right)\right)\wedge \left({0}_{{R}}{\cdot }_{{R}}{x}={0}_{{R}}\wedge {x}{\cdot }_{{R}}{0}_{{R}}={0}_{{R}}\right)\right)$
16 4 2 5 6 9 issrg ${⊢}{R}\in \mathrm{SRing}↔\left({R}\in \mathrm{CMnd}\wedge {\mathrm{mulGrp}}_{{R}}\in \mathrm{Mnd}\wedge \forall {x}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{R}}\left({y}{+}_{{R}}{z}\right)=\left({x}{\cdot }_{{R}}{y}\right){+}_{{R}}\left({x}{\cdot }_{{R}}{z}\right)\wedge \left({x}{+}_{{R}}{y}\right){\cdot }_{{R}}{z}=\left({x}{\cdot }_{{R}}{z}\right){+}_{{R}}\left({y}{\cdot }_{{R}}{z}\right)\right)\wedge \left({0}_{{R}}{\cdot }_{{R}}{x}={0}_{{R}}\wedge {x}{\cdot }_{{R}}{0}_{{R}}={0}_{{R}}\right)\right)\right)$
17 1 3 15 16 syl3anbrc ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{SRing}$