Theorem grpidcl 19038

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2142  ‘cfv 6536  Basecbs 17275  0_gc0g 17498  Mndcmnd 18798  Grpcgrp 19006

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  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 3368  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-iota 6492  df-fun 6538  df-fv 6544  df-riota 7369  df-ov 7415  df-0g 17500  df-mgm 18704  df-sgrp 18783  df-mnd 18799  df-grp 19009

This theorem is used by:  grpbn0  19039  grprcan  19046  grpid  19048  isgrpid2  19049  grprinv  19063  grpidinv  19071  grpinvid  19072  grpidrcan  19076  grpidlcan  19077  grpidssd  19088  grpinvval2  19095  grpsubid1  19097  imasgrp  19128  mulgcl  19163  mulgz  19174  subg0  19204  subg0cl  19206  issubg4  19218  nmzsubg  19237  eqgid  19254  eqg0el  19260  qusgrp  19263  qus0  19266  ghmid  19298  ghmpreima  19314  f1ghm0to0  19321  kerf1ghm  19323  ghmqusker  19363  gafo  19372  gaid  19375  gass  19377  gaorber  19384  gastacl  19385  lactghmga  19481  cayleylem2  19489  symgsssg  19543  symgfisg  19544  od1  19635  gexdvds  19660  sylow1lem2  19675  sylow3lem1  19703  lsmdisj2  19758  0frgp  19855  odadd1  19924  torsubg  19930  oddvdssubg  19931  0cyg  19969  prmcyg  19970  telgsums  20069  dprdfadd  20098  dprdz  20108  pgpfac1lem3a  20154  ablsimpgprmd  20193  ogrpinv0lt  20219  ogrpinvlt  20220  rng0cl  20247  rnglz  20249  rngrz  20250  ring0cl  20357  zrrnghm  20646  isdomn4  20825  isdrng2  20854  srng0  20968  orngsqr  20980  ornglmulle  20981  orngrmulle  20982  ornglmullt  20983  orngrmullt  20984  orngmullt  20985  lmod0vcl  21023  islmhm2  21170  rnglidl0  21366  frgpcyg  21734  ofldchr  21737  ip0l  21797  ocvlss  21833  ascl0  22045  psr0cl  22113  mplsubglem  22159  mhp0cl  22320  mhpaddcl  22325  evl1gsumd  22528  grpvlinv  22566  matinvgcell  22603  mat0dim0  22635  mdetdiag  22767  mdetuni0  22789  chpdmatlem2  23007  chp0mat  23014  istgp2  24259  cldsubg  24279  tgpconncompeqg  24280  tgpconncomp  24281  snclseqg  24284  tgphaus  24285  tgpt1  24286  qustgphaus  24291  tgptsmscls  24318  nrmmetd  24742  nmfval2  24759  nmval2  24760  nmf2  24761  ngpds3  24776  nmge0  24785  nmeq0  24786  nminv  24789  nmmtri  24790  nmrtri  24792  nm0  24797  tngnm  24819  idnghm  24911  nmcn  25013  clmvz  25281  nmoleub2lem2  25286  nglmle  25472  mdeg0  26238  dchrinv  27436  dchr1re  27438  dchrpt  27442  dchrsum2  27443  dchrhash  27446  rpvmasumlem  27662  rpvmasum2  27687  dchrisum0re  27688  grpidcld  33368  conjga  33499  fxpsubm  33501  fxpsubg  33502  fxpsubrg  33503  isarchi3  33516  archirng  33517  archirngz  33518  archiabllem1b  33521  isarchiofld  33528  rmfsupp2  33566  erler  33594  rlocaddval  33598  rlocmulval  33599  rloc0g  33601  fracfld  33638  qusker  33678  grplsm0l  33721  qus0g  33725  nsgqus0  33728  nsgmgclem  33729  mplvrpmga  33944  mplvrpmmhm  33945  psrmonprod  33951  mplgsum  33952  mplmonprod  33953  esplyind  33974  esplyfvn  33976  fedgmullem1  34028  irredminply  34115  rtelextdg2lem  34125  qqh0  34383  sconnpi1  35739  lfl0f  39871  lkrlss  39897  lshpkrlem1  39912  lkrin  39966  dvhgrp  41909  primrootscoprmpow  42894  aks5lem7  42995  fsuppind  43350  fsuppssind  43353  mhpind  43354  evl1at0  49199