Theorem grpmnd 18928

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3052  ∃wrex 3061  ‘cfv 6536  (class class class)co 7410  Basecbs 17233  +_gcplusg 17276  0_gc0g 17458  Mndcmnd 18717  Grpcgrp 18921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-grp 18924

This theorem is referenced by:  grpcl  18929  grpass  18930  grpideu  18932  grpmndd  18934  grpplusf  18936  grpplusfo  18937  grpsgrp  18948  dfgrp2  18950  grpidcl  18953  grplid  18955  grprid  18956  dfgrp3  19027  prdsgrpd  19038  prdsinvgd  19039  mulgaddcom  19086  mulginvcom  19087  mulgz  19090  mulgneg2  19096  mulgass  19099  issubg3  19132  grpissubg  19134  0subg  19139  subgacs  19149  0ghm  19218  pwsdiagghm  19232  cntzsubg  19327  oppggrp  19345  symgsubmefmndALT  19389  psgnunilem5  19480  psgnuni  19485  0subgALT  19554  lsmcntzr  19666  pj1ghm  19689  isabl2  19776  cntrabl  19829  dprdfid  20005  dprdfeq0  20010  dprdlub  20014  dmdprdsplitlem  20025  dprddisj2  20027  dpjidcl  20046  pgpfaclem3  20071  simpgnideld  20087  c0ghm  20426  c0snghm  20429  dsmmsubg  21708  frlm0  21719  mdetunilem7  22561  istgp2  24034  cyc3genpm  33168  isarchi3  33190  reofld  33364  lbslsat  33661  dimkerim  33672  fedgmullem2  33675  primrootscoprbij  42120  grpods  42212  pwssplit4  43088  pwslnmlem2  43092  lcoel0  48384