Theorem grpmnd 18882

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  ‘cfv 6500  (class class class)co 7368  Basecbs 17148  +_gcplusg 17189  0_gc0g 17371  Mndcmnd 18671  Grpcgrp 18875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-grp 18878

This theorem is referenced by:  grpcl  18883  grpass  18884  grpideu  18886  grpmndd  18888  grpplusf  18890  grpplusfo  18891  grpsgrp  18902  dfgrp2  18904  grpidcl  18907  grplid  18909  grprid  18910  dfgrp3  18981  prdsgrpd  18992  prdsinvgd  18993  mulgaddcom  19040  mulginvcom  19041  mulgz  19044  mulgneg2  19050  mulgass  19053  issubg3  19086  grpissubg  19088  0subg  19093  subgacs  19102  0ghm  19171  pwsdiagghm  19185  cntzsubg  19280  oppggrp  19298  symgsubmefmndALT  19344  psgnunilem5  19435  psgnuni  19440  0subgALT  19509  lsmcntzr  19621  pj1ghm  19644  isabl2  19731  cntrabl  19784  dprdfid  19960  dprdfeq0  19965  dprdlub  19969  dmdprdsplitlem  19980  dprddisj2  19982  dpjidcl  20001  pgpfaclem3  20026  simpgnideld  20042  c0ghm  20409  c0snghm  20412  dsmmsubg  21710  frlm0  21721  mdetunilem7  22574  istgp2  24047  cyc3genpm  33245  isarchi3  33280  reofld  33435  lbslsat  33793  dimkerim  33804  fedgmullem2  33807  primrootscoprbij  42461  grpods  42553  pwssplit4  43435  pwslnmlem2  43439  lcoel0  48777