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

Theorem grpidcl 15557
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 15541 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpidcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpidcl.o . . 3  |-  .0.  =  ( 0g `  G )
42, 3mndidcl 15431 . 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 1369    e. wcel 1756   ` cfv 5413   Basecbs 14166   0gc0g 14370   Mndcmnd 15401   Grpcgrp 15402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-iota 5376  df-fun 5415  df-fv 5421  df-riota 6047  df-ov 6089  df-0g 14372  df-mnd 15407  df-grp 15536
This theorem is referenced by:  grpbn0  15558  grprcan  15562  grpid  15564  isgrpid2  15565  grprinv  15576  grpinvid  15580  grpidrcan  15582  grpidlcan  15583  grpidssd  15593  grpinvval2  15600  grpsubid1  15602  mulgcl  15635  mulgz  15639  imasgrp  15662  subg0  15678  subg0cl  15680  issubg4  15691  0subg  15697  nmzsubg  15713  eqgid  15724  divsgrp  15727  divs0  15730  ghmid  15744  ghmpreima  15759  ghmf1  15766  gafo  15805  gaid  15808  gass  15810  gaorber  15817  gastacl  15818  lactghmga  15900  cayleylem2  15909  symgsssg  15964  symgfisg  15965  od1  16051  gexdvds  16074  sylow1lem2  16089  sylow3lem1  16117  lsmdisj2  16170  0frgp  16267  odadd1  16321  torsubg  16327  oddvdssubg  16328  0cyg  16360  prmcyg  16361  dprdfadd  16500  dprdfaddOLD  16507  dprdz  16517  pgpfac1lem3a  16567  rng0cl  16656  rnglz  16671  rngrz  16672  isdrng2  16822  srng0  16925  lmod0vcl  16957  islmhm2  17099  psr0cl  17445  mplsubglem  17490  mplsubglemOLD  17492  evl1gsumd  17771  frgpcyg  17986  ip0l  18045  ocvlss  18077  grpvlinv  18275  mdet1  18388  mdetuni0  18407  istgp2  19642  cldsubg  19661  tgpconcompeqg  19662  tgpconcomp  19663  snclseqg  19666  tgphaus  19667  tgpt1  19668  divstgphaus  19673  tgptsmscls  19704  nrmmetd  20147  nmfval2  20163  nmval2  20164  nmf2  20165  ngpds3  20179  nmge0  20188  nmeq0  20189  nminv  20192  nmmtri  20193  nmrtri  20195  nm0  20198  tngnm  20217  idnghm  20302  nmcn  20401  nmoleub2lem2  20651  mdeg0  21521  dchrinv  22580  dchr1re  22582  dchrpt  22586  dchrsum2  22587  dchrhash  22590  rpvmasumlem  22716  rpvmasum2  22741  dchrisum0re  22742  ogrpinvOLD  26146  ogrpinv0lt  26154  ogrpinvlt  26155  isarchi3  26172  archirng  26173  archirngz  26174  archiabllem1b  26177  orngsqr  26240  ornglmulle  26241  orngrmulle  26242  ornglmullt  26243  orngrmullt  26244  orngmullt  26245  ofldchr  26250  isarchiofld  26253  kerf1hrm  26260  qqh0  26382  sconpi1  27097  ascl0  30781  evl1at0  30809  mat0dim0  30823  scmatsubcl  30844  mdetdiag  30867  lfl0f  32607  lkrlss  32633  lshpkrlem1  32648  lkrin  32702  dvhgrp  34645
  Copyright terms: Public domain W3C validator