Theorem grpmnd 19007

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095  ‘cfv 6537  (class class class)co 7411  Basecbs 17269  +_gcplusg 17310  0_gc0g 17492  Mndcmnd 18792  Grpcgrp 19000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5112  df-iota 6493  df-fv 6545  df-ov 7414  df-grp 19003

This theorem is referenced by:  grpcl  19008  grpass  19009  grpideu  19011  grpmndd  19013  grpplusf  19015  grpplusfo  19016  grpsgrp  19027  dfgrp2  19029  grpidcl  19032  grplid  19034  grprid  19035  dfgrp3  19105  prdsgrpd  19116  prdsinvgd  19117  mulgaddcom  19164  mulginvcom  19165  mulgz  19168  mulgneg2  19174  mulgass  19177  issubg3  19211  grpissubg  19213  0subg  19218  subgacs  19227  0ghm  19300  pwsdiagghm  19314  cntzsubg  19409  oppggrp  19427  symgsubmefmndALT  19473  psgnunilem5  19564  psgnuni  19569  0subgALT  19638  lsmcntzr  19750  pj1ghm  19773  isabl2  19860  cntrabl  19913  dprdfid  20089  dprdfeq0  20094  dprdlub  20098  dmdprdsplitlem  20109  dprddisj2  20111  dpjidcl  20130  pgpfaclem3  20155  simpgnideld  20171  c0ghm  20543  c0snghm  20546  dsmmsubg  21862  frlm0  21873  mdetunilem7  22744  istgp2  24217  cyc3genpm  33413  isarchi3  33448  reofld  33606  lbslsat  33951  dimkerim  33962  fedgmullem2  33965  primrootscoprbij  42794  grpods  42886  pwssplit4  43743  pwslnmlem2  43747  lcoel0  49128