Theorem grpmnd 18959

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  ∀wral 3060  ∃wrex 3069  ‘cfv 6560  (class class class)co 7432  Basecbs 17248  +_gcplusg 17298  0_gc0g 17485  Mndcmnd 18748  Grpcgrp 18952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-ov 7435  df-grp 18955

This theorem is referenced by:  grpcl  18960  grpass  18961  grpideu  18963  grpmndd  18965  grpplusf  18967  grpplusfo  18968  grpsgrp  18979  dfgrp2  18981  grpidcl  18984  grplid  18986  grprid  18987  dfgrp3  19058  prdsgrpd  19069  prdsinvgd  19070  mulgaddcom  19117  mulginvcom  19118  mulgz  19121  mulgneg2  19127  mulgass  19130  issubg3  19163  grpissubg  19165  0subg  19170  subgacs  19180  0ghm  19249  pwsdiagghm  19263  cntzsubg  19358  oppggrp  19377  symgsubmefmndALT  19422  psgnunilem5  19513  psgnuni  19518  0subgALT  19587  lsmcntzr  19699  pj1ghm  19722  isabl2  19809  cntrabl  19862  dprdfid  20038  dprdfeq0  20043  dprdlub  20047  dmdprdsplitlem  20058  dprddisj2  20060  dpjidcl  20079  pgpfaclem3  20104  simpgnideld  20120  c0ghm  20462  c0snghm  20465  dsmmsubg  21764  frlm0  21775  mdetunilem7  22625  istgp2  24100  cyc3genpm  33173  isarchi3  33195  reofld  33373  lbslsat  33668  dimkerim  33679  fedgmullem2  33682  primrootscoprbij  42104  grpods  42196  pwssplit4  43106  pwslnmlem2  43110  lcoel0  48350