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

Theorem grpidcl 18061
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 18040 . 2 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2 grpidcl.b . . 3 𝐵 = (Base‘𝐺)
3 grpidcl.o . . 3 0 = (0g𝐺)
42, 3mndidcl 17914 . 2 (𝐺 ∈ Mnd → 0𝐵)
51, 4syl 17 1 (𝐺 ∈ Grp → 0𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wcel 2107  cfv 6352  Basecbs 16473  0gc0g 16703  Mndcmnd 17900  Grpcgrp 18033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-iota 6312  df-fun 6354  df-fv 6360  df-riota 7106  df-ov 7151  df-0g 16705  df-mgm 17842  df-sgrp 17890  df-mnd 17901  df-grp 18036
This theorem is referenced by:  grpbn0  18062  grprcan  18067  grpid  18069  isgrpid2  18070  grprinv  18083  grpidinv  18089  grpinvid  18090  grpidrcan  18094  grpidlcan  18095  grpidssd  18105  grpinvval2  18112  grpsubid1  18114  imasgrp  18145  mulgcl  18175  mulgz  18185  subg0  18215  subg0cl  18217  issubg4  18228  0subg  18234  nmzsubg  18247  eqgid  18262  qusgrp  18265  qus0  18268  ghmid  18294  ghmpreima  18310  ghmf1  18317  gafo  18356  gaid  18359  gass  18361  gaorber  18368  gastacl  18369  lactghmga  18452  cayleylem2  18461  symgsssg  18515  symgfisg  18516  od1  18606  gexdvds  18629  sylow1lem2  18644  sylow3lem1  18672  lsmdisj2  18728  0frgp  18825  odadd1  18888  torsubg  18894  oddvdssubg  18895  0cyg  18933  prmcyg  18934  telgsums  19033  dprdfadd  19062  dprdz  19072  pgpfac1lem3a  19118  ablsimpgprmd  19157  ring0cl  19239  ringlz  19257  ringrz  19258  f1ghm0to0  19412  kerf1ghm  19417  kerf1hrmOLD  19418  isdrng2  19432  srng0  19551  lmod0vcl  19583  islmhm2  19730  ascl0  20032  psr0cl  20093  mplsubglem  20133  mhp0cl  20254  mhpaddcl  20255  mhpinvcl  20256  evl1gsumd  20436  frgpcyg  20636  ip0l  20696  ocvlss  20732  grpvlinv  20922  matinvgcell  20960  mat0dim0  20992  mdetdiag  21124  mdetuni0  21146  chpdmatlem2  21363  chp0mat  21370  istgp2  22615  cldsubg  22634  tgpconncompeqg  22635  tgpconncomp  22636  snclseqg  22639  tgphaus  22640  tgpt1  22641  qustgphaus  22646  tgptsmscls  22673  nrmmetd  23099  nmfval2  23115  nmval2  23116  nmf2  23117  ngpds3  23132  nmge0  23141  nmeq0  23142  nminv  23145  nmmtri  23146  nmrtri  23148  nm0  23153  tngnm  23175  idnghm  23267  nmcn  23367  clmvz  23630  nmoleub2lem2  23635  nglmle  23820  mdeg0  24579  dchrinv  25751  dchr1re  25753  dchrpt  25757  dchrsum2  25758  dchrhash  25761  rpvmasumlem  25977  rpvmasum2  26002  dchrisum0re  26003  ogrpinv0lt  30637  ogrpinvlt  30638  isarchi3  30730  archirng  30731  archirngz  30732  archiabllem1b  30735  rmfsupp2  30780  orngsqr  30791  ornglmulle  30792  orngrmulle  30793  ornglmullt  30794  orngrmullt  30795  orngmullt  30796  ofldchr  30801  isarchiofld  30804  qusker  30832  eqg0el  30840  fedgmullem1  30911  qqh0  31111  sconnpi1  32370  lfl0f  36072  lkrlss  36098  lshpkrlem1  36113  lkrin  36167  dvhgrp  38110  rnglz  43987  zrrnghm  44020  evl1at0  44277
  Copyright terms: Public domain W3C validator