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

Theorem grpidcl 18783
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 𝐵 = (Base‘𝐺)
grpidcl.o 0 = (0g𝐺)
Assertion
Ref Expression
grpidcl (𝐺 ∈ Grp → 0𝐵)

Proof of Theorem grpidcl
StepHypRef Expression
1 grpmnd 18760 . 2 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2 grpidcl.b . . 3 𝐵 = (Base‘𝐺)
3 grpidcl.o . . 3 0 = (0g𝐺)
42, 3mndidcl 18576 . 2 (𝐺 ∈ Mnd → 0𝐵)
51, 4syl 17 1 (𝐺 ∈ Grp → 0𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  cfv 6497  Basecbs 17088  0gc0g 17326  Mndcmnd 18561  Grpcgrp 18753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-iota 6449  df-fun 6499  df-fv 6505  df-riota 7314  df-ov 7361  df-0g 17328  df-mgm 18502  df-sgrp 18551  df-mnd 18562  df-grp 18756
This theorem is referenced by:  grpbn0  18784  grprcan  18789  grpid  18791  isgrpid2  18792  grprinv  18806  grpidinv  18812  grpinvid  18813  grpidrcan  18817  grpidlcan  18818  grpidssd  18828  grpinvval2  18835  grpsubid1  18837  imasgrp  18868  mulgcl  18898  mulgz  18909  subg0  18939  subg0cl  18941  issubg4  18952  0subgOLD  18959  nmzsubg  18972  eqgid  18987  qusgrp  18990  qus0  18993  ghmid  19019  ghmpreima  19035  ghmf1  19042  gafo  19081  gaid  19084  gass  19086  gaorber  19093  gastacl  19094  lactghmga  19192  cayleylem2  19200  symgsssg  19254  symgfisg  19255  od1  19346  gexdvds  19371  sylow1lem2  19386  sylow3lem1  19414  lsmdisj2  19469  0frgp  19566  odadd1  19631  torsubg  19637  oddvdssubg  19638  0cyg  19675  prmcyg  19676  telgsums  19775  dprdfadd  19804  dprdz  19814  pgpfac1lem3a  19860  ablsimpgprmd  19899  ring0cl  19995  ringlz  20016  ringrz  20017  f1ghm0to0  20181  kerf1ghm  20184  isdrng2  20210  srng0  20333  lmod0vcl  20366  islmhm2  20514  frgpcyg  20996  ip0l  21056  ocvlss  21092  ascl0  21303  psr0cl  21378  mplsubglem  21421  mhp0cl  21552  mhpaddcl  21557  evl1gsumd  21739  grpvlinv  21760  matinvgcell  21800  mat0dim0  21832  mdetdiag  21964  mdetuni0  21986  chpdmatlem2  22204  chp0mat  22211  istgp2  23458  cldsubg  23478  tgpconncompeqg  23479  tgpconncomp  23480  snclseqg  23483  tgphaus  23484  tgpt1  23485  qustgphaus  23490  tgptsmscls  23517  nrmmetd  23946  nmfval2  23963  nmval2  23964  nmf2  23965  ngpds3  23980  nmge0  23989  nmeq0  23990  nminv  23993  nmmtri  23994  nmrtri  23996  nm0  24001  tngnm  24031  idnghm  24123  nmcn  24223  clmvz  24490  nmoleub2lem2  24495  nglmle  24682  mdeg0  25451  dchrinv  26625  dchr1re  26627  dchrpt  26631  dchrsum2  26632  dchrhash  26635  rpvmasumlem  26851  rpvmasum2  26876  dchrisum0re  26877  ogrpinv0lt  31979  ogrpinvlt  31980  isarchi3  32072  archirng  32073  archirngz  32074  archiabllem1b  32077  rmfsupp2  32122  orngsqr  32146  ornglmulle  32147  orngrmulle  32148  ornglmullt  32149  orngrmullt  32150  orngmullt  32151  ofldchr  32156  isarchiofld  32159  qusker  32188  eqg0el  32196  grplsm0l  32232  nsgqus0  32236  nsgmgclem  32237  ghmqusker  32246  fedgmullem1  32381  qqh0  32622  sconnpi1  33890  lfl0f  37577  lkrlss  37603  lshpkrlem1  37618  lkrin  37672  dvhgrp  39616  isdomn4  40670  fsuppind  40808  fsuppssind  40811  mhpind  40812  rnglz  46268  zrrnghm  46301  evl1at0  46558
  Copyright terms: Public domain W3C validator