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

Theorem grpidcl 18069
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 18048 . 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 1528  wcel 2105  cfv 6348  Basecbs 16471  0gc0g 16701  Mndcmnd 17899  Grpcgrp 18041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fv 6356  df-riota 7103  df-ov 7148  df-0g 16703  df-mgm 17840  df-sgrp 17889  df-mnd 17900  df-grp 18044
This theorem is referenced by:  grpbn0  18070  grprcan  18075  grpid  18077  isgrpid2  18078  grprinv  18091  grpidinv  18097  grpinvid  18098  grpidrcan  18102  grpidlcan  18103  grpidssd  18113  grpinvval2  18120  grpsubid1  18122  imasgrp  18153  mulgcl  18183  mulgz  18193  subg0  18223  subg0cl  18225  issubg4  18236  0subg  18242  nmzsubg  18255  eqgid  18270  qusgrp  18273  qus0  18276  ghmid  18302  ghmpreima  18318  ghmf1  18325  gafo  18364  gaid  18367  gass  18369  gaorber  18376  gastacl  18377  lactghmga  18462  cayleylem2  18470  symgsssg  18524  symgfisg  18525  od1  18615  gexdvds  18638  sylow1lem2  18653  sylow3lem1  18681  lsmdisj2  18737  0frgp  18834  odadd1  18897  torsubg  18903  oddvdssubg  18904  0cyg  18942  prmcyg  18943  telgsums  19042  dprdfadd  19071  dprdz  19081  pgpfac1lem3a  19127  ablsimpgprmd  19166  ring0cl  19248  ringlz  19266  ringrz  19267  f1ghm0to0  19421  kerf1ghm  19426  kerf1hrmOLD  19427  isdrng2  19441  srng0  19560  lmod0vcl  19592  islmhm2  19739  ascl0  20041  psr0cl  20102  mplsubglem  20142  mhp0cl  20265  mhpaddcl  20266  mhpinvcl  20267  evl1gsumd  20448  frgpcyg  20648  ip0l  20708  ocvlss  20744  grpvlinv  20934  matinvgcell  20972  mat0dim0  21004  mdetdiag  21136  mdetuni0  21158  chpdmatlem2  21375  chp0mat  21382  istgp2  22627  cldsubg  22646  tgpconncompeqg  22647  tgpconncomp  22648  snclseqg  22651  tgphaus  22652  tgpt1  22653  qustgphaus  22658  tgptsmscls  22685  nrmmetd  23111  nmfval2  23127  nmval2  23128  nmf2  23129  ngpds3  23144  nmge0  23153  nmeq0  23154  nminv  23157  nmmtri  23158  nmrtri  23160  nm0  23165  tngnm  23187  idnghm  23279  nmcn  23379  clmvz  23642  nmoleub2lem2  23647  nglmle  23832  mdeg0  24591  dchrinv  25764  dchr1re  25766  dchrpt  25770  dchrsum2  25771  dchrhash  25774  rpvmasumlem  25990  rpvmasum2  26015  dchrisum0re  26016  ogrpinv0lt  30650  ogrpinvlt  30651  isarchi3  30743  archirng  30744  archirngz  30745  archiabllem1b  30748  rmfsupp2  30793  orngsqr  30804  ornglmulle  30805  orngrmulle  30806  ornglmullt  30807  orngrmullt  30808  orngmullt  30809  ofldchr  30814  isarchiofld  30817  qusker  30845  eqg0el  30853  fedgmullem1  30924  qqh0  31124  sconnpi1  32383  lfl0f  36085  lkrlss  36111  lshpkrlem1  36126  lkrin  36180  dvhgrp  38123  symgsubmefmndALT  43996  rnglz  44083  zrrnghm  44116  evl1at0  44373
  Copyright terms: Public domain W3C validator