Theorem grpmnd 18769

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ∀wral 3060  ∃wrex 3069  ‘cfv 6501  (class class class)co 7362  Basecbs 17094  +_gcplusg 17147  0_gc0g 17335  Mndcmnd 18570  Grpcgrp 18762

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-grp 18765

This theorem is referenced by:  grpcl  18770  grpass  18771  grpideu  18773  grpmndd  18774  grpplusf  18776  grpplusfo  18777  grpsgrp  18788  dfgrp2  18789  grpidcl  18792  grplid  18794  grprid  18795  dfgrp3  18860  prdsgrpd  18871  prdsinvgd  18872  mulgaddcom  18914  mulginvcom  18915  mulgz  18918  mulgneg2  18924  mulgass  18927  issubg3  18960  grpissubg  18962  0subg  18967  subgacs  18977  0ghm  19036  pwsdiagghm  19050  cntzsubg  19131  oppggrp  19152  symgsubmefmndALT  19199  psgnunilem5  19290  psgnuni  19295  0subgALT  19364  lsmcntzr  19476  pj1ghm  19499  isabl2  19586  cntrabl  19635  dprdfid  19810  dprdfeq0  19815  dprdlub  19819  dmdprdsplitlem  19830  dprddisj2  19832  dpjidcl  19851  pgpfaclem3  19876  simpgnideld  19892  dsmmsubg  21186  frlm0  21197  mdetunilem7  22004  istgp2  23479  cyc3genpm  32071  isarchi3  32093  ofldchr  32180  reofld  32207  lbslsat  32398  dimkerim  32409  fedgmullem2  32412  pwssplit4  41474  pwslnmlem2  41478  c0ghm  46329  c0snghm  46334  lcoel0  46629