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

Theorem grpmnd 15936
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 2443 . . 3  |-  ( Base `  G )  =  (
Base `  G )
2 eqid 2443 . . 3  |-  ( +g  `  G )  =  ( +g  `  G )
3 eqid 2443 . . 3  |-  ( 0g
`  G )  =  ( 0g `  G
)
41, 2, 3isgrp 15935 . 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 1383    e. wcel 1804   A.wral 2793   E.wrex 2794   ` cfv 5578  (class class class)co 6281   Basecbs 14509   +g cplusg 14574   0gc0g 14714   Mndcmnd 15793   Grpcgrp 15927
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284  df-grp 15931
This theorem is referenced by:  grpcl  15937  grpass  15938  grpideu  15940  grpplusf  15941  grpidcl  15952  grplid  15954  grprid  15955  mulgz  16037  mulgdirlem  16040  mulgneg2  16043  mulgass  16046  prdsgrpd  16053  prdsinvgd  16054  ghmgrp  16068  issubg3  16093  subgacs  16110  ghmmhm  16151  0ghm  16155  pwsdiagghm  16168  cntzsubg  16248  oppggrp  16266  gsumccatsymgsn  16325  symggen  16369  symgtrinv  16371  psgnunilem5  16393  psgnunilem2  16394  psgnuni  16398  psgneldm2  16403  psgnfitr  16416  lsmass  16562  lsmcntzr  16572  pj1ghm  16595  frgpmhm  16657  frgpuplem  16664  frgpupf  16665  frgpup1  16667  isabl2  16680  isabld  16685  gsumzinv  16843  gsumzinvOLD  16844  telgsumfzslem  16891  telgsumfzs  16892  dprdssv  16930  dprdfid  16931  dprdfadd  16934  dprdfeq0  16936  dprdfidOLD  16938  dprdfaddOLD  16941  dprdfeq0OLD  16943  dprdlub  16947  dmdprdsplitlem  16958  dmdprdsplitlemOLD  16959  dprddisj2  16961  dprddisj2OLD  16962  dpjidcl  16981  dpjidclOLD  16988  pgpfac1lem3a  17001  pgpfaclem3  17008  ringmnd  17081  unitabl  17191  unitsubm  17193  lmodvsmmulgdi  17421  psgnghm  18489  dsmmsubg  18647  frlm0  18658  mdetunilem7  18993  istgp2  20463  symgtgp  20473  clmmulg  21466  dchrptlem3  23413  abliso  27559  isarchi3  27604  ofldchr  27677  reofld  27703  pwssplit4  31010  pwslnmlem2  31014  gicabl  31022  mendring  31117  lmodvsmdi  32710  lincvalsng  32752  lincvalsc0  32757  linc0scn0  32759  linc1  32761  lcoel0  32764  lincsum  32765  lincsumcl  32767  snlindsntor  32807
  Copyright terms: Public domain W3C validator