Theorem srgcmn

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

	Ref	Expression
Assertion	srgcmn	⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ CMnd )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
2		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
3		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
4		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
5		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
6	1 2 3 4 5	issrg	⊢ ( 𝑅 ∈ SRing ↔ ( 𝑅 ∈ CMnd ∧ ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑧 ) ) ∧ ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑧 ) ( +g ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ) ∧ ( ( ( 0g ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 0g ‘ 𝑅 ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) ) ) ) )
7	6	simp1bi	⊢ ( 𝑅 ∈ SRing → 𝑅 ∈ CMnd )