Metamath Proof Explorer


Theorem ringmgp

Description: A ring is a monoid under multiplication. (Contributed by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypothesis ringmgp.g
|- G = ( mulGrp ` R )
Assertion ringmgp
|- ( R e. Ring -> G e. Mnd )

Proof

Step Hyp Ref Expression
1 ringmgp.g
 |-  G = ( mulGrp ` R )
2 eqid
 |-  ( Base ` R ) = ( Base ` R )
3 eqid
 |-  ( +g ` R ) = ( +g ` R )
4 eqid
 |-  ( .r ` R ) = ( .r ` R )
5 2 1 3 4 isring
 |-  ( R e. Ring <-> ( R e. Grp /\ G 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 ) ) ) ) )
6 5 simp2bi
 |-  ( R e. Ring -> G e. Mnd )