Theorem grpidcl 19177

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ‘cfv 6538  Basecbs 17388  0_gc0g 17611  Mndcmnd 18924  Grpcgrp 19145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6540  df-fv 6546  df-riota 7377  df-ov 7423  df-0g 17613  df-mgm 18817  df-sgrp 18909  df-mnd 18925  df-grp 19148

This theorem is used by:  grpbn0  19178  grprcan  19185  grpid  19187  isgrpid2  19188  grprinv  19202  grpidinv  19210  grpinvid  19211  grpidrcan  19215  grpidlcan  19216  grpidssd  19227  grpinvval2  19234  grpsubid1  19236  imasgrp  19267  mulgcl  19302  mulgz  19313  subg0  19343  subg0cl  19345  issubg4  19357  nmzsubg  19376  eqgid  19393  eqg0el  19399  qusgrp  19402  qus0  19405  ghmid  19437  ghmpreima  19453  f1ghm0to0  19460  kerf1ghm  19462  ghmqusker  19502  gafo  19511  gaid  19514  gass  19516  gaorber  19523  gastacl  19524  lactghmga  19620  cayleylem2  19628  symgsssg  19682  symgfisg  19683  od1  19774  gexdvds  19799  sylow1lem2  19814  sylow3lem1  19842  lsmdisj2  19897  0frgp  19994  odadd1  20063  torsubg  20069  oddvdssubg  20070  0cyg  20108  prmcyg  20109  telgsums  20208  dprdfadd  20237  dprdz  20247  pgpfac1lem3a  20293  ablsimpgprmd  20332  ogrpinv0lt  20358  ogrpinvlt  20359  rng0cl  20386  rnglz  20388  rngrz  20389  ring0cl  20497  zrrnghm  20789  isdomn4  20968  isdrng2  20998  srng0  21112  orngsqr  21124  ornglmulle  21125  orngrmulle  21126  ornglmullt  21127  orngrmullt  21128  orngmullt  21129  lmod0vcl  21167  islmhm2  21314  rnglidl0  21510  frgpcyg  21880  ofldchr  21883  ip0l  21943  ocvlss  21979  ascl0  22193  psr0cl  22261  mplsubglem  22307  mhp0cl  22468  mhpaddcl  22473  evl1gsumd  22676  grpvlinv  22714  matinvgcell  22751  mat0dim0  22783  mdetdiag  22915  mdetuni0  22937  chpdmatlem2  23158  chp0mat  23165  istgp2  24411  cldsubg  24431  tgpconncompeqg  24432  tgpconncomp  24433  snclseqg  24436  tgphaus  24437  tgpt1  24438  qustgphaus  24443  tgptsmscls  24470  nrmmetd  24894  nmfval2  24911  nmval2  24912  nmf2  24913  ngpds3  24928  nmge0  24937  nmeq0  24938  nminv  24941  nmmtri  24942  nmrtri  24944  nm0  24949  tngnm  24971  idnghm  25063  nmcn  25165  clmvz  25433  nmoleub2lem2  25438  nglmle  25624  mdeg0  26389  dchrinv  27589  dchr1re  27591  dchrpt  27595  dchrsum2  27596  dchrhash  27599  rpvmasumlem  27815  rpvmasum2  27840  dchrisum0re  27841  grpidcld  33643  conjga  33774  fxpsubm  33776  fxpsubg  33777  fxpsubrg  33778  isarchi3  33791  archirng  33792  archirngz  33793  archiabllem1b  33796  isarchiofld  33803  rmfsupp2  33841  erler  33869  rlocaddval  33873  rlocmulval  33874  rloc0g  33876  fracfld  33913  qusker  33953  grplsm0l  33997  qus0g  34001  nsgqus0  34004  nsgmgclem  34005  mplvrpmga  34220  mplgsum  34228  mplmonprod  34229  esplyind  34250  esplyfvn  34252  fedgmullem1  34304  irredminply  34391  rtelextdg2lem  34401  qqh0  34659  sconnpi1  36073  lfl0f  40202  lkrlss  40228  lshpkrlem1  40243  lkrin  40297  dvhgrp  42240  primrootscoprmpow  43225  aks5lem7  43326  fsuppind  43694  fsuppssind  43697  mhpind  43698  evl1at0  49579