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

Theorem grpmnd 15549
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 2442 . . 3  |-  ( Base `  G )  =  (
Base `  G )
2 eqid 2442 . . 3  |-  ( +g  `  G )  =  ( +g  `  G )
3 eqid 2442 . . 3  |-  ( 0g
`  G )  =  ( 0g `  G
)
41, 2, 3isgrp 15548 . 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 1369    e. wcel 1756   A.wral 2714   E.wrex 2715   ` cfv 5417  (class class class)co 6090   Basecbs 14173   +g cplusg 14237   0gc0g 14377   Mndcmnd 15408   Grpcgrp 15409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ral 2719  df-rex 2720  df-rab 2723  df-v 2973  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-nul 3637  df-if 3791  df-sn 3877  df-pr 3879  df-op 3883  df-uni 4091  df-br 4292  df-iota 5380  df-fv 5425  df-ov 6093  df-grp 15544
This theorem is referenced by:  grpcl  15550  grpass  15551  grpideu  15553  grpplusf  15554  grpidcl  15565  grplid  15567  grprid  15568  mulgz  15647  mulgdirlem  15650  mulgneg2  15653  mulgass  15656  prdsgrpd  15663  prdsinvgd  15664  issubg3  15698  subgacs  15715  ghmmhm  15756  0ghm  15760  pwsdiagghm  15773  cntzsubg  15853  oppggrp  15871  gsumccatsymgsn  15930  symggen  15975  symgtrinv  15977  psgnunilem5  15999  psgnunilem2  16000  psgnuni  16004  psgneldm2  16009  psgnfitr  16022  lsmass  16166  lsmcntzr  16176  pj1ghm  16199  frgpmhm  16261  frgpuplem  16268  frgpupf  16269  frgpup1  16271  isabl2  16284  isabld  16289  gsumzinv  16441  gsumzinvOLD  16442  dprdssv  16505  dprdfid  16506  dprdfadd  16509  dprdfeq0  16511  dprdfidOLD  16513  dprdfaddOLD  16516  dprdfeq0OLD  16518  dprdlub  16522  dmdprdsplitlem  16533  dmdprdsplitlemOLD  16534  dprddisj2  16536  dprddisj2OLD  16537  dpjidcl  16556  dpjidclOLD  16563  pgpfac1lem3a  16576  pgpfaclem3  16583  rngmnd  16653  unitabl  16759  unitsubm  16761  psgnghm  18009  dsmmsubg  18167  frlm0  18178  mdetunilem7  18423  istgp2  19661  symgtgp  19671  clmmulg  20664  dchrptlem3  22604  abliso  26158  isarchi3  26203  ofldchr  26281  reofld  26307  pwssplit4  29440  pwslnmlem2  29444  gicabl  29452  mendrng  29547  telescfzgsumlem  30807  telescfzgsum  30808  lmodvsmdi  30810  lmodvsmmulgdi  30811  lincvalsng  30948  lincvalsc0  30953  linc0scn0  30955  linc1  30957  lcoel0  30960  lincsum  30961  lincsumcl  30963  snlindsntor  31003
  Copyright terms: Public domain W3C validator