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 = ( mulGrp ` R )
Assertion	iscsrg	|- ( R e. CSRing <-> ( R e. SRing /\ G e. CMnd ) )

Proof

Step	Hyp	Ref	Expression
1		iscsrg.g	|- G = ( mulGrp ` R )
2		fveq2	|- ( r = R -> ( mulGrp ` r ) = ( mulGrp ` R ) )
3	2 1	eqtr4di	|- ( r = R -> ( mulGrp ` r ) = G )
4	3	eleq1d	|- ( r = R -> ( ( mulGrp ` r ) e. CMnd <-> G e. CMnd ) )
5		df-csring	|- CSRing = { r e. SRing | ( mulGrp ` r ) e. CMnd }
6	4 5	elrab2	|- ( R e. CSRing <-> ( R e. SRing /\ G e. CMnd ) )