Metamath Proof Explorer

Theorem grpmnd

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

Ref Expression
Assertion grpmnd 
|- ( G e. Grp -> G e. Mnd )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` G ) = ( Base ` G )
2 eqid 
 |-  ( +g ` G ) = ( +g ` G )
3 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
4 1 2 3 isgrp 
 |-  ( G e. Grp <-> ( G e. Mnd /\ A. a e. ( Base ` G ) E. m e. ( Base ` G ) ( m ( +g ` G ) a ) = ( 0g ` G ) ) )
5 4 simplbi 
 |-  ( G e. Grp -> G e. Mnd )