Theorem grpmnd 18874

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3061  ‘cfv 6493  (class class class)co 7360  Basecbs 17140  +_gcplusg 17181  0_gc0g 17363  Mndcmnd 18663  Grpcgrp 18867

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363  df-grp 18870

This theorem is referenced by:  grpcl  18875  grpass  18876  grpideu  18878  grpmndd  18880  grpplusf  18882  grpplusfo  18883  grpsgrp  18894  dfgrp2  18896  grpidcl  18899  grplid  18901  grprid  18902  dfgrp3  18973  prdsgrpd  18984  prdsinvgd  18985  mulgaddcom  19032  mulginvcom  19033  mulgz  19036  mulgneg2  19042  mulgass  19045  issubg3  19078  grpissubg  19080  0subg  19085  subgacs  19094  0ghm  19163  pwsdiagghm  19177  cntzsubg  19272  oppggrp  19290  symgsubmefmndALT  19336  psgnunilem5  19427  psgnuni  19432  0subgALT  19501  lsmcntzr  19613  pj1ghm  19636  isabl2  19723  cntrabl  19776  dprdfid  19952  dprdfeq0  19957  dprdlub  19961  dmdprdsplitlem  19972  dprddisj2  19974  dpjidcl  19993  pgpfaclem3  20018  simpgnideld  20034  c0ghm  20401  c0snghm  20404  dsmmsubg  21702  frlm0  21713  mdetunilem7  22566  istgp2  24039  cyc3genpm  33215  isarchi3  33250  reofld  33405  lbslsat  33754  dimkerim  33765  fedgmullem2  33768  primrootscoprbij  42393  grpods  42485  pwssplit4  43367  pwslnmlem2  43371  lcoel0  48710