Theorem grpmnd 17650

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

Syntax hints:   → wi 4   = wceq 1632   ∈ wcel 2139  ∀wral 3050  ∃wrex 3051  ‘cfv 6049  (class class class)co 6814  Basecbs 16079  +_gcplusg 16163  0_gc0g 16322  Mndcmnd 17515  Grpcgrp 17643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6817  df-grp 17646

This theorem is referenced by:  grpcl  17651  grpass  17652  grpideu  17654  grpplusf  17655  grpplusfo  17656  grpsgrp  17667  dfgrp2  17668  grpidcl  17671  grplid  17673  grprid  17674  dfgrp3  17735  prdsgrpd  17746  prdsinvgd  17747  ghmgrp  17760  mulgaddcom  17785  mulginvcom  17786  mulgz  17789  mulgdirlem  17793  mulgneg2  17796  mulgass  17800  issubg3  17833  subgacs  17850  ghmmhm  17891  0ghm  17895  pwsdiagghm  17909  cntzsubg  17989  oppggrp  18007  gsumccatsymgsn  18066  symggen  18110  symgtrinv  18112  psgnunilem5  18134  psgnunilem2  18135  psgnuni  18139  psgneldm2  18144  psgnfitr  18157  lsmass  18303  lsmcntzr  18313  pj1ghm  18336  frgpmhm  18398  frgpuplem  18405  frgpupf  18406  frgpup1  18408  isabl2  18421  isabld  18426  gsumzinv  18565  telgsumfzslem  18605  telgsumfzs  18606  dprdssv  18635  dprdfid  18636  dprdfadd  18639  dprdfeq0  18641  dprdlub  18645  dmdprdsplitlem  18656  dprddisj2  18658  dpjidcl  18677  pgpfac1lem3a  18695  pgpfaclem3  18702  ringmnd  18776  unitabl  18888  unitsubm  18890  lmodvsmmulgdi  19120  psgnghm  20148  dsmmsubg  20309  frlm0  20320  mdetunilem7  20646  istgp2  22116  symgtgp  22126  clmmulg  23121  dchrptlem3  25211  abliso  30026  isarchi3  30071  ofldchr  30144  reofld  30170  pwssplit4  38179  pwslnmlem2  38183  gicabl  38189  mendring  38282  c0ghm  42439  c0snghm  42444  lmodvsmdi  42691  lincvalsng  42733  lincvalsc0  42738  linc0scn0  42740  linc1  42742  lcoel0  42745  lincsum  42746  lincsumcl  42748  snlindsntor  42788