Theorem grpmnd 18879

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3045  ∃wrex 3054  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  +_gcplusg 17227  0_gc0g 17409  Mndcmnd 18668  Grpcgrp 18872

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-grp 18875

This theorem is referenced by:  grpcl  18880  grpass  18881  grpideu  18883  grpmndd  18885  grpplusf  18887  grpplusfo  18888  grpsgrp  18899  dfgrp2  18901  grpidcl  18904  grplid  18906  grprid  18907  dfgrp3  18978  prdsgrpd  18989  prdsinvgd  18990  mulgaddcom  19037  mulginvcom  19038  mulgz  19041  mulgneg2  19047  mulgass  19050  issubg3  19083  grpissubg  19085  0subg  19090  subgacs  19100  0ghm  19169  pwsdiagghm  19183  cntzsubg  19278  oppggrp  19296  symgsubmefmndALT  19340  psgnunilem5  19431  psgnuni  19436  0subgALT  19505  lsmcntzr  19617  pj1ghm  19640  isabl2  19727  cntrabl  19780  dprdfid  19956  dprdfeq0  19961  dprdlub  19965  dmdprdsplitlem  19976  dprddisj2  19978  dpjidcl  19997  pgpfaclem3  20022  simpgnideld  20038  c0ghm  20377  c0snghm  20380  dsmmsubg  21659  frlm0  21670  mdetunilem7  22512  istgp2  23985  cyc3genpm  33116  isarchi3  33148  reofld  33322  lbslsat  33619  dimkerim  33630  fedgmullem2  33633  primrootscoprbij  42097  grpods  42189  pwssplit4  43085  pwslnmlem2  43089  lcoel0  48421