Theorem grpmnd 18102

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

Syntax hints:   → wi 4   = wceq 1531   ∈ wcel 2108  ∀wral 3136  ∃wrex 3137  ‘cfv 6348  (class class class)co 7148  Basecbs 16475  +_gcplusg 16557  0_gc0g 16705  Mndcmnd 17903  Grpcgrp 18095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7151  df-grp 18098

This theorem is referenced by:  grpcl  18103  grpass  18104  grpideu  18106  grpplusf  18107  grpplusfo  18108  grpsgrp  18119  dfgrp2  18120  grpidcl  18123  grplid  18125  grprid  18126  hashfingrpnn  18128  dfgrp3  18190  prdsgrpd  18201  prdsinvgd  18202  ghmgrp  18215  mulgaddcom  18243  mulginvcom  18244  mulgz  18247  mulgdirlem  18250  mulgneg2  18253  mulgass  18256  issubg3  18289  grpissubg  18291  subgacs  18305  ghmmhm  18360  0ghm  18364  pwsdiagghm  18378  cntzsubg  18459  oppggrp  18477  symgsubmefmndALT  18523  gsumccatsymgsn  18546  symggen  18590  symgtrinv  18592  psgnunilem5  18614  psgnunilem2  18615  psgnuni  18619  psgneldm2  18624  psgnfitr  18637  lsmass  18787  lsmcntzr  18798  pj1ghm  18821  frgpmhm  18883  frgpuplem  18890  frgpupf  18891  frgpup1  18893  isabl2  18907  isabld  18912  cntrabl  18955  gsumzinv  19057  telgsumfzslem  19100  telgsumfzs  19101  dprdssv  19130  dprdfid  19131  dprdfadd  19134  dprdfeq0  19136  dprdlub  19140  dmdprdsplitlem  19151  dprddisj2  19153  dpjidcl  19172  pgpfac1lem3a  19190  pgpfaclem3  19197  simpgnideld  19213  ringmnd  19298  unitabl  19410  unitsubm  19412  lmodvsmmulgdi  19661  psgnghm  20716  dsmmsubg  20879  frlm0  20890  mdetunilem7  21219  istgp2  22691  clmmulg  23697  dchrptlem3  25834  abliso  30676  cyc3genpmlem  30786  cyc3genpm  30787  isarchi3  30809  ofldchr  30880  reofld  30906  lbslsat  31007  dimkerim  31016  fedgmullem2  31019  pwssplit4  39679  pwslnmlem2  39683  gicabl  39689  mendring  39782  c0ghm  44172  c0snghm  44177  lmodvsmdi  44420  lincvalsng  44461  lincvalsc0  44466  linc0scn0  44468  linc1  44470  lcoel0  44473  lincsum  44474  lincsumcl  44476  snlindsntor  44516