Theorem grpmnd 18110

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  ∀wral 3138  ∃wrex 3139  ‘cfv 6355  (class class class)co 7156  Basecbs 16483  +_gcplusg 16565  0_gc0g 16713  Mndcmnd 17911  Grpcgrp 18103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-grp 18106

This theorem is referenced by:  grpcl  18111  grpass  18112  grpideu  18114  grpplusf  18115  grpplusfo  18116  grpsgrp  18127  dfgrp2  18128  grpidcl  18131  grplid  18133  grprid  18134  hashfingrpnn  18136  dfgrp3  18198  prdsgrpd  18209  prdsinvgd  18210  ghmgrp  18223  mulgaddcom  18251  mulginvcom  18252  mulgz  18255  mulgdirlem  18258  mulgneg2  18261  mulgass  18264  issubg3  18297  grpissubg  18299  subgacs  18313  ghmmhm  18368  0ghm  18372  pwsdiagghm  18386  cntzsubg  18467  oppggrp  18485  symgsubmefmndALT  18531  gsumccatsymgsn  18554  symggen  18598  symgtrinv  18600  psgnunilem5  18622  psgnunilem2  18623  psgnuni  18627  psgneldm2  18632  psgnfitr  18645  lsmass  18795  lsmcntzr  18806  pj1ghm  18829  frgpmhm  18891  frgpuplem  18898  frgpupf  18899  frgpup1  18901  isabl2  18915  isabld  18920  cntrabl  18963  gsumzinv  19065  telgsumfzslem  19108  telgsumfzs  19109  dprdssv  19138  dprdfid  19139  dprdfadd  19142  dprdfeq0  19144  dprdlub  19148  dmdprdsplitlem  19159  dprddisj2  19161  dpjidcl  19180  pgpfac1lem3a  19198  pgpfaclem3  19205  simpgnideld  19221  ringmnd  19306  unitabl  19418  unitsubm  19420  lmodvsmmulgdi  19669  psgnghm  20724  dsmmsubg  20887  frlm0  20898  mdetunilem7  21227  istgp2  22699  clmmulg  23705  dchrptlem3  25842  abliso  30683  cyc3genpmlem  30793  cyc3genpm  30794  isarchi3  30816  ofldchr  30887  reofld  30913  lbslsat  31014  dimkerim  31023  fedgmullem2  31026  pwssplit4  39709  pwslnmlem2  39713  gicabl  39719  mendring  39812  c0ghm  44202  c0snghm  44207  lmodvsmdi  44450  lincvalsng  44491  lincvalsc0  44496  linc0scn0  44498  linc1  44500  lcoel0  44503  lincsum  44504  lincsumcl  44506  snlindsntor  44546