Theorem grpmnd 18499

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064  ‘cfv 6418  (class class class)co 7255  Basecbs 16840  +_gcplusg 16888  0_gc0g 17067  Mndcmnd 18300  Grpcgrp 18492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-grp 18495

This theorem is referenced by:  grpcl  18500  grpass  18501  grpideu  18503  grpmndd  18504  grpplusf  18506  grpplusfo  18507  grpsgrp  18518  dfgrp2  18519  grpidcl  18522  grplid  18524  grprid  18525  dfgrp3  18589  prdsgrpd  18600  prdsinvgd  18601  mulgaddcom  18642  mulginvcom  18643  mulgz  18646  mulgneg2  18652  mulgass  18655  issubg3  18688  grpissubg  18690  subgacs  18704  0ghm  18763  pwsdiagghm  18777  cntzsubg  18858  oppggrp  18879  symgsubmefmndALT  18926  psgnunilem5  19017  psgnuni  19022  lsmcntzr  19201  pj1ghm  19224  isabl2  19310  cntrabl  19359  dprdfid  19535  dprdfeq0  19540  dprdlub  19544  dmdprdsplitlem  19555  dprddisj2  19557  dpjidcl  19576  pgpfaclem3  19601  simpgnideld  19617  dsmmsubg  20860  frlm0  20871  mdetunilem7  21675  istgp2  23150  cyc3genpm  31321  isarchi3  31343  ofldchr  31415  reofld  31446  lbslsat  31601  dimkerim  31610  fedgmullem2  31613  pwssplit4  40830  pwslnmlem2  40834  c0ghm  45357  c0snghm  45362  lcoel0  45657