Theorem grpidcl 19205

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ‘cfv 6558  Basecbs 17416  0_gc0g 17639  Mndcmnd 18952  Grpcgrp 19173

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6512  df-fun 6560  df-fv 6566  df-riota 7400  df-ov 7446  df-0g 17641  df-mgm 18845  df-sgrp 18937  df-mnd 18953  df-grp 19176

This theorem is used by:  grpbn0  19206  grprcan  19213  grpid  19215  isgrpid2  19216  grprinv  19230  grpidinv  19238  grpinvid  19239  grpidrcan  19243  grpidlcan  19244  grpidssd  19255  grpinvval2  19262  grpsubid1  19264  imasgrp  19295  mulgcl  19330  mulgz  19341  subg0  19371  subg0cl  19373  issubg4  19385  nmzsubg  19404  eqgid  19421  eqg0el  19427  qusgrp  19430  qus0  19433  ghmid  19465  ghmpreima  19481  f1ghm0to0  19488  kerf1ghm  19490  ghmqusker  19531  gafo  19540  gaid  19543  gass  19545  gaorber  19552  gastacl  19553  lactghmga  19649  cayleylem2  19657  symgsssg  19711  symgfisg  19712  od1  19803  gexdvds  19828  sylow1lem2  19843  sylow3lem1  19871  lsmdisj2  19926  0frgp  20023  odadd1  20092  torsubg  20098  oddvdssubg  20099  0cyg  20137  prmcyg  20138  telgsums  20237  dprdfadd  20266  dprdz  20276  pgpfac1lem3a  20322  ablsimpgprmd  20361  ogrpinv0lt  20387  ogrpinvlt  20388  rng0cl  20415  rnglz  20417  rngrz  20418  ring0cl  20526  zrrnghm  20818  isdomn4  20997  isdrng2  21027  srng0  21141  orngsqr  21153  ornglmulle  21154  orngrmulle  21155  ornglmullt  21156  orngrmullt  21157  orngmullt  21158  lmod0vcl  21196  islmhm2  21343  rnglidl0  21539  frgpcyg  21909  ofldchr  21912  ip0l  21972  ocvlss  22008  ascl0  22222  psr0cl  22290  mplsubglem  22336  mhp0cl  22497  mhpaddcl  22502  evl1gsumd  22705  grpvlinv  22743  matinvgcell  22780  mat0dim0  22812  mdetdiag  22944  mdetuni0  22966  chpdmatlem2  23187  chp0mat  23194  istgp2  24440  cldsubg  24460  tgpconncompeqg  24461  tgpconncomp  24462  snclseqg  24465  tgphaus  24466  tgpt1  24467  qustgphaus  24472  tgptsmscls  24499  nrmmetd  24923  nmfval2  24940  nmval2  24941  nmf2  24942  ngpds3  24957  nmge0  24966  nmeq0  24967  nminv  24970  nmmtri  24971  nmrtri  24973  nm0  24978  tngnm  25000  idnghm  25092  nmcn  25194  clmvz  25462  nmoleub2lem2  25467  nglmle  25653  mdeg0  26418  dchrinv  27618  dchr1re  27620  dchrpt  27624  dchrsum2  27625  dchrhash  27628  rpvmasumlem  27844  rpvmasum2  27869  dchrisum0re  27870  grpidcld  33670  conjga  33801  fxpsubm  33803  fxpsubg  33804  fxpsubrg  33805  isarchi3  33818  archirng  33819  archirngz  33820  archiabllem1b  33823  isarchiofld  33830  rmfsupp2  33868  erler  33896  rlocaddval  33900  rlocmulval  33901  rloc0g  33903  fracfld  33940  qusker  33980  grplsm0l  34024  qus0g  34028  nsgqus0  34031  nsgmgclem  34032  mplvrpmga  34247  mplgsum  34255  mplmonprod  34256  esplyind  34277  esplyfvn  34279  fedgmullem1  34331  irredminply  34418  rtelextdg2lem  34428  qqh0  34686  sconnpi1  36171  lfl0f  40318  lkrlss  40344  lshpkrlem1  40359  lkrin  40413  dvhgrp  42356  primrootscoprmpow  43341  aks5lem7  43442  fsuppind  43811  fsuppssind  43814  mhpind  43815  evl1at0  49708