Theorem grpidcl 18941

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

Step	Hyp	Ref	Expression
1		grpmnd 18916	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpidcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grpidcl.o	. . 3 ⊢ 0 = (0g‘𝐺)
4	2, 3	mndidcl 18717	. 2 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)
5	1, 4	syl 17	1 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6499  Basecbs 17179  0_gc0g 17402  Mndcmnd 18702  Grpcgrp 18909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5376

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6455  df-fun 6501  df-fv 6507  df-riota 7324  df-ov 7370  df-0g 17404  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-grp 18912

This theorem is referenced by:  grpbn0  18942  grprcan  18949  grpid  18951  isgrpid2  18952  grprinv  18966  grpidinv  18974  grpinvid  18975  grpidrcan  18979  grpidlcan  18980  grpidssd  18992  grpinvval2  18999  grpsubid1  19001  imasgrp  19032  mulgcl  19067  mulgz  19078  subg0  19108  subg0cl  19110  issubg4  19121  nmzsubg  19140  eqgid  19155  eqg0el  19158  qusgrp  19161  qus0  19164  ghmid  19197  ghmpreima  19213  f1ghm0to0  19220  kerf1ghm  19222  ghmqusker  19262  gafo  19271  gaid  19274  gass  19276  gaorber  19283  gastacl  19284  lactghmga  19380  cayleylem2  19388  symgsssg  19442  symgfisg  19443  od1  19534  gexdvds  19559  sylow1lem2  19574  sylow3lem1  19602  lsmdisj2  19657  0frgp  19754  odadd1  19823  torsubg  19829  oddvdssubg  19830  0cyg  19868  prmcyg  19869  telgsums  19968  dprdfadd  19997  dprdz  20007  pgpfac1lem3a  20053  ablsimpgprmd  20092  ogrpinv0lt  20118  ogrpinvlt  20119  rng0cl  20144  rnglz  20146  rngrz  20147  ring0cl  20248  zrrnghm  20513  isdomn4  20693  isdrng2  20720  srng0  20831  orngsqr  20843  ornglmulle  20844  orngrmulle  20845  ornglmullt  20846  orngrmullt  20847  orngmullt  20848  lmod0vcl  20886  islmhm2  21033  rnglidl0  21227  frgpcyg  21553  ofldchr  21556  ip0l  21616  ocvlss  21652  ascl0  21864  psr0cl  21931  mplsubglem  21977  mhp0cl  22112  mhpaddcl  22117  evl1gsumd  22322  grpvlinv  22363  matinvgcell  22400  mat0dim0  22432  mdetdiag  22564  mdetuni0  22586  chpdmatlem2  22804  chp0mat  22811  istgp2  24056  cldsubg  24076  tgpconncompeqg  24077  tgpconncomp  24078  snclseqg  24081  tgphaus  24082  tgpt1  24083  qustgphaus  24088  tgptsmscls  24115  nrmmetd  24539  nmfval2  24556  nmval2  24557  nmf2  24558  ngpds3  24573  nmge0  24582  nmeq0  24583  nminv  24586  nmmtri  24587  nmrtri  24589  nm0  24594  tngnm  24616  idnghm  24708  nmcn  24810  clmvz  25078  nmoleub2lem2  25083  nglmle  25269  mdeg0  26035  dchrinv  27224  dchr1re  27226  dchrpt  27230  dchrsum2  27231  dchrhash  27234  rpvmasumlem  27450  rpvmasum2  27475  dchrisum0re  27476  conjga  33231  fxpsubm  33233  fxpsubg  33234  fxpsubrg  33235  isarchi3  33248  archirng  33249  archirngz  33250  archiabllem1b  33253  isarchiofld  33260  rmfsupp2  33299  erler  33326  rlocaddval  33329  rlocmulval  33330  rloc0g  33332  fracfld  33369  qusker  33409  grplsm0l  33463  qus0g  33467  nsgqus0  33470  nsgmgclem  33471  mplvrpmga  33689  mplvrpmmhm  33690  psrmonprod  33696  mplgsum  33697  mplmonprod  33698  esplyind  33719  esplyfvn  33721  fedgmullem1  33773  irredminply  33860  rtelextdg2lem  33870  qqh0  34128  sconnpi1  35421  lfl0f  39515  lkrlss  39541  lshpkrlem1  39556  lkrin  39610  dvhgrp  41553  primrootscoprmpow  42538  aks5lem7  42639  fsuppind  43023  fsuppssind  43026  mhpind  43027  evl1at0  48861