MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  grpmnd Structured version   Visualization version   GIF version

Theorem grpmnd 18756
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.
StepHypRef Expression
1 eqid 2737 . . 3 (Base‘𝐺) = (Base‘𝐺)
2 eqid 2737 . . 3 (+g𝐺) = (+g𝐺)
3 eqid 2737 . . 3 (0g𝐺) = (0g𝐺)
41, 2, 3isgrp 18755 . 2 (𝐺 ∈ Grp ↔ (𝐺 ∈ Mnd ∧ ∀𝑎 ∈ (Base‘𝐺)∃𝑚 ∈ (Base‘𝐺)(𝑚(+g𝐺)𝑎) = (0g𝐺)))
54simplbi 499 1 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  wral 3065  wrex 3074  cfv 6497  (class class class)co 7358  Basecbs 17084  +gcplusg 17134  0gc0g 17322  Mndcmnd 18557  Grpcgrp 18749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361  df-grp 18752
This theorem is referenced by:  grpcl  18757  grpass  18758  grpideu  18760  grpmndd  18761  grpplusf  18763  grpplusfo  18764  grpsgrp  18775  dfgrp2  18776  grpidcl  18779  grplid  18781  grprid  18782  dfgrp3  18847  prdsgrpd  18858  prdsinvgd  18859  mulgaddcom  18901  mulginvcom  18902  mulgz  18905  mulgneg2  18911  mulgass  18914  issubg3  18947  grpissubg  18949  0subg  18954  subgacs  18964  0ghm  19023  pwsdiagghm  19037  cntzsubg  19118  oppggrp  19139  symgsubmefmndALT  19186  psgnunilem5  19277  psgnuni  19282  0subgALT  19351  lsmcntzr  19463  pj1ghm  19486  isabl2  19573  cntrabl  19622  dprdfid  19797  dprdfeq0  19802  dprdlub  19806  dmdprdsplitlem  19817  dprddisj2  19819  dpjidcl  19838  pgpfaclem3  19863  simpgnideld  19879  dsmmsubg  21152  frlm0  21163  mdetunilem7  21970  istgp2  23445  cyc3genpm  32004  isarchi3  32026  ofldchr  32112  reofld  32139  lbslsat  32316  dimkerim  32325  fedgmullem2  32328  pwssplit4  41419  pwslnmlem2  41423  c0ghm  46216  c0snghm  46221  lcoel0  46516
  Copyright terms: Public domain W3C validator