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

Theorem grpidcl 14510
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 14494 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpidcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpidcl.o . . 3  |-  .0.  =  ( 0g `  G )
42, 3mndidcl 14391 . 2  |-  ( G  e.  Mnd  ->  .0.  e.  B )
51, 4syl 15 1  |-  ( G  e.  Grp  ->  .0.  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   ` cfv 5255   Basecbs 13148   0gc0g 13400   Mndcmnd 14361   Grpcgrp 14362
This theorem is referenced by:  grpbn0  14511  grprcan  14515  grpid  14517  isgrpid2  14518  grprinv  14529  grpinvid  14533  grpinvval2  14549  grpsubid1  14551  mulgcl  14584  mulgz  14588  imasgrp  14611  subg0  14627  subg0cl  14629  issubg4  14638  0subg  14642  nmzsubg  14658  eqgid  14669  divsgrp  14672  divs0  14675  ghmid  14689  ghmpreima  14704  ghmf1  14711  gafo  14750  gaid  14753  gass  14755  gaorber  14762  gastacl  14763  lactghmga  14784  cayleylem2  14788  od1  14872  gexdvds  14895  sylow1lem2  14910  sylow3lem1  14938  lsmdisj2  14991  0frgp  15088  odadd1  15140  torsubg  15146  oddvdssubg  15147  0cyg  15179  prmcyg  15180  dprdfadd  15255  dprdsubg  15259  dprdz  15265  pgpfac1lem3a  15311  rng0cl  15362  rnglz  15377  rngrz  15378  isdrng2  15522  srng0  15625  lmod0vcl  15659  islmhm2  15795  psr0cl  16139  mplsubglem  16179  frgpcyg  16527  ip0l  16540  ocvlss  16572  istgp2  17774  cldsubg  17793  tgpconcompeqg  17794  tgpconcomp  17795  snclseqg  17798  tgphaus  17799  tgpt1  17800  divstgphaus  17805  tgptsmscls  17832  nrmmetd  18097  nmfval2  18113  nmval2  18114  nmf2  18115  ngpds3  18129  nmge0  18138  nmeq0  18139  nminv  18142  nmmtri  18143  nmrtri  18145  nm0  18148  tngnm  18167  idnghm  18252  nmcn  18349  nmoleub2lem2  18597  mdeg0  19456  dchrinv  20500  dchr1re  20502  dchrpt  20506  dchrsum2  20507  dchrhash  20510  rpvmasumlem  20636  rpvmasum2  20661  dchrisum0re  20662  sconpi1  23770  symgsssg  27408  symgfisg  27409  grpvlinv  27450  lfl0f  29259  lkrlss  29285  lshpkrlem1  29300  lkrin  29354  dvhgrp  31297
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fv 5263  df-ov 5861  df-riota 6304  df-0g 13404  df-mnd 14367  df-grp 14489
  Copyright terms: Public domain W3C validator