Theorem grpidcl 18904

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6514  Basecbs 17186  0_gc0g 17409  Mndcmnd 18668  Grpcgrp 18872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-riota 7347  df-ov 7393  df-0g 17411  df-mgm 18574  df-sgrp 18653  df-mnd 18669  df-grp 18875

This theorem is referenced by:  grpbn0  18905  grprcan  18912  grpid  18914  isgrpid2  18915  grprinv  18929  grpidinv  18937  grpinvid  18938  grpidrcan  18942  grpidlcan  18943  grpidssd  18955  grpinvval2  18962  grpsubid1  18964  imasgrp  18995  mulgcl  19030  mulgz  19041  subg0  19071  subg0cl  19073  issubg4  19084  0subgOLD  19091  nmzsubg  19104  eqgid  19119  eqg0el  19122  qusgrp  19125  qus0  19128  ghmid  19161  ghmpreima  19177  f1ghm0to0  19184  kerf1ghm  19186  ghmqusker  19226  gafo  19235  gaid  19238  gass  19240  gaorber  19247  gastacl  19248  lactghmga  19342  cayleylem2  19350  symgsssg  19404  symgfisg  19405  od1  19496  gexdvds  19521  sylow1lem2  19536  sylow3lem1  19564  lsmdisj2  19619  0frgp  19716  odadd1  19785  torsubg  19791  oddvdssubg  19792  0cyg  19830  prmcyg  19831  telgsums  19930  dprdfadd  19959  dprdz  19969  pgpfac1lem3a  20015  ablsimpgprmd  20054  rng0cl  20079  rnglz  20081  rngrz  20082  ring0cl  20183  zrrnghm  20452  isdomn4  20632  isdrng2  20659  srng0  20770  lmod0vcl  20804  islmhm2  20952  rnglidl0  21146  frgpcyg  21490  ip0l  21552  ocvlss  21588  ascl0  21800  psr0cl  21868  mplsubglem  21915  mhp0cl  22040  mhpaddcl  22045  evl1gsumd  22251  grpvlinv  22292  matinvgcell  22329  mat0dim0  22361  mdetdiag  22493  mdetuni0  22515  chpdmatlem2  22733  chp0mat  22740  istgp2  23985  cldsubg  24005  tgpconncompeqg  24006  tgpconncomp  24007  snclseqg  24010  tgphaus  24011  tgpt1  24012  qustgphaus  24017  tgptsmscls  24044  nrmmetd  24469  nmfval2  24486  nmval2  24487  nmf2  24488  ngpds3  24503  nmge0  24512  nmeq0  24513  nminv  24516  nmmtri  24517  nmrtri  24519  nm0  24524  tngnm  24546  idnghm  24638  nmcn  24740  clmvz  25018  nmoleub2lem2  25023  nglmle  25209  mdeg0  25982  dchrinv  27179  dchr1re  27181  dchrpt  27185  dchrsum2  27186  dchrhash  27189  rpvmasumlem  27405  rpvmasum2  27430  dchrisum0re  27431  ogrpinv0lt  33043  ogrpinvlt  33044  conjga  33134  fxpsubm  33136  isarchi3  33148  archirng  33149  archirngz  33150  archiabllem1b  33153  rmfsupp2  33196  erler  33223  rlocaddval  33226  rlocmulval  33227  rloc0g  33229  fracfld  33265  orngsqr  33289  ornglmulle  33290  orngrmulle  33291  ornglmullt  33292  orngrmullt  33293  orngmullt  33294  ofldchr  33299  isarchiofld  33302  qusker  33327  grplsm0l  33381  qus0g  33385  nsgqus0  33388  nsgmgclem  33389  fedgmullem1  33632  irredminply  33713  rtelextdg2lem  33723  qqh0  33981  sconnpi1  35233  lfl0f  39069  lkrlss  39095  lshpkrlem1  39110  lkrin  39164  dvhgrp  41108  primrootscoprmpow  42094  aks5lem7  42195  fsuppind  42585  fsuppssind  42588  mhpind  42589  evl1at0  48384