Theorem grpidcl 18930

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6490  Basecbs 17168  0_gc0g 17391  Mndcmnd 18691  Grpcgrp 18898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-iota 6446  df-fun 6492  df-fv 6498  df-riota 7315  df-ov 7361  df-0g 17393  df-mgm 18597  df-sgrp 18676  df-mnd 18692  df-grp 18901

This theorem is referenced by:  grpbn0  18931  grprcan  18938  grpid  18940  isgrpid2  18941  grprinv  18955  grpidinv  18963  grpinvid  18964  grpidrcan  18968  grpidlcan  18969  grpidssd  18981  grpinvval2  18988  grpsubid1  18990  imasgrp  19021  mulgcl  19056  mulgz  19067  subg0  19097  subg0cl  19099  issubg4  19110  nmzsubg  19129  eqgid  19144  eqg0el  19147  qusgrp  19150  qus0  19153  ghmid  19186  ghmpreima  19202  f1ghm0to0  19209  kerf1ghm  19211  ghmqusker  19251  gafo  19260  gaid  19263  gass  19265  gaorber  19272  gastacl  19273  lactghmga  19369  cayleylem2  19377  symgsssg  19431  symgfisg  19432  od1  19523  gexdvds  19548  sylow1lem2  19563  sylow3lem1  19591  lsmdisj2  19646  0frgp  19743  odadd1  19812  torsubg  19818  oddvdssubg  19819  0cyg  19857  prmcyg  19858  telgsums  19957  dprdfadd  19986  dprdz  19996  pgpfac1lem3a  20042  ablsimpgprmd  20081  ogrpinv0lt  20107  ogrpinvlt  20108  rng0cl  20133  rnglz  20135  rngrz  20136  ring0cl  20237  zrrnghm  20502  isdomn4  20682  isdrng2  20709  srng0  20820  orngsqr  20832  ornglmulle  20833  orngrmulle  20834  ornglmullt  20835  orngrmullt  20836  orngmullt  20837  lmod0vcl  20875  islmhm2  21023  rnglidl0  21217  frgpcyg  21561  ofldchr  21564  ip0l  21624  ocvlss  21660  ascl0  21872  psr0cl  21940  mplsubglem  21986  mhp0cl  22121  mhpaddcl  22126  evl1gsumd  22331  grpvlinv  22372  matinvgcell  22409  mat0dim0  22441  mdetdiag  22573  mdetuni0  22595  chpdmatlem2  22813  chp0mat  22820  istgp2  24065  cldsubg  24085  tgpconncompeqg  24086  tgpconncomp  24087  snclseqg  24090  tgphaus  24091  tgpt1  24092  qustgphaus  24097  tgptsmscls  24124  nrmmetd  24548  nmfval2  24565  nmval2  24566  nmf2  24567  ngpds3  24582  nmge0  24591  nmeq0  24592  nminv  24595  nmmtri  24596  nmrtri  24598  nm0  24603  tngnm  24625  idnghm  24717  nmcn  24819  clmvz  25087  nmoleub2lem2  25092  nglmle  25278  mdeg0  26047  dchrinv  27243  dchr1re  27245  dchrpt  27249  dchrsum2  27250  dchrhash  27253  rpvmasumlem  27469  rpvmasum2  27494  dchrisum0re  27495  conjga  33251  fxpsubm  33253  fxpsubg  33254  fxpsubrg  33255  isarchi3  33268  archirng  33269  archirngz  33270  archiabllem1b  33273  isarchiofld  33280  rmfsupp2  33319  erler  33346  rlocaddval  33349  rlocmulval  33350  rloc0g  33352  fracfld  33389  qusker  33429  grplsm0l  33483  qus0g  33487  nsgqus0  33490  nsgmgclem  33491  mplvrpmga  33709  mplvrpmmhm  33710  psrmonprod  33716  mplgsum  33717  mplmonprod  33718  esplyind  33739  esplyfvn  33741  fedgmullem1  33794  irredminply  33881  rtelextdg2lem  33891  qqh0  34149  sconnpi1  35442  lfl0f  39526  lkrlss  39552  lshpkrlem1  39567  lkrin  39621  dvhgrp  41564  primrootscoprmpow  42549  aks5lem7  42650  fsuppind  43034  fsuppssind  43037  mhpind  43038  evl1at0  48864