Theorem grpidcl 18983

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ‘cfv 6561  Basecbs 17247  0_gc0g 17484  Mndcmnd 18747  Grpcgrp 18951

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-riota 7388  df-ov 7434  df-0g 17486  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-grp 18954

This theorem is referenced by:  grpbn0  18984  grprcan  18991  grpid  18993  isgrpid2  18994  grprinv  19008  grpidinv  19016  grpinvid  19017  grpidrcan  19021  grpidlcan  19022  grpidssd  19034  grpinvval2  19041  grpsubid1  19043  imasgrp  19074  mulgcl  19109  mulgz  19120  subg0  19150  subg0cl  19152  issubg4  19163  0subgOLD  19170  nmzsubg  19183  eqgid  19198  eqg0el  19201  qusgrp  19204  qus0  19207  ghmid  19240  ghmpreima  19256  f1ghm0to0  19263  kerf1ghm  19265  ghmqusker  19305  gafo  19314  gaid  19317  gass  19319  gaorber  19326  gastacl  19327  lactghmga  19423  cayleylem2  19431  symgsssg  19485  symgfisg  19486  od1  19577  gexdvds  19602  sylow1lem2  19617  sylow3lem1  19645  lsmdisj2  19700  0frgp  19797  odadd1  19866  torsubg  19872  oddvdssubg  19873  0cyg  19911  prmcyg  19912  telgsums  20011  dprdfadd  20040  dprdz  20050  pgpfac1lem3a  20096  ablsimpgprmd  20135  rng0cl  20160  rnglz  20162  rngrz  20163  ring0cl  20264  zrrnghm  20536  isdomn4  20716  isdrng2  20743  srng0  20855  lmod0vcl  20889  islmhm2  21037  rnglidl0  21239  frgpcyg  21592  ip0l  21654  ocvlss  21690  ascl0  21904  psr0cl  21972  mplsubglem  22019  mhp0cl  22150  mhpaddcl  22155  evl1gsumd  22361  grpvlinv  22402  matinvgcell  22441  mat0dim0  22473  mdetdiag  22605  mdetuni0  22627  chpdmatlem2  22845  chp0mat  22852  istgp2  24099  cldsubg  24119  tgpconncompeqg  24120  tgpconncomp  24121  snclseqg  24124  tgphaus  24125  tgpt1  24126  qustgphaus  24131  tgptsmscls  24158  nrmmetd  24587  nmfval2  24604  nmval2  24605  nmf2  24606  ngpds3  24621  nmge0  24630  nmeq0  24631  nminv  24634  nmmtri  24635  nmrtri  24637  nm0  24642  tngnm  24672  idnghm  24764  nmcn  24866  clmvz  25144  nmoleub2lem2  25149  nglmle  25336  mdeg0  26109  dchrinv  27305  dchr1re  27307  dchrpt  27311  dchrsum2  27312  dchrhash  27315  rpvmasumlem  27531  rpvmasum2  27556  dchrisum0re  27557  ogrpinv0lt  33099  ogrpinvlt  33100  isarchi3  33194  archirng  33195  archirngz  33196  archiabllem1b  33199  rmfsupp2  33242  erler  33269  rlocaddval  33272  rlocmulval  33273  rloc0g  33275  fracfld  33310  orngsqr  33334  ornglmulle  33335  orngrmulle  33336  ornglmullt  33337  orngrmullt  33338  orngmullt  33339  ofldchr  33344  isarchiofld  33347  qusker  33377  grplsm0l  33431  qus0g  33435  nsgqus0  33438  nsgmgclem  33439  fedgmullem1  33680  irredminply  33757  rtelextdg2lem  33767  qqh0  33985  sconnpi1  35244  lfl0f  39070  lkrlss  39096  lshpkrlem1  39111  lkrin  39165  dvhgrp  41109  primrootscoprmpow  42100  aks5lem7  42201  fsuppind  42600  fsuppssind  42603  mhpind  42604  evl1at0  48308