Theorem grpmnd 18680

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ∀wral 3062  ∃wrex 3071  ‘cfv 6483  (class class class)co 7341  Basecbs 17009  +_gcplusg 17059  0_gc0g 17247  Mndcmnd 18482  Grpcgrp 18673

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-br 5097  df-iota 6435  df-fv 6491  df-ov 7344  df-grp 18676

This theorem is referenced by:  grpcl  18681  grpass  18682  grpideu  18684  grpmndd  18685  grpplusf  18687  grpplusfo  18688  grpsgrp  18699  dfgrp2  18700  grpidcl  18703  grplid  18705  grprid  18706  dfgrp3  18770  prdsgrpd  18781  prdsinvgd  18782  mulgaddcom  18823  mulginvcom  18824  mulgz  18827  mulgneg2  18833  mulgass  18836  issubg3  18869  grpissubg  18871  subgacs  18885  0ghm  18944  pwsdiagghm  18958  cntzsubg  19039  oppggrp  19060  symgsubmefmndALT  19107  psgnunilem5  19198  psgnuni  19203  lsmcntzr  19381  pj1ghm  19404  isabl2  19490  cntrabl  19539  dprdfid  19714  dprdfeq0  19719  dprdlub  19723  dmdprdsplitlem  19734  dprddisj2  19736  dpjidcl  19755  pgpfaclem3  19780  simpgnideld  19796  dsmmsubg  21055  frlm0  21066  mdetunilem7  21872  istgp2  23347  cyc3genpm  31704  isarchi3  31726  ofldchr  31811  reofld  31838  lbslsat  31995  dimkerim  32004  fedgmullem2  32007  pwssplit4  41228  pwslnmlem2  41232  c0ghm  45887  c0snghm  45892  lcoel0  46187