Theorem grpmnd 19013

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142  ∀wral 3078  ∃wrex 3088  ‘cfv 6536  (class class class)co 7412  Basecbs 17275  +_gcplusg 17316  0_gc0g 17498  Mndcmnd 18798  Grpcgrp 19006

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7415  df-grp 19009

This theorem is used by:  grpcl  19014  grpass  19015  grpideu  19017  grpmndd  19019  grpplusf  19021  grpplusfo  19022  grpsgrp  19033  dfgrp2  19035  grpidcl  19038  grplid  19040  grprid  19041  dfgrp3  19111  prdsgrpd  19122  prdsinvgd  19123  mulgaddcom  19170  mulginvcom  19171  mulgz  19174  mulgneg2  19180  mulgass  19183  issubg3  19217  grpissubg  19219  0subg  19224  subgacs  19233  0ghm  19306  pwsdiagghm  19320  cntzsubg  19415  oppggrp  19433  symgsubmefmndALT  19479  psgnunilem5  19570  psgnuni  19575  0subgALT  19644  lsmcntzr  19756  pj1ghm  19779  isabl2  19866  cntrabl  19919  dprdfid  20095  dprdfeq0  20100  dprdlub  20104  dmdprdsplitlem  20115  dprddisj2  20117  dpjidcl  20136  pgpfaclem3  20161  simpgnideld  20177  c0ghm  20550  c0snghm  20553  dsmmsubg  21904  frlm0  21915  mdetunilem7  22786  istgp2  24259  cyc3genpm  33481  isarchi3  33516  reofld  33672  lbslsat  34015  dimkerim  34026  fedgmullem2  34029  primrootscoprbij  42897  grpods  42989  pwssplit4  43844  pwslnmlem2  43848  lcoel0  49236