Theorem grpidcl 18125

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110  ‘cfv 6349  Basecbs 16477  0_gc0g 16707  Mndcmnd 17905  Grpcgrp 18097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-iota 6308  df-fun 6351  df-fv 6357  df-riota 7108  df-ov 7153  df-0g 16709  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-grp 18100

This theorem is referenced by:  grpbn0  18126  grprcan  18131  grpid  18133  isgrpid2  18134  grprinv  18147  grpidinv  18153  grpinvid  18154  grpidrcan  18158  grpidlcan  18159  grpidssd  18169  grpinvval2  18176  grpsubid1  18178  imasgrp  18209  mulgcl  18239  mulgz  18249  subg0  18279  subg0cl  18281  issubg4  18292  0subg  18298  nmzsubg  18311  eqgid  18326  qusgrp  18329  qus0  18332  ghmid  18358  ghmpreima  18374  ghmf1  18381  gafo  18420  gaid  18423  gass  18425  gaorber  18432  gastacl  18433  lactghmga  18527  cayleylem2  18535  symgsssg  18589  symgfisg  18590  od1  18680  gexdvds  18703  sylow1lem2  18718  sylow3lem1  18746  lsmdisj2  18802  0frgp  18899  odadd1  18962  torsubg  18968  oddvdssubg  18969  0cyg  19007  prmcyg  19008  telgsums  19107  dprdfadd  19136  dprdz  19146  pgpfac1lem3a  19192  ablsimpgprmd  19231  ring0cl  19313  ringlz  19331  ringrz  19332  f1ghm0to0  19486  kerf1ghm  19491  kerf1hrmOLD  19492  isdrng2  19506  srng0  19625  lmod0vcl  19657  islmhm2  19804  ascl0  20107  psr0cl  20168  mplsubglem  20208  mhp0cl  20331  mhpaddcl  20332  mhpinvcl  20333  evl1gsumd  20514  frgpcyg  20714  ip0l  20774  ocvlss  20810  grpvlinv  21000  matinvgcell  21038  mat0dim0  21070  mdetdiag  21202  mdetuni0  21224  chpdmatlem2  21441  chp0mat  21448  istgp2  22693  cldsubg  22713  tgpconncompeqg  22714  tgpconncomp  22715  snclseqg  22718  tgphaus  22719  tgpt1  22720  qustgphaus  22725  tgptsmscls  22752  nrmmetd  23178  nmfval2  23194  nmval2  23195  nmf2  23196  ngpds3  23211  nmge0  23220  nmeq0  23221  nminv  23224  nmmtri  23225  nmrtri  23227  nm0  23232  tngnm  23254  idnghm  23346  nmcn  23446  clmvz  23709  nmoleub2lem2  23714  nglmle  23899  mdeg0  24658  dchrinv  25831  dchr1re  25833  dchrpt  25837  dchrsum2  25838  dchrhash  25841  rpvmasumlem  26057  rpvmasum2  26082  dchrisum0re  26083  ogrpinv0lt  30718  ogrpinvlt  30719  isarchi3  30811  archirng  30812  archirngz  30813  archiabllem1b  30816  rmfsupp2  30861  orngsqr  30872  ornglmulle  30873  orngrmulle  30874  ornglmullt  30875  orngrmullt  30876  orngmullt  30877  ofldchr  30882  isarchiofld  30885  qusker  30913  eqg0el  30921  fedgmullem1  31020  qqh0  31220  sconnpi1  32481  lfl0f  36199  lkrlss  36225  lshpkrlem1  36240  lkrin  36294  dvhgrp  38237  rnglz  44149  zrrnghm  44182  evl1at0  44439