Theorem grpidcl 18522

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  ‘cfv 6418  Basecbs 16840  0_gc0g 17067  Mndcmnd 18300  Grpcgrp 18492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426  df-riota 7212  df-ov 7258  df-0g 17069  df-mgm 18241  df-sgrp 18290  df-mnd 18301  df-grp 18495

This theorem is referenced by:  grpbn0  18523  grprcan  18528  grpid  18530  isgrpid2  18531  grprinv  18544  grpidinv  18550  grpinvid  18551  grpidrcan  18555  grpidlcan  18556  grpidssd  18566  grpinvval2  18573  grpsubid1  18575  imasgrp  18606  mulgcl  18636  mulgz  18646  subg0  18676  subg0cl  18678  issubg4  18689  0subg  18695  nmzsubg  18708  eqgid  18723  qusgrp  18726  qus0  18729  ghmid  18755  ghmpreima  18771  ghmf1  18778  gafo  18817  gaid  18820  gass  18822  gaorber  18829  gastacl  18830  lactghmga  18928  cayleylem2  18936  symgsssg  18990  symgfisg  18991  od1  19081  gexdvds  19104  sylow1lem2  19119  sylow3lem1  19147  lsmdisj2  19203  0frgp  19300  odadd1  19364  torsubg  19370  oddvdssubg  19371  0cyg  19409  prmcyg  19410  telgsums  19509  dprdfadd  19538  dprdz  19548  pgpfac1lem3a  19594  ablsimpgprmd  19633  ring0cl  19723  ringlz  19741  ringrz  19742  f1ghm0to0  19899  kerf1ghm  19902  isdrng2  19916  srng0  20035  lmod0vcl  20067  islmhm2  20215  frgpcyg  20693  ip0l  20753  ocvlss  20789  ascl0  20998  psr0cl  21073  mplsubglem  21115  mhp0cl  21246  mhpaddcl  21251  evl1gsumd  21433  grpvlinv  21454  matinvgcell  21492  mat0dim0  21524  mdetdiag  21656  mdetuni0  21678  chpdmatlem2  21896  chp0mat  21903  istgp2  23150  cldsubg  23170  tgpconncompeqg  23171  tgpconncomp  23172  snclseqg  23175  tgphaus  23176  tgpt1  23177  qustgphaus  23182  tgptsmscls  23209  nrmmetd  23636  nmfval2  23653  nmval2  23654  nmf2  23655  ngpds3  23670  nmge0  23679  nmeq0  23680  nminv  23683  nmmtri  23684  nmrtri  23686  nm0  23691  tngnm  23721  idnghm  23813  nmcn  23913  clmvz  24180  nmoleub2lem2  24185  nglmle  24371  mdeg0  25140  dchrinv  26314  dchr1re  26316  dchrpt  26320  dchrsum2  26321  dchrhash  26324  rpvmasumlem  26540  rpvmasum2  26565  dchrisum0re  26566  ogrpinv0lt  31250  ogrpinvlt  31251  isarchi3  31343  archirng  31344  archirngz  31345  archiabllem1b  31348  rmfsupp2  31394  orngsqr  31405  ornglmulle  31406  orngrmulle  31407  ornglmullt  31408  orngrmullt  31409  orngmullt  31410  ofldchr  31415  isarchiofld  31418  qusker  31451  eqg0el  31459  grplsm0l  31493  nsgqus0  31497  nsgmgclem  31498  fedgmullem1  31612  qqh0  31834  sconnpi1  33101  lfl0f  37010  lkrlss  37036  lshpkrlem1  37051  lkrin  37105  dvhgrp  39048  isdomn4  40100  fsuppind  40202  fsuppssind  40205  mhpind  40206  rnglz  45330  zrrnghm  45363  evl1at0  45620