Theorem grpidcl 18907

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6500  Basecbs 17148  0_gc0g 17371  Mndcmnd 18671  Grpcgrp 18875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-riota 7325  df-ov 7371  df-0g 17373  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-grp 18878

This theorem is referenced by:  grpbn0  18908  grprcan  18915  grpid  18917  isgrpid2  18918  grprinv  18932  grpidinv  18940  grpinvid  18941  grpidrcan  18945  grpidlcan  18946  grpidssd  18958  grpinvval2  18965  grpsubid1  18967  imasgrp  18998  mulgcl  19033  mulgz  19044  subg0  19074  subg0cl  19076  issubg4  19087  nmzsubg  19106  eqgid  19121  eqg0el  19124  qusgrp  19127  qus0  19130  ghmid  19163  ghmpreima  19179  f1ghm0to0  19186  kerf1ghm  19188  ghmqusker  19228  gafo  19237  gaid  19240  gass  19242  gaorber  19249  gastacl  19250  lactghmga  19346  cayleylem2  19354  symgsssg  19408  symgfisg  19409  od1  19500  gexdvds  19525  sylow1lem2  19540  sylow3lem1  19568  lsmdisj2  19623  0frgp  19720  odadd1  19789  torsubg  19795  oddvdssubg  19796  0cyg  19834  prmcyg  19835  telgsums  19934  dprdfadd  19963  dprdz  19973  pgpfac1lem3a  20019  ablsimpgprmd  20058  ogrpinv0lt  20084  ogrpinvlt  20085  rng0cl  20110  rnglz  20112  rngrz  20113  ring0cl  20214  zrrnghm  20481  isdomn4  20661  isdrng2  20688  srng0  20799  orngsqr  20811  ornglmulle  20812  orngrmulle  20813  ornglmullt  20814  orngrmullt  20815  orngmullt  20816  lmod0vcl  20854  islmhm2  21002  rnglidl0  21196  frgpcyg  21540  ofldchr  21543  ip0l  21603  ocvlss  21639  ascl0  21852  psr0cl  21920  mplsubglem  21966  mhp0cl  22101  mhpaddcl  22106  evl1gsumd  22313  grpvlinv  22354  matinvgcell  22391  mat0dim0  22423  mdetdiag  22555  mdetuni0  22577  chpdmatlem2  22795  chp0mat  22802  istgp2  24047  cldsubg  24067  tgpconncompeqg  24068  tgpconncomp  24069  snclseqg  24072  tgphaus  24073  tgpt1  24074  qustgphaus  24079  tgptsmscls  24106  nrmmetd  24530  nmfval2  24547  nmval2  24548  nmf2  24549  ngpds3  24564  nmge0  24573  nmeq0  24574  nminv  24577  nmmtri  24578  nmrtri  24580  nm0  24585  tngnm  24607  idnghm  24699  nmcn  24801  clmvz  25079  nmoleub2lem2  25084  nglmle  25270  mdeg0  26043  dchrinv  27240  dchr1re  27242  dchrpt  27246  dchrsum2  27247  dchrhash  27250  rpvmasumlem  27466  rpvmasum2  27491  dchrisum0re  27492  conjga  33263  fxpsubm  33265  fxpsubg  33266  fxpsubrg  33267  isarchi3  33280  archirng  33281  archirngz  33282  archiabllem1b  33285  isarchiofld  33292  rmfsupp2  33331  erler  33358  rlocaddval  33361  rlocmulval  33362  rloc0g  33364  fracfld  33401  qusker  33441  grplsm0l  33495  qus0g  33499  nsgqus0  33502  nsgmgclem  33503  mplvrpmga  33721  mplvrpmmhm  33722  psrmonprod  33728  mplgsum  33729  mplmonprod  33730  esplyind  33751  esplyfvn  33753  fedgmullem1  33806  irredminply  33893  rtelextdg2lem  33903  qqh0  34161  sconnpi1  35452  lfl0f  39434  lkrlss  39460  lshpkrlem1  39475  lkrin  39529  dvhgrp  41472  primrootscoprmpow  42458  aks5lem7  42559  fsuppind  42937  fsuppssind  42940  mhpind  42941  evl1at0  48740