Theorem grpmnd 19113

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3076  ∃wrex 3086  ‘cfv 6527  (class class class)co 7408  Basecbs 17349  +_gcplusg 17390  0_gc0g 17572  Mndcmnd 18885  Grpcgrp 19106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6483  df-fv 6535  df-ov 7411  df-grp 19109

This theorem is used by:  grpcl  19114  grpass  19115  grpideu  19117  grpmndd  19119  grpplusf  19121  grpplusfo  19122  grpsgrp  19133  dfgrp2  19135  grpidcl  19138  grplid  19140  grprid  19141  dfgrp3  19211  prdsgrpd  19222  prdsinvgd  19223  mulgaddcom  19270  mulginvcom  19271  mulgz  19274  mulgneg2  19280  mulgass  19283  issubg3  19317  grpissubg  19319  0subg  19324  subgacs  19333  0ghm  19406  pwsdiagghm  19420  cntzsubg  19515  oppggrp  19533  symgsubmefmndALT  19579  psgnunilem5  19670  psgnuni  19675  0subgALT  19744  lsmcntzr  19856  pj1ghm  19879  isabl2  19966  cntrabl  20019  dprdfid  20195  dprdfeq0  20200  dprdlub  20204  dmdprdsplitlem  20215  dprddisj2  20217  dpjidcl  20236  pgpfaclem3  20261  simpgnideld  20277  c0ghm  20653  c0snghm  20656  dsmmsubg  22011  frlm0  22022  mdetunilem7  22895  istgp2  24372  cyc3genpm  33647  isarchi3  33682  reofld  33838  lbslsat  34182  dimkerim  34193  fedgmullem2  34196  primrootscoprbij  43072  grpods  43164  pwssplit4  44034  pwslnmlem2  44038  lcoel0  49462