Theorem grpidcl 18888

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ‘cfv 6489  Basecbs 17130  0_gc0g 17353  Mndcmnd 18652  Grpcgrp 18856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-iota 6445  df-fun 6491  df-fv 6497  df-riota 7312  df-ov 7358  df-0g 17355  df-mgm 18558  df-sgrp 18637  df-mnd 18653  df-grp 18859

This theorem is referenced by:  grpbn0  18889  grprcan  18896  grpid  18898  isgrpid2  18899  grprinv  18913  grpidinv  18921  grpinvid  18922  grpidrcan  18926  grpidlcan  18927  grpidssd  18939  grpinvval2  18946  grpsubid1  18948  imasgrp  18979  mulgcl  19014  mulgz  19025  subg0  19055  subg0cl  19057  issubg4  19068  nmzsubg  19087  eqgid  19102  eqg0el  19105  qusgrp  19108  qus0  19111  ghmid  19144  ghmpreima  19160  f1ghm0to0  19167  kerf1ghm  19169  ghmqusker  19209  gafo  19218  gaid  19221  gass  19223  gaorber  19230  gastacl  19231  lactghmga  19327  cayleylem2  19335  symgsssg  19389  symgfisg  19390  od1  19481  gexdvds  19506  sylow1lem2  19521  sylow3lem1  19549  lsmdisj2  19604  0frgp  19701  odadd1  19770  torsubg  19776  oddvdssubg  19777  0cyg  19815  prmcyg  19816  telgsums  19915  dprdfadd  19944  dprdz  19954  pgpfac1lem3a  20000  ablsimpgprmd  20039  ogrpinv0lt  20065  ogrpinvlt  20066  rng0cl  20091  rnglz  20093  rngrz  20094  ring0cl  20195  zrrnghm  20461  isdomn4  20641  isdrng2  20668  srng0  20779  orngsqr  20791  ornglmulle  20792  orngrmulle  20793  ornglmullt  20794  orngrmullt  20795  orngmullt  20796  lmod0vcl  20834  islmhm2  20982  rnglidl0  21176  frgpcyg  21520  ofldchr  21523  ip0l  21583  ocvlss  21619  ascl0  21831  psr0cl  21899  mplsubglem  21946  mhp0cl  22071  mhpaddcl  22076  evl1gsumd  22282  grpvlinv  22323  matinvgcell  22360  mat0dim0  22392  mdetdiag  22524  mdetuni0  22546  chpdmatlem2  22764  chp0mat  22771  istgp2  24016  cldsubg  24036  tgpconncompeqg  24037  tgpconncomp  24038  snclseqg  24041  tgphaus  24042  tgpt1  24043  qustgphaus  24048  tgptsmscls  24075  nrmmetd  24499  nmfval2  24516  nmval2  24517  nmf2  24518  ngpds3  24533  nmge0  24542  nmeq0  24543  nminv  24546  nmmtri  24547  nmrtri  24549  nm0  24554  tngnm  24576  idnghm  24668  nmcn  24770  clmvz  25048  nmoleub2lem2  25053  nglmle  25239  mdeg0  26012  dchrinv  27209  dchr1re  27211  dchrpt  27215  dchrsum2  27216  dchrhash  27219  rpvmasumlem  27435  rpvmasum2  27460  dchrisum0re  27461  conjga  33150  fxpsubm  33152  fxpsubg  33153  fxpsubrg  33154  isarchi3  33167  archirng  33168  archirngz  33169  archiabllem1b  33172  isarchiofld  33179  rmfsupp2  33216  erler  33243  rlocaddval  33246  rlocmulval  33247  rloc0g  33249  fracfld  33285  qusker  33325  grplsm0l  33379  qus0g  33383  nsgqus0  33386  nsgmgclem  33387  mplvrpmga  33586  mplvrpmmhm  33587  fedgmullem1  33653  irredminply  33740  rtelextdg2lem  33750  qqh0  34008  sconnpi1  35294  lfl0f  39178  lkrlss  39204  lshpkrlem1  39219  lkrin  39273  dvhgrp  41216  primrootscoprmpow  42202  aks5lem7  42303  fsuppind  42698  fsuppssind  42701  mhpind  42702  evl1at0  48506