Theorem grpmnd 17252

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.

Step	Hyp	Ref	Expression
1		eqid 2610	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		eqid 2610	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
3		eqid 2610	. . 3 ⊢ (0g‘𝐺) = (0g‘𝐺)
4	1, 2, 3	isgrp 17251	. 2 ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Mnd ∧ ∀𝑎 ∈ (Base‘𝐺)∃𝑚 ∈ (Base‘𝐺)(𝑚(+g‘𝐺)𝑎) = (0g‘𝐺)))
5	4	simplbi 475	1 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  +_gcplusg 15768  0_gc0g 15923  Mndcmnd 17117  Grpcgrp 17245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-grp 17248

This theorem is referenced by:  grpcl  17253  grpass  17254  grpideu  17256  grpplusf  17257  grpplusfo  17258  grpsgrp  17269  dfgrp2  17270  grpidcl  17273  grplid  17275  grprid  17276  dfgrp3  17337  prdsgrpd  17348  prdsinvgd  17349  ghmgrp  17362  mulgaddcom  17387  mulginvcom  17388  mulgz  17391  mulgdirlem  17395  mulgneg2  17398  mulgass  17402  issubg3  17435  subgacs  17452  ghmmhm  17493  0ghm  17497  pwsdiagghm  17511  cntzsubg  17592  oppggrp  17610  gsumccatsymgsn  17669  symggen  17713  symgtrinv  17715  psgnunilem5  17737  psgnunilem2  17738  psgnuni  17742  psgneldm2  17747  psgnfitr  17760  lsmass  17906  lsmcntzr  17916  pj1ghm  17939  frgpmhm  18001  frgpuplem  18008  frgpupf  18009  frgpup1  18011  isabl2  18024  isabld  18029  gsumzinv  18168  telgsumfzslem  18208  telgsumfzs  18209  dprdssv  18238  dprdfid  18239  dprdfadd  18242  dprdfeq0  18244  dprdlub  18248  dmdprdsplitlem  18259  dprddisj2  18261  dpjidcl  18280  pgpfac1lem3a  18298  pgpfaclem3  18305  ringmnd  18379  unitabl  18491  unitsubm  18493  lmodvsmmulgdi  18721  psgnghm  19745  dsmmsubg  19906  frlm0  19917  mdetunilem7  20243  istgp2  21705  symgtgp  21715  clmmulg  22709  dchrptlem3  24791  abliso  29027  isarchi3  29072  ofldchr  29145  reofld  29171  pwssplit4  36677  pwslnmlem2  36681  gicabl  36687  mendring  36781  c0ghm  41701  c0snghm  41706  lmodvsmdi  41957  lincvalsng  41999  lincvalsc0  42004  linc0scn0  42006  linc1  42008  lcoel0  42011  lincsum  42012  lincsumcl  42014  snlindsntor  42054