Theorem grpidcl 19022

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  ‘cfv 6525  Basecbs 17259  0_gc0g 17482  Mndcmnd 18782  Grpcgrp 18990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-iota 6481  df-fun 6527  df-fv 6533  df-riota 7357  df-ov 7403  df-0g 17484  df-mgm 18688  df-sgrp 18767  df-mnd 18783  df-grp 18993

This theorem is referenced by:  grpbn0  19023  grprcan  19030  grpid  19032  isgrpid2  19033  grprinv  19047  grpidinv  19055  grpinvid  19056  grpidrcan  19060  grpidlcan  19061  grpidssd  19073  grpinvval2  19080  grpsubid1  19082  imasgrp  19113  mulgcl  19148  mulgz  19159  subg0  19189  subg0cl  19191  issubg4  19203  nmzsubg  19222  eqgid  19239  eqg0el  19245  qusgrp  19248  qus0  19251  ghmid  19283  ghmpreima  19299  f1ghm0to0  19306  kerf1ghm  19308  ghmqusker  19348  gafo  19357  gaid  19360  gass  19362  gaorber  19369  gastacl  19370  lactghmga  19466  cayleylem2  19474  symgsssg  19528  symgfisg  19529  od1  19620  gexdvds  19645  sylow1lem2  19660  sylow3lem1  19688  lsmdisj2  19743  0frgp  19840  odadd1  19909  torsubg  19915  oddvdssubg  19916  0cyg  19954  prmcyg  19955  telgsums  20054  dprdfadd  20083  dprdz  20093  pgpfac1lem3a  20139  ablsimpgprmd  20178  ogrpinv0lt  20204  ogrpinvlt  20205  rng0cl  20232  rnglz  20234  rngrz  20235  ring0cl  20341  zrrnghm  20612  isdomn4  20791  isdrng2  20818  srng0  20926  orngsqr  20938  ornglmulle  20939  orngrmulle  20940  ornglmullt  20941  orngrmullt  20942  orngmullt  20943  lmod0vcl  20981  islmhm2  21128  rnglidl0  21324  frgpcyg  21683  ofldchr  21686  ip0l  21746  ocvlss  21782  ascl0  21994  psr0cl  22062  mplsubglem  22108  mhp0cl  22269  mhpaddcl  22274  evl1gsumd  22478  grpvlinv  22516  matinvgcell  22553  mat0dim0  22585  mdetdiag  22717  mdetuni0  22739  chpdmatlem2  22957  chp0mat  22964  istgp2  24209  cldsubg  24229  tgpconncompeqg  24230  tgpconncomp  24231  snclseqg  24234  tgphaus  24235  tgpt1  24236  qustgphaus  24241  tgptsmscls  24268  nrmmetd  24692  nmfval2  24709  nmval2  24710  nmf2  24711  ngpds3  24726  nmge0  24735  nmeq0  24736  nminv  24739  nmmtri  24740  nmrtri  24742  nm0  24747  tngnm  24769  idnghm  24861  nmcn  24963  clmvz  25231  nmoleub2lem2  25236  nglmle  25422  mdeg0  26188  dchrinv  27383  dchr1re  27385  dchrpt  27389  dchrsum2  27390  dchrhash  27393  rpvmasumlem  27609  rpvmasum2  27634  dchrisum0re  27635  grpidcld  33272  conjga  33403  fxpsubm  33405  fxpsubg  33406  fxpsubrg  33407  isarchi3  33420  archirng  33421  archirngz  33422  archiabllem1b  33425  isarchiofld  33432  rmfsupp2  33470  erler  33498  rlocaddval  33502  rlocmulval  33503  rloc0g  33505  fracfld  33544  qusker  33584  grplsm0l  33628  qus0g  33632  nsgqus0  33635  nsgmgclem  33636  mplvrpmga  33852  mplvrpmmhm  33853  psrmonprod  33859  mplgsum  33860  mplmonprod  33861  esplyind  33882  esplyfvn  33884  fedgmullem1  33936  irredminply  34023  rtelextdg2lem  34033  qqh0  34291  sconnpi1  35602  lfl0f  39705  lkrlss  39731  lshpkrlem1  39746  lkrin  39800  dvhgrp  41743  primrootscoprmpow  42728  aks5lem7  42829  fsuppind  43184  fsuppssind  43187  mhpind  43188  evl1at0  49022