Theorem grpmnd 18872

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 18871	. 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 6511  (class class class)co 7387  Basecbs 17179  +_gcplusg 17220  0_gc0g 17402  Mndcmnd 18661  Grpcgrp 18865

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-grp 18868

This theorem is referenced by:  grpcl  18873  grpass  18874  grpideu  18876  grpmndd  18878  grpplusf  18880  grpplusfo  18881  grpsgrp  18892  dfgrp2  18894  grpidcl  18897  grplid  18899  grprid  18900  dfgrp3  18971  prdsgrpd  18982  prdsinvgd  18983  mulgaddcom  19030  mulginvcom  19031  mulgz  19034  mulgneg2  19040  mulgass  19043  issubg3  19076  grpissubg  19078  0subg  19083  subgacs  19093  0ghm  19162  pwsdiagghm  19176  cntzsubg  19271  oppggrp  19289  symgsubmefmndALT  19333  psgnunilem5  19424  psgnuni  19429  0subgALT  19498  lsmcntzr  19610  pj1ghm  19633  isabl2  19720  cntrabl  19773  dprdfid  19949  dprdfeq0  19954  dprdlub  19958  dmdprdsplitlem  19969  dprddisj2  19971  dpjidcl  19990  pgpfaclem3  20015  simpgnideld  20031  c0ghm  20370  c0snghm  20373  dsmmsubg  21652  frlm0  21663  mdetunilem7  22505  istgp2  23978  cyc3genpm  33109  isarchi3  33141  reofld  33315  lbslsat  33612  dimkerim  33623  fedgmullem2  33626  primrootscoprbij  42090  grpods  42182  pwssplit4  43078  pwslnmlem2  43082  lcoel0  48417