Theorem grpmnd 19068

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 2762	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		eqid 2762	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
3		eqid 2762	. . 3 ⊢ (0g‘𝐺) = (0g‘𝐺)
4	1, 2, 3	isgrp 19067	. 2 ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Mnd ∧ ∀𝑎 ∈ (Base‘𝐺)∃𝑚 ∈ (Base‘𝐺)(𝑚(+g‘𝐺)𝑎) = (0g‘𝐺)))
5	4	simplbi 502	1 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3078  ∃wrex 3088  ‘cfv 6537  (class class class)co 7416  Basecbs 17305  +_gcplusg 17346  0_gc0g 17528  Mndcmnd 18840  Grpcgrp 19061

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419  df-grp 19064

This theorem is used by:  grpcl  19069  grpass  19070  grpideu  19072  grpmndd  19074  grpplusf  19076  grpplusfo  19077  grpsgrp  19088  dfgrp2  19090  grpidcl  19093  grplid  19095  grprid  19096  dfgrp3  19166  prdsgrpd  19177  prdsinvgd  19178  mulgaddcom  19225  mulginvcom  19226  mulgz  19229  mulgneg2  19235  mulgass  19238  issubg3  19272  grpissubg  19274  0subg  19279  subgacs  19288  0ghm  19361  pwsdiagghm  19375  cntzsubg  19470  oppggrp  19488  symgsubmefmndALT  19534  psgnunilem5  19625  psgnuni  19630  0subgALT  19699  lsmcntzr  19811  pj1ghm  19834  isabl2  19921  cntrabl  19974  dprdfid  20150  dprdfeq0  20155  dprdlub  20159  dmdprdsplitlem  20170  dprddisj2  20172  dpjidcl  20191  pgpfaclem3  20216  simpgnideld  20232  c0ghm  20606  c0snghm  20609  dsmmsubg  21960  frlm0  21971  mdetunilem7  22844  istgp2  24321  cyc3genpm  33594  isarchi3  33629  reofld  33785  lbslsat  34128  dimkerim  34139  fedgmullem2  34142  primrootscoprbij  42970  grpods  43062  pwssplit4  43932  pwslnmlem2  43936  lcoel0  49360