Theorem grpmnd 17476

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 2651	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		eqid 2651	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
3		eqid 2651	. . 3 ⊢ (0g‘𝐺) = (0g‘𝐺)
4	1, 2, 3	isgrp 17475	. 2 ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Mnd ∧ ∀𝑎 ∈ (Base‘𝐺)∃𝑚 ∈ (Base‘𝐺)(𝑚(+g‘𝐺)𝑎) = (0g‘𝐺)))
5	4	simplbi 475	1 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)

Syntax hints:   → wi 4   = wceq 1523   ∈ wcel 2030  ∀wral 2941  ∃wrex 2942  ‘cfv 5926  (class class class)co 6690  Basecbs 15904  +_gcplusg 15988  0_gc0g 16147  Mndcmnd 17341  Grpcgrp 17469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-grp 17472

This theorem is referenced by:  grpcl  17477  grpass  17478  grpideu  17480  grpplusf  17481  grpplusfo  17482  grpsgrp  17493  dfgrp2  17494  grpidcl  17497  grplid  17499  grprid  17500  dfgrp3  17561  prdsgrpd  17572  prdsinvgd  17573  ghmgrp  17586  mulgaddcom  17611  mulginvcom  17612  mulgz  17615  mulgdirlem  17619  mulgneg2  17622  mulgass  17626  issubg3  17659  subgacs  17676  ghmmhm  17717  0ghm  17721  pwsdiagghm  17735  cntzsubg  17815  oppggrp  17833  gsumccatsymgsn  17892  symggen  17936  symgtrinv  17938  psgnunilem5  17960  psgnunilem2  17961  psgnuni  17965  psgneldm2  17970  psgnfitr  17983  lsmass  18129  lsmcntzr  18139  pj1ghm  18162  frgpmhm  18224  frgpuplem  18231  frgpupf  18232  frgpup1  18234  isabl2  18247  isabld  18252  gsumzinv  18391  telgsumfzslem  18431  telgsumfzs  18432  dprdssv  18461  dprdfid  18462  dprdfadd  18465  dprdfeq0  18467  dprdlub  18471  dmdprdsplitlem  18482  dprddisj2  18484  dpjidcl  18503  pgpfac1lem3a  18521  pgpfaclem3  18528  ringmnd  18602  unitabl  18714  unitsubm  18716  lmodvsmmulgdi  18946  psgnghm  19974  dsmmsubg  20135  frlm0  20146  mdetunilem7  20472  istgp2  21942  symgtgp  21952  clmmulg  22947  dchrptlem3  25036  abliso  29824  isarchi3  29869  ofldchr  29942  reofld  29968  pwssplit4  37976  pwslnmlem2  37980  gicabl  37986  mendring  38079  c0ghm  42236  c0snghm  42241  lmodvsmdi  42488  lincvalsng  42530  lincvalsc0  42535  linc0scn0  42537  linc1  42539  lcoel0  42542  lincsum  42543  lincsumcl  42545  snlindsntor  42585