Theorem grpmnd 18914

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ∀wral 3054  ∃wrex 3064  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  +_gcplusg 17218  0_gc0g 17400  Mndcmnd 18700  Grpcgrp 18907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-grp 18910

This theorem is referenced by:  grpcl  18915  grpass  18916  grpideu  18918  grpmndd  18920  grpplusf  18922  grpplusfo  18923  grpsgrp  18934  dfgrp2  18936  grpidcl  18939  grplid  18941  grprid  18942  dfgrp3  19013  prdsgrpd  19024  prdsinvgd  19025  mulgaddcom  19072  mulginvcom  19073  mulgz  19076  mulgneg2  19082  mulgass  19085  issubg3  19118  grpissubg  19120  0subg  19125  subgacs  19134  0ghm  19203  pwsdiagghm  19217  cntzsubg  19312  oppggrp  19330  symgsubmefmndALT  19376  psgnunilem5  19467  psgnuni  19472  0subgALT  19541  lsmcntzr  19653  pj1ghm  19676  isabl2  19763  cntrabl  19816  dprdfid  19992  dprdfeq0  19997  dprdlub  20001  dmdprdsplitlem  20012  dprddisj2  20014  dpjidcl  20033  pgpfaclem3  20058  simpgnideld  20074  c0ghm  20439  c0snghm  20442  dsmmsubg  21725  frlm0  21736  mdetunilem7  22608  istgp2  24081  cyc3genpm  33240  isarchi3  33275  reofld  33433  lbslsat  33807  dimkerim  33818  fedgmullem2  33821  primrootscoprbij  42588  grpods  42680  pwssplit4  43535  pwslnmlem2  43539  lcoel0  48920