Theorem grpmnd 17856

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

Syntax hints:   → wi 4   = wceq 1520   ∈ wcel 2079  ∀wral 3103  ∃wrex 3104  ‘cfv 6217  (class class class)co 7007  Basecbs 16300  +_gcplusg 16382  0_gc0g 16530  Mndcmnd 17721  Grpcgrp 17849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-iota 6181  df-fv 6225  df-ov 7010  df-grp 17852

This theorem is referenced by:  grpcl  17857  grpass  17858  grpideu  17860  grpplusf  17861  grpplusfo  17862  grpsgrp  17873  dfgrp2  17874  grpidcl  17877  grplid  17879  grprid  17880  dfgrp3  17943  prdsgrpd  17954  prdsinvgd  17955  ghmgrp  17968  mulgaddcom  17993  mulginvcom  17994  mulgz  17997  mulgdirlem  18000  mulgneg2  18003  mulgass  18006  issubg3  18039  subgacs  18056  ghmmhm  18097  0ghm  18101  pwsdiagghm  18115  cntzsubg  18196  oppggrp  18214  gsumccatsymgsn  18273  symggen  18317  symgtrinv  18319  psgnunilem5  18341  psgnunilem2  18342  psgnuni  18346  psgneldm2  18351  psgnfitr  18364  lsmass  18511  lsmcntzr  18521  pj1ghm  18544  frgpmhm  18606  frgpuplem  18613  frgpupf  18614  frgpup1  18616  isabl2  18629  isabld  18634  gsumzinv  18773  telgsumfzslem  18813  telgsumfzs  18814  dprdssv  18843  dprdfid  18844  dprdfadd  18847  dprdfeq0  18849  dprdlub  18853  dmdprdsplitlem  18864  dprddisj2  18866  dpjidcl  18885  pgpfac1lem3a  18903  pgpfaclem3  18910  ringmnd  18984  unitabl  19096  unitsubm  19098  lmodvsmmulgdi  19347  psgnghm  20394  dsmmsubg  20557  frlm0  20568  mdetunilem7  20899  istgp2  22371  symgtgp  22381  clmmulg  23376  dchrptlem3  25512  abliso  30327  cyc3genpmlem  30389  cyc3genpm  30390  isarchi3  30412  cntrabl  30464  ofldchr  30496  reofld  30522  lbslsat  30573  dimkerim  30582  fedgmullem2  30585  pwssplit4  39125  pwslnmlem2  39129  gicabl  39135  mendring  39228  hashfingrpnn  40097  simpgnideld  40107  c0ghm  43614  c0snghm  43619  lmodvsmdi  43864  lincvalsng  43905  lincvalsc0  43910  linc0scn0  43912  linc1  43914  lcoel0  43917  lincsum  43918  lincsumcl  43920  snlindsntor  43960