Theorem grpmnd 19152

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086  ‘cfv 6538  (class class class)co 7420  Basecbs 17388  +_gcplusg 17429  0_gc0g 17611  Mndcmnd 18924  Grpcgrp 19145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423  df-grp 19148

This theorem is used by:  grpcl  19153  grpass  19154  grpideu  19156  grpmndd  19158  grpplusf  19160  grpplusfo  19161  grpsgrp  19172  dfgrp2  19174  grpidcl  19177  grplid  19179  grprid  19180  dfgrp3  19250  prdsgrpd  19261  prdsinvgd  19262  mulgaddcom  19309  mulginvcom  19310  mulgz  19313  mulgneg2  19319  mulgass  19322  issubg3  19356  grpissubg  19358  0subg  19363  subgacs  19372  0ghm  19445  pwsdiagghm  19459  cntzsubg  19554  oppggrp  19572  symgsubmefmndALT  19618  psgnunilem5  19709  psgnuni  19714  0subgALT  19783  lsmcntzr  19895  pj1ghm  19918  isabl2  20005  cntrabl  20058  dprdfid  20234  dprdfeq0  20239  dprdlub  20243  dmdprdsplitlem  20254  dprddisj2  20256  dpjidcl  20275  pgpfaclem3  20300  simpgnideld  20316  c0ghm  20692  c0snghm  20695  dsmmsubg  22050  frlm0  22061  mdetunilem7  22934  istgp2  24411  cyc3genpm  33756  isarchi3  33791  reofld  33947  lbslsat  34291  dimkerim  34302  fedgmullem2  34305  primrootscoprbij  43228  grpods  43320  pwssplit4  44167  pwslnmlem2  44171  lcoel0  49616