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

Theorem grpmnd 17630
Description: A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
Assertion
Ref Expression
grpmnd (𝐺 ∈ Grp → 𝐺 ∈ Mnd)

Proof of Theorem grpmnd
Dummy variables 𝑚 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2806 . . 3 (Base‘𝐺) = (Base‘𝐺)
2 eqid 2806 . . 3 (+g𝐺) = (+g𝐺)
3 eqid 2806 . . 3 (0g𝐺) = (0g𝐺)
41, 2, 3isgrp 17629 . 2 (𝐺 ∈ Grp ↔ (𝐺 ∈ Mnd ∧ ∀𝑎 ∈ (Base‘𝐺)∃𝑚 ∈ (Base‘𝐺)(𝑚(+g𝐺)𝑎) = (0g𝐺)))
54simplbi 487 1 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  wcel 2156  wral 3096  wrex 3097  cfv 6097  (class class class)co 6870  Basecbs 16064  +gcplusg 16149  0gc0g 16301  Mndcmnd 17495  Grpcgrp 17623
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-iota 6060  df-fv 6105  df-ov 6873  df-grp 17626
This theorem is referenced by:  grpcl  17631  grpass  17632  grpideu  17634  grpplusf  17635  grpplusfo  17636  grpsgrp  17647  dfgrp2  17648  grpidcl  17651  grplid  17653  grprid  17654  dfgrp3  17715  prdsgrpd  17726  prdsinvgd  17727  ghmgrp  17740  mulgaddcom  17764  mulginvcom  17765  mulgz  17768  mulgdirlem  17771  mulgneg2  17774  mulgass  17777  issubg3  17810  subgacs  17827  ghmmhm  17868  0ghm  17872  pwsdiagghm  17886  cntzsubg  17966  oppggrp  17984  gsumccatsymgsn  18043  symggen  18087  symgtrinv  18089  psgnunilem5  18111  psgnunilem2  18112  psgnuni  18116  psgneldm2  18121  psgnfitr  18134  lsmass  18280  lsmcntzr  18290  pj1ghm  18313  frgpmhm  18375  frgpuplem  18382  frgpupf  18383  frgpup1  18385  isabl2  18398  isabld  18403  gsumzinv  18542  telgsumfzslem  18583  telgsumfzs  18584  dprdssv  18613  dprdfid  18614  dprdfadd  18617  dprdfeq0  18619  dprdlub  18623  dmdprdsplitlem  18634  dprddisj2  18636  dpjidcl  18655  pgpfac1lem3a  18673  pgpfaclem3  18680  ringmnd  18754  unitabl  18866  unitsubm  18868  lmodvsmmulgdi  19098  psgnghm  20129  dsmmsubg  20294  frlm0  20305  mdetunilem7  20632  istgp2  22105  symgtgp  22115  clmmulg  23110  dchrptlem3  25204  abliso  30020  isarchi3  30065  ofldchr  30138  reofld  30164  pwssplit4  38157  pwslnmlem2  38161  gicabl  38167  mendring  38260  c0ghm  42476  c0snghm  42481  lmodvsmdi  42728  lincvalsng  42770  lincvalsc0  42775  linc0scn0  42777  linc1  42779  lcoel0  42782  lincsum  42783  lincsumcl  42785  snlindsntor  42825
  Copyright terms: Public domain W3C validator