Theorem grpmnd 18958

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

Syntax hints:   → wi 4   = wceq 1554   ∈ wcel 2136  ∀wral 3070  ∃wrex 3080  ‘cfv 6510  (class class class)co 7385  Basecbs 17221  +_gcplusg 17262  0_gc0g 17444  Mndcmnd 18744  Grpcgrp 18951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-iota 6466  df-fv 6518  df-ov 7388  df-grp 18954

This theorem is referenced by:  grpcl  18959  grpass  18960  grpideu  18962  grpmndd  18964  grpplusf  18966  grpplusfo  18967  grpsgrp  18978  dfgrp2  18980  grpidcl  18983  grplid  18985  grprid  18986  dfgrp3  19057  prdsgrpd  19068  prdsinvgd  19069  mulgaddcom  19116  mulginvcom  19117  mulgz  19120  mulgneg2  19126  mulgass  19129  issubg3  19162  grpissubg  19164  0subg  19169  subgacs  19178  0ghm  19246  pwsdiagghm  19260  cntzsubg  19355  oppggrp  19373  symgsubmefmndALT  19419  psgnunilem5  19510  psgnuni  19515  0subgALT  19584  lsmcntzr  19696  pj1ghm  19719  isabl2  19806  cntrabl  19859  dprdfid  20035  dprdfeq0  20040  dprdlub  20044  dmdprdsplitlem  20055  dprddisj2  20057  dpjidcl  20076  pgpfaclem3  20101  simpgnideld  20117  c0ghm  20482  c0snghm  20485  dsmmsubg  21768  frlm0  21779  mdetunilem7  22651  istgp2  24124  cyc3genpm  33286  isarchi3  33321  reofld  33483  lbslsat  33867  dimkerim  33878  fedgmullem2  33881  primrootscoprbij  42667  grpods  42759  pwssplit4  43614  pwslnmlem2  43618  lcoel0  48998