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

Theorem grpidcl 14796
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 14780 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpidcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpidcl.o . . 3  |-  .0.  =  ( 0g `  G )
42, 3mndidcl 14677 . 2  |-  ( G  e.  Mnd  ->  .0.  e.  B )
51, 4syl 16 1  |-  ( G  e.  Grp  ->  .0.  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721   ` cfv 5421   Basecbs 13432   0gc0g 13686   Mndcmnd 14647   Grpcgrp 14648
This theorem is referenced by:  grpbn0  14797  grprcan  14801  grpid  14803  isgrpid2  14804  grprinv  14815  grpinvid  14819  grpinvval2  14835  grpsubid1  14837  mulgcl  14870  mulgz  14874  imasgrp  14897  subg0  14913  subg0cl  14915  issubg4  14924  0subg  14928  nmzsubg  14944  eqgid  14955  divsgrp  14958  divs0  14961  ghmid  14975  ghmpreima  14990  ghmf1  14997  gafo  15036  gaid  15039  gass  15041  gaorber  15048  gastacl  15049  lactghmga  15070  cayleylem2  15074  od1  15158  gexdvds  15181  sylow1lem2  15196  sylow3lem1  15224  lsmdisj2  15277  0frgp  15374  odadd1  15426  torsubg  15432  oddvdssubg  15433  0cyg  15465  prmcyg  15466  dprdfadd  15541  dprdsubg  15545  dprdz  15551  pgpfac1lem3a  15597  rng0cl  15648  rnglz  15663  rngrz  15664  isdrng2  15808  srng0  15911  lmod0vcl  15942  islmhm2  16077  psr0cl  16421  mplsubglem  16461  frgpcyg  16817  ip0l  16830  ocvlss  16862  istgp2  18082  cldsubg  18101  tgpconcompeqg  18102  tgpconcomp  18103  snclseqg  18106  tgphaus  18107  tgpt1  18108  divstgphaus  18113  tgptsmscls  18140  nrmmetd  18583  nmfval2  18599  nmval2  18600  nmf2  18601  ngpds3  18615  nmge0  18624  nmeq0  18625  nminv  18628  nmmtri  18629  nmrtri  18631  nm0  18634  tngnm  18653  idnghm  18738  nmcn  18836  nmoleub2lem2  19085  mdeg0  19954  dchrinv  21006  dchr1re  21008  dchrpt  21012  dchrsum2  21013  dchrhash  21016  rpvmasumlem  21142  rpvmasum2  21167  dchrisum0re  21168  ofldsqr  24201  ofldchr  24205  kerf1hrm  24223  qqh0  24329  sibf0  24610  sconpi1  24887  symgsssg  27284  symgfisg  27285  grpvlinv  27326  lfl0f  29564  lkrlss  29590  lshpkrlem1  29605  lkrin  29659  dvhgrp  31602
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-reu 2681  df-rmo 2682  df-rab 2683  df-v 2926  df-sbc 3130  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-mpt 4236  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-iota 5385  df-fun 5423  df-fv 5429  df-ov 6051  df-riota 6516  df-0g 13690  df-mnd 14653  df-grp 14775
  Copyright terms: Public domain W3C validator