Theorem grpmnd 19180

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 2763	. . 3 ⊢ (Base‘𝐺) = (Base‘𝐺)
2		eqid 2763	. . 3 ⊢ (+g‘𝐺) = (+g‘𝐺)
3		eqid 2763	. . 3 ⊢ (0g‘𝐺) = (0g‘𝐺)
4	1, 2, 3	isgrp 19179	. 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 2147  ∀wral 3080  ∃wrex 3090  ‘cfv 6558  (class class class)co 7443  Basecbs 17416  +_gcplusg 17457  0_gc0g 17639  Mndcmnd 18952  Grpcgrp 19173

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446  df-grp 19176

This theorem is used by:  grpcl  19181  grpass  19182  grpideu  19184  grpmndd  19186  grpplusf  19188  grpplusfo  19189  grpsgrp  19200  dfgrp2  19202  grpidcl  19205  grplid  19207  grprid  19208  dfgrp3  19278  prdsgrpd  19289  prdsinvgd  19290  mulgaddcom  19337  mulginvcom  19338  mulgz  19341  mulgneg2  19347  mulgass  19350  issubg3  19384  grpissubg  19386  0subg  19391  subgacs  19400  0ghm  19473  pwsdiagghm  19487  cntzsubg  19583  oppggrp  19601  symgsubmefmndALT  19647  psgnunilem5  19738  psgnuni  19743  0subgALT  19812  lsmcntzr  19924  pj1ghm  19947  isabl2  20034  cntrabl  20087  dprdfid  20263  dprdfeq0  20268  dprdlub  20272  dmdprdsplitlem  20283  dprddisj2  20285  dpjidcl  20304  pgpfaclem3  20329  simpgnideld  20345  c0ghm  20721  c0snghm  20724  dsmmsubg  22079  frlm0  22090  mdetunilem7  22963  istgp2  24440  cyc3genpm  33783  isarchi3  33818  reofld  33974  lbslsat  34318  dimkerim  34329  fedgmullem2  34332  primrootscoprbij  43344  grpods  43436  pwssplit4  44284  pwslnmlem2  44288  lcoel0  49745