srgcmn

Description: A semiring is a commutative monoid. (Contributed by Thierry Arnoux, 21-Mar-2018)

		Ref	Expression
	Assertion	srgcmn	$⊢ R \in SRing \to R \in CMnd$

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{R} = {Base}_{R}$
2		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
3		eqid	$⊢ +_{R} = +_{R}$
4		eqid	$⊢ \cdot_{R} = \cdot_{R}$
5		eqid	$⊢ 0_{R} = 0_{R}$
6	1 2 3 4 5	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})))$
7	6	simp1bi	$⊢ R \in SRing \to R \in CMnd$

Metamath Proof Explorer