This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 Ring \to R \in SRing$

Proof

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