Theorem grpidcl 19093

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  Basecbs 17305  0_gc0g 17528  Mndcmnd 18840  Grpcgrp 19061

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545  df-riota 7373  df-ov 7419  df-0g 17530  df-mgm 18734  df-sgrp 18825  df-mnd 18841  df-grp 19064

This theorem is used by:  grpbn0  19094  grprcan  19101  grpid  19103  isgrpid2  19104  grprinv  19118  grpidinv  19126  grpinvid  19127  grpidrcan  19131  grpidlcan  19132  grpidssd  19143  grpinvval2  19150  grpsubid1  19152  imasgrp  19183  mulgcl  19218  mulgz  19229  subg0  19259  subg0cl  19261  issubg4  19273  nmzsubg  19292  eqgid  19309  eqg0el  19315  qusgrp  19318  qus0  19321  ghmid  19353  ghmpreima  19369  f1ghm0to0  19376  kerf1ghm  19378  ghmqusker  19418  gafo  19427  gaid  19430  gass  19432  gaorber  19439  gastacl  19440  lactghmga  19536  cayleylem2  19544  symgsssg  19598  symgfisg  19599  od1  19690  gexdvds  19715  sylow1lem2  19730  sylow3lem1  19758  lsmdisj2  19813  0frgp  19910  odadd1  19979  torsubg  19985  oddvdssubg  19986  0cyg  20024  prmcyg  20025  telgsums  20124  dprdfadd  20153  dprdz  20163  pgpfac1lem3a  20209  ablsimpgprmd  20248  ogrpinv0lt  20274  ogrpinvlt  20275  rng0cl  20302  rnglz  20304  rngrz  20305  ring0cl  20412  zrrnghm  20702  isdomn4  20881  isdrng2  20910  srng0  21024  orngsqr  21036  ornglmulle  21037  orngrmulle  21038  ornglmullt  21039  orngrmullt  21040  orngmullt  21041  lmod0vcl  21079  islmhm2  21226  rnglidl0  21422  frgpcyg  21790  ofldchr  21793  ip0l  21853  ocvlss  21889  ascl0  22103  psr0cl  22171  mplsubglem  22217  mhp0cl  22378  mhpaddcl  22383  evl1gsumd  22586  grpvlinv  22624  matinvgcell  22661  mat0dim0  22693  mdetdiag  22825  mdetuni0  22847  chpdmatlem2  23068  chp0mat  23075  istgp2  24321  cldsubg  24341  tgpconncompeqg  24342  tgpconncomp  24343  snclseqg  24346  tgphaus  24347  tgpt1  24348  qustgphaus  24353  tgptsmscls  24380  nrmmetd  24804  nmfval2  24821  nmval2  24822  nmf2  24823  ngpds3  24838  nmge0  24847  nmeq0  24848  nminv  24851  nmmtri  24852  nmrtri  24854  nm0  24859  tngnm  24881  idnghm  24973  nmcn  25075  clmvz  25343  nmoleub2lem2  25348  nglmle  25534  mdeg0  26300  dchrinv  27498  dchr1re  27500  dchrpt  27504  dchrsum2  27505  dchrhash  27508  rpvmasumlem  27724  rpvmasum2  27749  dchrisum0re  27750  grpidcld  33481  conjga  33612  fxpsubm  33614  fxpsubg  33615  fxpsubrg  33616  isarchi3  33629  archirng  33630  archirngz  33631  archiabllem1b  33634  isarchiofld  33641  rmfsupp2  33679  erler  33707  rlocaddval  33711  rlocmulval  33712  rloc0g  33714  fracfld  33751  qusker  33791  grplsm0l  33834  qus0g  33838  nsgqus0  33841  nsgmgclem  33842  mplvrpmga  34057  mplgsum  34065  mplmonprod  34066  esplyind  34087  esplyfvn  34089  fedgmullem1  34141  irredminply  34228  rtelextdg2lem  34238  qqh0  34496  sconnpi1  35820  lfl0f  39944  lkrlss  39970  lshpkrlem1  39985  lkrin  40039  dvhgrp  41982  primrootscoprmpow  42967  aks5lem7  43068  fsuppind  43438  fsuppssind  43441  mhpind  43442  evl1at0  49323