Metamath Proof Explorer

Theorem srgcmn

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

Ref Expression
Assertion srgcmn 
|- ( R e. SRing -> R e. CMnd )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` R ) = ( Base ` R )
2 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
3 eqid 
 |-  ( +g ` R ) = ( +g ` R )
4 eqid 
 |-  ( .r ` R ) = ( .r ` R )
5 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
6 1 2 3 4 5 issrg 
 |-  ( R e. SRing <-> ( R e. CMnd /\ ( mulGrp ` R ) e. Mnd /\ A. x e. ( Base ` R ) ( A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) /\ ( ( ( 0g ` R ) ( .r ` R ) x ) = ( 0g ` R ) /\ ( x ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) ) ) )
7 6 simp1bi 
 |-  ( R e. SRing -> R e. CMnd )