Theorem grpmnd 18888

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  ∀wral 3056  ∃wrex 3065  ‘cfv 6542  (class class class)co 7414  Basecbs 17171  +_gcplusg 17224  0_gc0g 17412  Mndcmnd 18685  Grpcgrp 18881

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 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-iota 6494  df-fv 6550  df-ov 7417  df-grp 18884

This theorem is referenced by:  grpcl  18889  grpass  18890  grpideu  18892  grpmndd  18894  grpplusf  18896  grpplusfo  18897  grpsgrp  18908  dfgrp2  18910  grpidcl  18913  grplid  18915  grprid  18916  dfgrp3  18986  prdsgrpd  18997  prdsinvgd  18998  mulgaddcom  19044  mulginvcom  19045  mulgz  19048  mulgneg2  19054  mulgass  19057  issubg3  19090  grpissubg  19092  0subg  19097  subgacs  19107  0ghm  19175  pwsdiagghm  19189  cntzsubg  19281  oppggrp  19302  symgsubmefmndALT  19349  psgnunilem5  19440  psgnuni  19445  0subgALT  19514  lsmcntzr  19626  pj1ghm  19649  isabl2  19736  cntrabl  19789  dprdfid  19965  dprdfeq0  19970  dprdlub  19974  dmdprdsplitlem  19985  dprddisj2  19987  dpjidcl  20006  pgpfaclem3  20031  simpgnideld  20047  c0ghm  20389  c0snghm  20392  dsmmsubg  21664  frlm0  21675  mdetunilem7  22507  istgp2  23982  cyc3genpm  32851  isarchi3  32873  reofld  32996  lbslsat  33246  dimkerim  33257  fedgmullem2  33260  primrootscoprbij  41509  pwssplit4  42435  pwslnmlem2  42439  lcoel0  47419