MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  grpmnd Structured version   Unicode version

Theorem grpmnd 15858
Description: A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
Assertion
Ref Expression
grpmnd  |-  ( G  e.  Grp  ->  G  e.  Mnd )

Proof of Theorem grpmnd
Dummy variables  m  a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2462 . . 3  |-  ( Base `  G )  =  (
Base `  G )
2 eqid 2462 . . 3  |-  ( +g  `  G )  =  ( +g  `  G )
3 eqid 2462 . . 3  |-  ( 0g
`  G )  =  ( 0g `  G
)
41, 2, 3isgrp 15857 . 2  |-  ( G  e.  Grp  <->  ( G  e.  Mnd  /\  A. a  e.  ( Base `  G
) E. m  e.  ( Base `  G
) ( m ( +g  `  G ) a )  =  ( 0g `  G ) ) )
54simplbi 460 1  |-  ( G  e.  Grp  ->  G  e.  Mnd )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374    e. wcel 1762   A.wral 2809   E.wrex 2810   ` cfv 5581  (class class class)co 6277   Basecbs 14481   +g cplusg 14546   0gc0g 14686   Mndcmnd 15717   Grpcgrp 15718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-br 4443  df-iota 5544  df-fv 5589  df-ov 6280  df-grp 15853
This theorem is referenced by:  grpcl  15859  grpass  15860  grpideu  15862  grpplusf  15863  grpidcl  15874  grplid  15876  grprid  15877  mulgz  15958  mulgdirlem  15961  mulgneg2  15964  mulgass  15967  prdsgrpd  15974  prdsinvgd  15975  issubg3  16009  subgacs  16026  ghmmhm  16067  0ghm  16071  pwsdiagghm  16084  cntzsubg  16164  oppggrp  16182  gsumccatsymgsn  16241  symggen  16286  symgtrinv  16288  psgnunilem5  16310  psgnunilem2  16311  psgnuni  16315  psgneldm2  16320  psgnfitr  16333  lsmass  16479  lsmcntzr  16489  pj1ghm  16512  frgpmhm  16574  frgpuplem  16581  frgpupf  16582  frgpup1  16584  isabl2  16597  isabld  16602  gsumzinv  16755  gsumzinvOLD  16756  telgsumfzslem  16803  telgsumfzs  16804  dprdssv  16841  dprdfid  16842  dprdfadd  16845  dprdfeq0  16847  dprdfidOLD  16849  dprdfaddOLD  16852  dprdfeq0OLD  16854  dprdlub  16858  dmdprdsplitlem  16869  dmdprdsplitlemOLD  16870  dprddisj2  16872  dprddisj2OLD  16873  dpjidcl  16892  dpjidclOLD  16899  pgpfac1lem3a  16912  pgpfaclem3  16919  rngmnd  16990  unitabl  17096  unitsubm  17098  lmodvsmmulgdi  17325  psgnghm  18378  dsmmsubg  18536  frlm0  18547  mdetunilem7  18882  istgp2  20320  symgtgp  20330  clmmulg  21323  dchrptlem3  23264  abliso  27336  isarchi3  27381  ofldchr  27455  reofld  27481  pwssplit4  30630  pwslnmlem2  30634  gicabl  30642  mendrng  30737  grpsgrp  31855  lmodvsmdi  31925  lincvalsng  31967  lincvalsc0  31972  linc0scn0  31974  linc1  31976  lcoel0  31979  lincsum  31980  lincsumcl  31982  snlindsntor  32022
  Copyright terms: Public domain W3C validator