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	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
Assertion	iscsrg	⊢ ( 𝑅 ∈ CSRing ↔ ( 𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd ) )

Proof

Step	Hyp	Ref	Expression
1		iscsrg.g	⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
2		fveq2	⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑅 ) )
3	2 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = 𝐺 )
4	3	eleq1d	⊢ ( 𝑟 = 𝑅 → ( ( mulGrp ‘ 𝑟 ) ∈ CMnd ↔ 𝐺 ∈ CMnd ) )
5		df-csring	⊢ CSRing = { 𝑟 ∈ SRing ∣ ( mulGrp ‘ 𝑟 ) ∈ CMnd }
6	4 5	elrab2	⊢ ( 𝑅 ∈ CSRing ↔ ( 𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd ) )