Theorem grpidcl 18616

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  ‘cfv 6437  Basecbs 16921  0_gc0g 17159  Mndcmnd 18394  Grpcgrp 18586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rmo 3072  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6395  df-fun 6439  df-fv 6445  df-riota 7241  df-ov 7287  df-0g 17161  df-mgm 18335  df-sgrp 18384  df-mnd 18395  df-grp 18589

This theorem is referenced by:  grpbn0  18617  grprcan  18622  grpid  18624  isgrpid2  18625  grprinv  18638  grpidinv  18644  grpinvid  18645  grpidrcan  18649  grpidlcan  18650  grpidssd  18660  grpinvval2  18667  grpsubid1  18669  imasgrp  18700  mulgcl  18730  mulgz  18740  subg0  18770  subg0cl  18772  issubg4  18783  0subg  18789  nmzsubg  18802  eqgid  18817  qusgrp  18820  qus0  18823  ghmid  18849  ghmpreima  18865  ghmf1  18872  gafo  18911  gaid  18914  gass  18916  gaorber  18923  gastacl  18924  lactghmga  19022  cayleylem2  19030  symgsssg  19084  symgfisg  19085  od1  19175  gexdvds  19198  sylow1lem2  19213  sylow3lem1  19241  lsmdisj2  19297  0frgp  19394  odadd1  19458  torsubg  19464  oddvdssubg  19465  0cyg  19503  prmcyg  19504  telgsums  19603  dprdfadd  19632  dprdz  19642  pgpfac1lem3a  19688  ablsimpgprmd  19727  ring0cl  19817  ringlz  19835  ringrz  19836  f1ghm0to0  19993  kerf1ghm  19996  isdrng2  20010  srng0  20129  lmod0vcl  20161  islmhm2  20309  frgpcyg  20790  ip0l  20850  ocvlss  20886  ascl0  21097  psr0cl  21172  mplsubglem  21214  mhp0cl  21345  mhpaddcl  21350  evl1gsumd  21532  grpvlinv  21553  matinvgcell  21593  mat0dim0  21625  mdetdiag  21757  mdetuni0  21779  chpdmatlem2  21997  chp0mat  22004  istgp2  23251  cldsubg  23271  tgpconncompeqg  23272  tgpconncomp  23273  snclseqg  23276  tgphaus  23277  tgpt1  23278  qustgphaus  23283  tgptsmscls  23310  nrmmetd  23739  nmfval2  23756  nmval2  23757  nmf2  23758  ngpds3  23773  nmge0  23782  nmeq0  23783  nminv  23786  nmmtri  23787  nmrtri  23789  nm0  23794  tngnm  23824  idnghm  23916  nmcn  24016  clmvz  24283  nmoleub2lem2  24288  nglmle  24475  mdeg0  25244  dchrinv  26418  dchr1re  26420  dchrpt  26424  dchrsum2  26425  dchrhash  26428  rpvmasumlem  26644  rpvmasum2  26669  dchrisum0re  26670  ogrpinv0lt  31357  ogrpinvlt  31358  isarchi3  31450  archirng  31451  archirngz  31452  archiabllem1b  31455  rmfsupp2  31501  orngsqr  31512  ornglmulle  31513  orngrmulle  31514  ornglmullt  31515  orngrmullt  31516  orngmullt  31517  ofldchr  31522  isarchiofld  31525  qusker  31558  eqg0el  31566  grplsm0l  31600  nsgqus0  31604  nsgmgclem  31605  fedgmullem1  31719  qqh0  31943  sconnpi1  33210  lfl0f  37090  lkrlss  37116  lshpkrlem1  37131  lkrin  37185  dvhgrp  39128  isdomn4  40179  fsuppind  40286  fsuppssind  40289  mhpind  40290  rnglz  45453  zrrnghm  45486  evl1at0  45743