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

Theorem grpidcl 17273
Description: The identity element of a group belongs to the group. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
Hypotheses
Ref Expression
grpidcl.b 𝐵 = (Base‘𝐺)
grpidcl.o 0 = (0g𝐺)
Assertion
Ref Expression
grpidcl (𝐺 ∈ Grp → 0𝐵)

Proof of Theorem grpidcl
StepHypRef Expression
1 grpmnd 17252 . 2 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2 grpidcl.b . . 3 𝐵 = (Base‘𝐺)
3 grpidcl.o . . 3 0 = (0g𝐺)
42, 3mndidcl 17131 . 2 (𝐺 ∈ Mnd → 0𝐵)
51, 4syl 17 1 (𝐺 ∈ Grp → 0𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wcel 1977  cfv 5804  Basecbs 15695  0gc0g 15923  Mndcmnd 17117  Grpcgrp 17245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fv 5812  df-riota 6511  df-ov 6552  df-0g 15925  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-grp 17248
This theorem is referenced by:  grpbn0  17274  grprcan  17278  grpid  17280  isgrpid2  17281  grprinv  17292  grpidinv  17298  grpinvid  17299  grpidrcan  17303  grpidlcan  17304  grpidssd  17314  grpinvval2  17321  grpsubid1  17323  imasgrp  17354  mulgcl  17382  mulgz  17391  subg0  17423  subg0cl  17425  issubg4  17436  0subg  17442  nmzsubg  17458  eqgid  17469  qusgrp  17472  qus0  17475  ghmid  17489  ghmpreima  17505  ghmf1  17512  gafo  17552  gaid  17555  gass  17557  gaorber  17564  gastacl  17565  lactghmga  17647  cayleylem2  17656  symgsssg  17710  symgfisg  17711  od1  17799  gexdvds  17822  sylow1lem2  17837  sylow3lem1  17865  lsmdisj2  17918  0frgp  18015  odadd1  18074  torsubg  18080  oddvdssubg  18081  0cyg  18117  prmcyg  18118  telgsums  18213  dprdfadd  18242  dprdz  18252  pgpfac1lem3a  18298  ring0cl  18392  ringlz  18410  ringrz  18411  kerf1hrm  18566  isdrng2  18580  srng0  18683  lmod0vcl  18715  islmhm2  18859  psr0cl  19215  mplsubglem  19255  evl1gsumd  19542  frgpcyg  19741  ip0l  19800  ocvlss  19835  grpvlinv  20020  matinvgcell  20060  mat0dim0  20092  mdetdiag  20224  mdetuni0  20246  chpdmatlem2  20463  chp0mat  20470  istgp2  21705  cldsubg  21724  tgpconcompeqg  21725  tgpconcomp  21726  snclseqg  21729  tgphaus  21730  tgpt1  21731  qustgphaus  21736  tgptsmscls  21763  nrmmetd  22189  nmfval2  22205  nmval2  22206  nmf2  22207  ngpds3  22222  nmge0  22231  nmeq0  22232  nminv  22235  nmmtri  22236  nmrtri  22238  nm0  22243  tngnm  22265  idnghm  22357  nmcn  22455  clmvz  22719  nmoleub2lem2  22724  nglmle  22908  mdeg0  23634  dchrinv  24786  dchr1re  24788  dchrpt  24792  dchrsum2  24793  dchrhash  24796  rpvmasumlem  24976  rpvmasum2  25001  dchrisum0re  25002  ogrpinvOLD  29046  ogrpinv0lt  29054  ogrpinvlt  29055  isarchi3  29072  archirng  29073  archirngz  29074  archiabllem1b  29077  orngsqr  29135  ornglmulle  29136  orngrmulle  29137  ornglmullt  29138  orngrmullt  29139  orngmullt  29140  ofldchr  29145  isarchiofld  29148  qqh0  29356  sconpi1  30475  lfl0f  33374  lkrlss  33400  lshpkrlem1  33415  lkrin  33469  dvhgrp  35414  rnglz  41674  zrrnghm  41707  ascl0  41959  evl1at0  41973
  Copyright terms: Public domain W3C validator