Theorem grpmnd 18837

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  ‘cfv 6486  (class class class)co 7353  Basecbs 17138  +_gcplusg 17179  0_gc0g 17361  Mndcmnd 18626  Grpcgrp 18830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356  df-grp 18833

This theorem is referenced by:  grpcl  18838  grpass  18839  grpideu  18841  grpmndd  18843  grpplusf  18845  grpplusfo  18846  grpsgrp  18857  dfgrp2  18859  grpidcl  18862  grplid  18864  grprid  18865  dfgrp3  18936  prdsgrpd  18947  prdsinvgd  18948  mulgaddcom  18995  mulginvcom  18996  mulgz  18999  mulgneg2  19005  mulgass  19008  issubg3  19041  grpissubg  19043  0subg  19048  subgacs  19058  0ghm  19127  pwsdiagghm  19141  cntzsubg  19236  oppggrp  19254  symgsubmefmndALT  19300  psgnunilem5  19391  psgnuni  19396  0subgALT  19465  lsmcntzr  19577  pj1ghm  19600  isabl2  19687  cntrabl  19740  dprdfid  19916  dprdfeq0  19921  dprdlub  19925  dmdprdsplitlem  19936  dprddisj2  19938  dpjidcl  19957  pgpfaclem3  19982  simpgnideld  19998  c0ghm  20364  c0snghm  20367  dsmmsubg  21668  frlm0  21679  mdetunilem7  22521  istgp2  23994  cyc3genpm  33107  isarchi3  33139  reofld  33291  lbslsat  33588  dimkerim  33599  fedgmullem2  33602  primrootscoprbij  42075  grpods  42167  pwssplit4  43062  pwslnmlem2  43066  lcoel0  48401