Theorem grpmnd 18916

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 18915	. 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 6499  (class class class)co 7367  Basecbs 17179  +_gcplusg 17220  0_gc0g 17402  Mndcmnd 18702  Grpcgrp 18909

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 6455  df-fv 6507  df-ov 7370  df-grp 18912

This theorem is referenced by:  grpcl  18917  grpass  18918  grpideu  18920  grpmndd  18922  grpplusf  18924  grpplusfo  18925  grpsgrp  18936  dfgrp2  18938  grpidcl  18941  grplid  18943  grprid  18944  dfgrp3  19015  prdsgrpd  19026  prdsinvgd  19027  mulgaddcom  19074  mulginvcom  19075  mulgz  19078  mulgneg2  19084  mulgass  19087  issubg3  19120  grpissubg  19122  0subg  19127  subgacs  19136  0ghm  19205  pwsdiagghm  19219  cntzsubg  19314  oppggrp  19332  symgsubmefmndALT  19378  psgnunilem5  19469  psgnuni  19474  0subgALT  19543  lsmcntzr  19655  pj1ghm  19678  isabl2  19765  cntrabl  19818  dprdfid  19994  dprdfeq0  19999  dprdlub  20003  dmdprdsplitlem  20014  dprddisj2  20016  dpjidcl  20035  pgpfaclem3  20060  simpgnideld  20076  c0ghm  20441  c0snghm  20444  dsmmsubg  21723  frlm0  21734  mdetunilem7  22583  istgp2  24056  cyc3genpm  33213  isarchi3  33248  reofld  33403  lbslsat  33760  dimkerim  33771  fedgmullem2  33774  primrootscoprbij  42541  grpods  42633  pwssplit4  43517  pwslnmlem2  43521  lcoel0  48898