Theorem grpmnd 18905

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  ‘cfv 6490  (class class class)co 7358  Basecbs 17168  +_gcplusg 17209  0_gc0g 17391  Mndcmnd 18691  Grpcgrp 18898

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 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361  df-grp 18901

This theorem is referenced by:  grpcl  18906  grpass  18907  grpideu  18909  grpmndd  18911  grpplusf  18913  grpplusfo  18914  grpsgrp  18925  dfgrp2  18927  grpidcl  18930  grplid  18932  grprid  18933  dfgrp3  19004  prdsgrpd  19015  prdsinvgd  19016  mulgaddcom  19063  mulginvcom  19064  mulgz  19067  mulgneg2  19073  mulgass  19076  issubg3  19109  grpissubg  19111  0subg  19116  subgacs  19125  0ghm  19194  pwsdiagghm  19208  cntzsubg  19303  oppggrp  19321  symgsubmefmndALT  19367  psgnunilem5  19458  psgnuni  19463  0subgALT  19532  lsmcntzr  19644  pj1ghm  19667  isabl2  19754  cntrabl  19807  dprdfid  19983  dprdfeq0  19988  dprdlub  19992  dmdprdsplitlem  20003  dprddisj2  20005  dpjidcl  20024  pgpfaclem3  20049  simpgnideld  20065  c0ghm  20430  c0snghm  20433  dsmmsubg  21731  frlm0  21742  mdetunilem7  22592  istgp2  24065  cyc3genpm  33233  isarchi3  33268  reofld  33423  lbslsat  33781  dimkerim  33792  fedgmullem2  33795  primrootscoprbij  42552  grpods  42644  pwssplit4  43532  pwslnmlem2  43536  lcoel0  48901