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

Theorem grpmnd 14510
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 2296 . . 3  |-  ( Base `  G )  =  (
Base `  G )
2 eqid 2296 . . 3  |-  ( +g  `  G )  =  ( +g  `  G )
3 eqid 2296 . . 3  |-  ( 0g
`  G )  =  ( 0g `  G
)
41, 2, 3isgrp 14509 . 2  |-  ( G  e.  Grp  <->  ( G  e.  Mnd  /\  A. a  e.  ( Base `  G
) E. m  e.  ( Base `  G
) ( m ( +g  `  G ) a )  =  ( 0g `  G ) ) )
54simplbi 446 1  |-  ( G  e.  Grp  ->  G  e.  Mnd )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696   A.wral 2556   E.wrex 2557   ` cfv 5271  (class class class)co 5874   Basecbs 13164   +g cplusg 13224   0gc0g 13416   Mndcmnd 14377   Grpcgrp 14378
This theorem is referenced by:  grpcl  14511  grpass  14512  grpideu  14514  grpplusf  14515  grpidcl  14526  grplid  14528  grprid  14529  mulgz  14604  mulgdirlem  14607  mulgneg2  14610  mulgass  14613  prdsgrpd  14620  prdsinvgd  14621  issubg3  14653  subgacs  14668  ghmmhm  14709  0ghm  14713  pwsdiagghm  14726  cntzsubg  14828  oppggrp  14846  lsmass  14995  lsmcntzr  15005  pj1ghm  15028  frgpmhm  15090  frgpuplem  15097  frgpupf  15098  frgpup1  15100  isabl2  15113  isabld  15118  gsumzinv  15233  dprdssv  15267  dprdfid  15268  dprdfadd  15271  dprdfeq0  15273  dprdlub  15277  dmdprdsplitlem  15288  dprddisj2  15290  dpjidcl  15309  pgpfac1lem3a  15327  pgpfaclem3  15334  rngmnd  15366  unitabl  15466  unitsubm  15468  istgp2  17790  symgtgp  17800  clmmulg  18607  dchrptlem3  20521  symgfo  25471  pwssplit4  27294  pwslnmlem2  27298  dsmmsubg  27312  frlm0  27325  gicabl  27366  symggen  27514  symgtrinv  27516  psgnunilem5  27520  psgnunilem2  27521  psgnuni  27525  psgneldm2  27530  psgnghm  27540  mendrng  27603
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-grp 14505
  Copyright terms: Public domain W3C validator