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

Theorem grpidcl 15872
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 15856 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpidcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpidcl.o . . 3  |-  .0.  =  ( 0g `  G )
42, 3mndidcl 15745 . 2  |-  ( G  e.  Mnd  ->  .0.  e.  B )
51, 4syl 16 1  |-  ( G  e.  Grp  ->  .0.  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374    e. wcel 1762   ` cfv 5579   Basecbs 14479   0gc0g 14684   Mndcmnd 15715   Grpcgrp 15716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-iota 5542  df-fun 5581  df-fv 5587  df-riota 6236  df-ov 6278  df-0g 14686  df-mnd 15721  df-grp 15851
This theorem is referenced by:  grpbn0  15873  grprcan  15877  grpid  15879  isgrpid2  15880  grprinv  15891  grpinvid  15895  grpidrcan  15897  grpidlcan  15898  grpidssd  15908  grpinvval2  15915  grpsubid1  15917  mulgcl  15952  mulgz  15956  imasgrp  15979  subg0  15995  subg0cl  15997  issubg4  16008  0subg  16014  nmzsubg  16030  eqgid  16041  divsgrp  16044  divs0  16047  ghmid  16061  ghmpreima  16076  ghmf1  16083  gafo  16122  gaid  16125  gass  16127  gaorber  16134  gastacl  16135  lactghmga  16217  cayleylem2  16226  symgsssg  16281  symgfisg  16282  od1  16370  gexdvds  16393  sylow1lem2  16408  sylow3lem1  16436  lsmdisj2  16489  0frgp  16586  odadd1  16640  torsubg  16646  oddvdssubg  16647  0cyg  16679  prmcyg  16680  telgsums  16806  dprdfadd  16843  dprdfaddOLD  16850  dprdz  16860  pgpfac1lem3a  16910  rng0cl  17000  rnglz  17015  rngrz  17016  kerf1hrm  17168  isdrng2  17182  srng0  17285  lmod0vcl  17317  islmhm2  17460  psr0cl  17811  mplsubglem  17857  mplsubglemOLD  17859  evl1gsumd  18157  frgpcyg  18372  ip0l  18431  ocvlss  18463  grpvlinv  18657  matinvgcell  18697  mat0dim0  18729  mdetdiag  18861  mdetuni0  18883  chpdmatlem2  19100  chp0mat  19107  istgp2  20318  cldsubg  20337  tgpconcompeqg  20338  tgpconcomp  20339  snclseqg  20342  tgphaus  20343  tgpt1  20344  divstgphaus  20349  tgptsmscls  20380  nrmmetd  20823  nmfval2  20839  nmval2  20840  nmf2  20841  ngpds3  20855  nmge0  20864  nmeq0  20865  nminv  20868  nmmtri  20869  nmrtri  20871  nm0  20874  tngnm  20893  idnghm  20978  nmcn  21077  nmoleub2lem2  21327  mdeg0  22198  dchrinv  23257  dchr1re  23259  dchrpt  23263  dchrsum2  23264  dchrhash  23267  rpvmasumlem  23393  rpvmasum2  23418  dchrisum0re  23419  ogrpinvOLD  27217  ogrpinv0lt  27225  ogrpinvlt  27226  isarchi3  27243  archirng  27244  archirngz  27245  archiabllem1b  27248  orngsqr  27307  ornglmulle  27308  orngrmulle  27309  ornglmullt  27310  orngrmullt  27311  orngmullt  27312  ofldchr  27317  isarchiofld  27320  qqh0  27451  sconpi1  28174  ascl0  31925  evl1at0  31939  lfl0f  33741  lkrlss  33767  lshpkrlem1  33782  lkrin  33836  dvhgrp  35779
  Copyright terms: Public domain W3C validator