Theorem grpmnd 18863

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∀wral 3049  ∃wrex 3058  ‘cfv 6489  (class class class)co 7355  Basecbs 17130  +_gcplusg 17171  0_gc0g 17353  Mndcmnd 18652  Grpcgrp 18856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-grp 18859

This theorem is referenced by:  grpcl  18864  grpass  18865  grpideu  18867  grpmndd  18869  grpplusf  18871  grpplusfo  18872  grpsgrp  18883  dfgrp2  18885  grpidcl  18888  grplid  18890  grprid  18891  dfgrp3  18962  prdsgrpd  18973  prdsinvgd  18974  mulgaddcom  19021  mulginvcom  19022  mulgz  19025  mulgneg2  19031  mulgass  19034  issubg3  19067  grpissubg  19069  0subg  19074  subgacs  19083  0ghm  19152  pwsdiagghm  19166  cntzsubg  19261  oppggrp  19279  symgsubmefmndALT  19325  psgnunilem5  19416  psgnuni  19421  0subgALT  19490  lsmcntzr  19602  pj1ghm  19625  isabl2  19712  cntrabl  19765  dprdfid  19941  dprdfeq0  19946  dprdlub  19950  dmdprdsplitlem  19961  dprddisj2  19963  dpjidcl  19982  pgpfaclem3  20007  simpgnideld  20023  c0ghm  20389  c0snghm  20392  dsmmsubg  21690  frlm0  21701  mdetunilem7  22543  istgp2  24016  cyc3genpm  33132  isarchi3  33167  reofld  33319  lbslsat  33640  dimkerim  33651  fedgmullem2  33654  primrootscoprbij  42205  grpods  42297  pwssplit4  43196  pwslnmlem2  43200  lcoel0  48543