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

Theorem grpidcl 14838
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 14822 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpidcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpidcl.o . . 3  |-  .0.  =  ( 0g `  G )
42, 3mndidcl 14719 . 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 1653    e. wcel 1726   ` cfv 5457   Basecbs 13474   0gc0g 13728   Mndcmnd 14689   Grpcgrp 14690
This theorem is referenced by:  grpbn0  14839  grprcan  14843  grpid  14845  isgrpid2  14846  grprinv  14857  grpinvid  14861  grpinvval2  14877  grpsubid1  14879  mulgcl  14912  mulgz  14916  imasgrp  14939  subg0  14955  subg0cl  14957  issubg4  14966  0subg  14970  nmzsubg  14986  eqgid  14997  divsgrp  15000  divs0  15003  ghmid  15017  ghmpreima  15032  ghmf1  15039  gafo  15078  gaid  15081  gass  15083  gaorber  15090  gastacl  15091  lactghmga  15112  cayleylem2  15116  od1  15200  gexdvds  15223  sylow1lem2  15238  sylow3lem1  15266  lsmdisj2  15319  0frgp  15416  odadd1  15468  torsubg  15474  oddvdssubg  15475  0cyg  15507  prmcyg  15508  dprdfadd  15583  dprdsubg  15587  dprdz  15593  pgpfac1lem3a  15639  rng0cl  15690  rnglz  15705  rngrz  15706  isdrng2  15850  srng0  15953  lmod0vcl  15984  islmhm2  16119  psr0cl  16463  mplsubglem  16503  frgpcyg  16859  ip0l  16872  ocvlss  16904  istgp2  18126  cldsubg  18145  tgpconcompeqg  18146  tgpconcomp  18147  snclseqg  18150  tgphaus  18151  tgpt1  18152  divstgphaus  18157  tgptsmscls  18184  nrmmetd  18627  nmfval2  18643  nmval2  18644  nmf2  18645  ngpds3  18659  nmge0  18668  nmeq0  18669  nminv  18672  nmmtri  18673  nmrtri  18675  nm0  18678  tngnm  18697  idnghm  18782  nmcn  18880  nmoleub2lem2  19129  mdeg0  19998  dchrinv  21050  dchr1re  21052  dchrpt  21056  dchrsum2  21057  dchrhash  21060  rpvmasumlem  21186  rpvmasum2  21211  dchrisum0re  21212  ofldsqr  24245  ofldchr  24249  kerf1hrm  24267  qqh0  24373  sibf0  24654  sconpi1  24931  symgsssg  27399  symgfisg  27400  grpvlinv  27441  lfl0f  29941  lkrlss  29967  lshpkrlem1  29982  lkrin  30036  dvhgrp  31979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-iota 5421  df-fun 5459  df-fv 5465  df-ov 6087  df-riota 6552  df-0g 13732  df-mnd 14695  df-grp 14817
  Copyright terms: Public domain W3C validator