Theorem grpidcl 18870

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 18845	. 2 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2		grpidcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐺)
3		grpidcl.o	. . 3 ⊢ 0 = (0g‘𝐺)
4	2, 3	mndidcl 18649	. 2 ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)
5	1, 4	syl 17	1 ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2110  ‘cfv 6477  Basecbs 17112  0_gc0g 17335  Mndcmnd 18634  Grpcgrp 18838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3344  df-reu 3345  df-rab 3394  df-v 3436  df-sbc 3740  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-iota 6433  df-fun 6479  df-fv 6485  df-riota 7298  df-ov 7344  df-0g 17337  df-mgm 18540  df-sgrp 18619  df-mnd 18635  df-grp 18841

This theorem is referenced by:  grpbn0  18871  grprcan  18878  grpid  18880  isgrpid2  18881  grprinv  18895  grpidinv  18903  grpinvid  18904  grpidrcan  18908  grpidlcan  18909  grpidssd  18921  grpinvval2  18928  grpsubid1  18930  imasgrp  18961  mulgcl  18996  mulgz  19007  subg0  19037  subg0cl  19039  issubg4  19050  0subgOLD  19057  nmzsubg  19070  eqgid  19085  eqg0el  19088  qusgrp  19091  qus0  19094  ghmid  19127  ghmpreima  19143  f1ghm0to0  19150  kerf1ghm  19152  ghmqusker  19192  gafo  19201  gaid  19204  gass  19206  gaorber  19213  gastacl  19214  lactghmga  19310  cayleylem2  19318  symgsssg  19372  symgfisg  19373  od1  19464  gexdvds  19489  sylow1lem2  19504  sylow3lem1  19532  lsmdisj2  19587  0frgp  19684  odadd1  19753  torsubg  19759  oddvdssubg  19760  0cyg  19798  prmcyg  19799  telgsums  19898  dprdfadd  19927  dprdz  19937  pgpfac1lem3a  19983  ablsimpgprmd  20022  ogrpinv0lt  20048  ogrpinvlt  20049  rng0cl  20074  rnglz  20076  rngrz  20077  ring0cl  20178  zrrnghm  20444  isdomn4  20624  isdrng2  20651  srng0  20762  orngsqr  20774  ornglmulle  20775  orngrmulle  20776  ornglmullt  20777  orngrmullt  20778  orngmullt  20779  lmod0vcl  20817  islmhm2  20965  rnglidl0  21159  frgpcyg  21503  ofldchr  21506  ip0l  21566  ocvlss  21602  ascl0  21814  psr0cl  21882  mplsubglem  21929  mhp0cl  22054  mhpaddcl  22059  evl1gsumd  22265  grpvlinv  22306  matinvgcell  22343  mat0dim0  22375  mdetdiag  22507  mdetuni0  22529  chpdmatlem2  22747  chp0mat  22754  istgp2  23999  cldsubg  24019  tgpconncompeqg  24020  tgpconncomp  24021  snclseqg  24024  tgphaus  24025  tgpt1  24026  qustgphaus  24031  tgptsmscls  24058  nrmmetd  24482  nmfval2  24499  nmval2  24500  nmf2  24501  ngpds3  24516  nmge0  24525  nmeq0  24526  nminv  24529  nmmtri  24530  nmrtri  24532  nm0  24537  tngnm  24559  idnghm  24651  nmcn  24753  clmvz  25031  nmoleub2lem2  25036  nglmle  25222  mdeg0  25995  dchrinv  27192  dchr1re  27194  dchrpt  27198  dchrsum2  27199  dchrhash  27202  rpvmasumlem  27418  rpvmasum2  27443  dchrisum0re  27444  conjga  33129  fxpsubm  33131  fxpsubg  33132  fxpsubrg  33133  isarchi3  33146  archirng  33147  archirngz  33148  archiabllem1b  33151  isarchiofld  33158  rmfsupp2  33195  erler  33222  rlocaddval  33225  rlocmulval  33226  rloc0g  33228  fracfld  33264  qusker  33304  grplsm0l  33358  qus0g  33362  nsgqus0  33365  nsgmgclem  33366  mplvrpmga  33565  mplvrpmmhm  33566  fedgmullem1  33632  irredminply  33719  rtelextdg2lem  33729  qqh0  33987  sconnpi1  35251  lfl0f  39087  lkrlss  39113  lshpkrlem1  39128  lkrin  39182  dvhgrp  41125  primrootscoprmpow  42111  aks5lem7  42212  fsuppind  42602  fsuppssind  42605  mhpind  42606  evl1at0  48402