Theorem iscsrg

Description: A commutative semiring is a semiring whose multiplication is a commutative monoid. (Contributed by metakunt, 4-Apr-2025)

	Ref	Expression
Hypothesis	iscsrg.g	$$⊢G={\mathrm{mulGrp}}_R$$
Assertion	iscsrg	$$⊢R\in \mathrm{CSRing}\leftrightarrow \left(R\in \mathrm{SRing}\wedge G\in \mathrm{CMnd}\right)$$

Proof

Step	Hyp	Ref	Expression
1		iscsrg.g	$$⊢G={\mathrm{mulGrp}}_R$$
2		fveq2	$$⊢r=R\to {\mathrm{mulGrp}}_r={\mathrm{mulGrp}}_R$$
3	2 1	eqtr4di	$$⊢r=R\to {\mathrm{mulGrp}}_r=G$$
4	3	eleq1d	$$⊢r=R\to \left({\mathrm{mulGrp}}_r\in \mathrm{CMnd}\leftrightarrow G\in \mathrm{CMnd}\right)$$
5		df-csring	$$⊢\mathrm{CSRing}=\left\{r\in \mathrm{SRing}|{\mathrm{mulGrp}}_r\in \mathrm{CMnd}\right\}$$
6	4 5	elrab2	$$⊢R\in \mathrm{CSRing}\leftrightarrow \left(R\in \mathrm{SRing}\wedge G\in \mathrm{CMnd}\right)$$