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

Theorem grpidcl 16402
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  |-  B  =  ( Base `  G
)
grpidcl.o  |-  .0.  =  ( 0g `  G )
Assertion
Ref Expression
grpidcl  |-  ( G  e.  Grp  ->  .0.  e.  B )

Proof of Theorem grpidcl
StepHypRef Expression
1 grpmnd 16386 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpidcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpidcl.o . . 3  |-  .0.  =  ( 0g `  G )
42, 3mndidcl 16262 . 2  |-  ( G  e.  Mnd  ->  .0.  e.  B )
51, 4syl 17 1  |-  ( G  e.  Grp  ->  .0.  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1405    e. wcel 1842   ` cfv 5569   Basecbs 14841   0gc0g 15054   Mndcmnd 16243   Grpcgrp 16377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-reu 2761  df-rmo 2762  df-rab 2763  df-v 3061  df-sbc 3278  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-iota 5533  df-fun 5571  df-fv 5577  df-riota 6240  df-ov 6281  df-0g 15056  df-mgm 16196  df-sgrp 16235  df-mnd 16245  df-grp 16381
This theorem is referenced by:  grpbn0  16403  grprcan  16407  grpid  16409  isgrpid2  16410  grprinv  16421  grpinvid  16425  grpidrcan  16427  grpidlcan  16428  grpidssd  16438  grpinvval2  16445  grpsubid1  16447  mulgcl  16483  mulgz  16487  imasgrp  16510  subg0  16531  subg0cl  16533  issubg4  16544  0subg  16550  nmzsubg  16566  eqgid  16577  qusgrp  16580  qus0  16583  ghmid  16597  ghmpreima  16612  ghmf1  16619  gafo  16658  gaid  16661  gass  16663  gaorber  16670  gastacl  16671  lactghmga  16753  cayleylem2  16762  symgsssg  16816  symgfisg  16817  od1  16905  gexdvds  16928  sylow1lem2  16943  sylow3lem1  16971  lsmdisj2  17024  0frgp  17121  odadd1  17178  torsubg  17184  oddvdssubg  17185  0cyg  17219  prmcyg  17220  telgsums  17342  dprdfadd  17380  dprdfaddOLD  17387  dprdz  17397  pgpfac1lem3a  17447  ring0cl  17540  ringlz  17555  ringrz  17556  kerf1hrm  17712  isdrng2  17726  srng0  17829  lmod0vcl  17861  islmhm2  18004  psr0cl  18367  mplsubglem  18413  mplsubglemOLD  18415  evl1gsumd  18713  frgpcyg  18910  ip0l  18969  ocvlss  19001  grpvlinv  19189  matinvgcell  19229  mat0dim0  19261  mdetdiag  19393  mdetuni0  19415  chpdmatlem2  19632  chp0mat  19639  istgp2  20882  cldsubg  20901  tgpconcompeqg  20902  tgpconcomp  20903  snclseqg  20906  tgphaus  20907  tgpt1  20908  qustgphaus  20913  tgptsmscls  20944  nrmmetd  21387  nmfval2  21403  nmval2  21404  nmf2  21405  ngpds3  21419  nmge0  21428  nmeq0  21429  nminv  21432  nmmtri  21433  nmrtri  21435  nm0  21438  tngnm  21457  idnghm  21542  nmcn  21641  nmoleub2lem2  21891  mdeg0  22762  dchrinv  23917  dchr1re  23919  dchrpt  23923  dchrsum2  23924  dchrhash  23927  rpvmasumlem  24053  rpvmasum2  24078  dchrisum0re  24079  ogrpinvOLD  28157  ogrpinv0lt  28165  ogrpinvlt  28166  isarchi3  28183  archirng  28184  archirngz  28185  archiabllem1b  28188  orngsqr  28247  ornglmulle  28248  orngrmulle  28249  ornglmullt  28250  orngrmullt  28251  orngmullt  28252  ofldchr  28257  isarchiofld  28260  qqh0  28417  sconpi1  29536  lfl0f  32087  lkrlss  32113  lshpkrlem1  32128  lkrin  32182  dvhgrp  34127  rnglz  38201  zrrnghm  38234  ascl0  38488  evl1at0  38502
  Copyright terms: Public domain W3C validator