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

Theorem grpidcl 15546
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 15530 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpidcl.b . . 3  |-  B  =  ( Base `  G
)
3 grpidcl.o . . 3  |-  .0.  =  ( 0g `  G )
42, 3mndidcl 15422 . 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 1362    e. wcel 1755   ` cfv 5406   Basecbs 14157   0gc0g 14361   Mndcmnd 15392   Grpcgrp 15393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-iota 5369  df-fun 5408  df-fv 5414  df-riota 6039  df-ov 6083  df-0g 14363  df-mnd 15398  df-grp 15525
This theorem is referenced by:  grpbn0  15547  grprcan  15551  grpid  15553  isgrpid2  15554  grprinv  15565  grpinvid  15569  grpidrcan  15571  grpidlcan  15572  grpidssd  15582  grpinvval2  15589  grpsubid1  15591  mulgcl  15624  mulgz  15628  imasgrp  15651  subg0  15667  subg0cl  15669  issubg4  15680  0subg  15686  nmzsubg  15702  eqgid  15713  divsgrp  15716  divs0  15719  ghmid  15733  ghmpreima  15748  ghmf1  15755  gafo  15794  gaid  15797  gass  15799  gaorber  15806  gastacl  15807  lactghmga  15889  cayleylem2  15898  symgsssg  15953  symgfisg  15954  od1  16040  gexdvds  16063  sylow1lem2  16078  sylow3lem1  16106  lsmdisj2  16159  0frgp  16256  odadd1  16310  torsubg  16316  oddvdssubg  16317  0cyg  16349  prmcyg  16350  dprdfadd  16484  dprdfaddOLD  16491  dprdz  16501  pgpfac1lem3a  16551  rng0cl  16602  rnglz  16617  rngrz  16618  isdrng2  16766  srng0  16869  lmod0vcl  16901  islmhm2  17041  psr0cl  17399  mplsubglem  17444  mplsubglemOLD  17446  frgpcyg  17848  ip0l  17907  ocvlss  17939  grpvlinv  18137  mdet1  18250  mdetuni0  18269  istgp2  19504  cldsubg  19523  tgpconcompeqg  19524  tgpconcomp  19525  snclseqg  19528  tgphaus  19529  tgpt1  19530  divstgphaus  19535  tgptsmscls  19566  nrmmetd  20009  nmfval2  20025  nmval2  20026  nmf2  20027  ngpds3  20041  nmge0  20050  nmeq0  20051  nminv  20054  nmmtri  20055  nmrtri  20057  nm0  20060  tngnm  20079  idnghm  20164  nmcn  20263  nmoleub2lem2  20513  mdeg0  21426  dchrinv  22485  dchr1re  22487  dchrpt  22491  dchrsum2  22492  dchrhash  22495  rpvmasumlem  22621  rpvmasum2  22646  dchrisum0re  22647  ogrpinvOLD  26002  ogrpinv0lt  26010  ogrpinvlt  26011  isarchi3  26028  archirng  26029  archirngz  26030  archiabllem1b  26033  orngsqr  26125  ornglmulle  26126  orngrmulle  26127  ornglmullt  26128  orngrmullt  26129  orngmullt  26130  ofldchr  26135  isarchiofld  26138  kerf1hrm  26145  qqh0  26267  sconpi1  26976  ascl0  30626  evl1at0  30631  mat0dim0  30643  lfl0f  32287  lkrlss  32313  lshpkrlem1  32328  lkrin  32382  dvhgrp  34325
  Copyright terms: Public domain W3C validator