Theorem grpidcl 18886

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104  ‘cfv 6542  Basecbs 17148  0_gc0g 17389  Mndcmnd 18659  Grpcgrp 18855

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6494  df-fun 6544  df-fv 6550  df-riota 7367  df-ov 7414  df-0g 17391  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-grp 18858

This theorem is referenced by:  grpbn0  18887  grprcan  18894  grpid  18896  isgrpid2  18897  grprinv  18911  grpidinv  18919  grpinvid  18920  grpidrcan  18924  grpidlcan  18925  grpidssd  18935  grpinvval2  18942  grpsubid1  18944  imasgrp  18975  mulgcl  19007  mulgz  19018  subg0  19048  subg0cl  19050  issubg4  19061  0subgOLD  19068  nmzsubg  19081  eqgid  19096  qusgrp  19101  qus0  19104  ghmid  19136  ghmpreima  19152  f1ghm0to0  19159  kerf1ghm  19161  gafo  19201  gaid  19204  gass  19206  gaorber  19213  gastacl  19214  lactghmga  19314  cayleylem2  19322  symgsssg  19376  symgfisg  19377  od1  19468  gexdvds  19493  sylow1lem2  19508  sylow3lem1  19536  lsmdisj2  19591  0frgp  19688  odadd1  19757  torsubg  19763  oddvdssubg  19764  0cyg  19802  prmcyg  19803  telgsums  19902  dprdfadd  19931  dprdz  19941  pgpfac1lem3a  19987  ablsimpgprmd  20026  rng0cl  20057  rnglz  20059  rngrz  20060  ring0cl  20155  zrrnghm  20425  isdrng2  20514  srng0  20611  lmod0vcl  20645  islmhm2  20793  rnglidl0  21032  isdomn4  21118  frgpcyg  21348  ip0l  21408  ocvlss  21444  ascl0  21657  psr0cl  21732  mplsubglem  21777  mhp0cl  21908  mhpaddcl  21913  evl1gsumd  22096  grpvlinv  22117  matinvgcell  22157  mat0dim0  22189  mdetdiag  22321  mdetuni0  22343  chpdmatlem2  22561  chp0mat  22568  istgp2  23815  cldsubg  23835  tgpconncompeqg  23836  tgpconncomp  23837  snclseqg  23840  tgphaus  23841  tgpt1  23842  qustgphaus  23847  tgptsmscls  23874  nrmmetd  24303  nmfval2  24320  nmval2  24321  nmf2  24322  ngpds3  24337  nmge0  24346  nmeq0  24347  nminv  24350  nmmtri  24351  nmrtri  24353  nm0  24358  tngnm  24388  idnghm  24480  nmcn  24580  clmvz  24858  nmoleub2lem2  24863  nglmle  25050  mdeg0  25823  dchrinv  27000  dchr1re  27002  dchrpt  27006  dchrsum2  27007  dchrhash  27010  rpvmasumlem  27226  rpvmasum2  27251  dchrisum0re  27252  ogrpinv0lt  32510  ogrpinvlt  32511  isarchi3  32603  archirng  32604  archirngz  32605  archiabllem1b  32608  rmfsupp2  32657  orngsqr  32692  ornglmulle  32693  orngrmulle  32694  ornglmullt  32695  orngrmullt  32696  orngmullt  32697  ofldchr  32702  isarchiofld  32705  qusker  32734  eqg0el  32747  grplsm0l  32787  qus0g  32792  nsgqus0  32795  nsgmgclem  32796  ghmqusker  32806  fedgmullem1  33002  qqh0  33262  sconnpi1  34528  lfl0f  38242  lkrlss  38268  lshpkrlem1  38283  lkrin  38337  dvhgrp  40281  fsuppind  41464  fsuppssind  41467  mhpind  41468  evl1at0  47159