Theorem grpidcl 18862

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6486  Basecbs 17138  0_gc0g 17361  Mndcmnd 18626  Grpcgrp 18830

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  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 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3345  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494  df-riota 7310  df-ov 7356  df-0g 17363  df-mgm 18532  df-sgrp 18611  df-mnd 18627  df-grp 18833

This theorem is referenced by:  grpbn0  18863  grprcan  18870  grpid  18872  isgrpid2  18873  grprinv  18887  grpidinv  18895  grpinvid  18896  grpidrcan  18900  grpidlcan  18901  grpidssd  18913  grpinvval2  18920  grpsubid1  18922  imasgrp  18953  mulgcl  18988  mulgz  18999  subg0  19029  subg0cl  19031  issubg4  19042  0subgOLD  19049  nmzsubg  19062  eqgid  19077  eqg0el  19080  qusgrp  19083  qus0  19086  ghmid  19119  ghmpreima  19135  f1ghm0to0  19142  kerf1ghm  19144  ghmqusker  19184  gafo  19193  gaid  19196  gass  19198  gaorber  19205  gastacl  19206  lactghmga  19302  cayleylem2  19310  symgsssg  19364  symgfisg  19365  od1  19456  gexdvds  19481  sylow1lem2  19496  sylow3lem1  19524  lsmdisj2  19579  0frgp  19676  odadd1  19745  torsubg  19751  oddvdssubg  19752  0cyg  19790  prmcyg  19791  telgsums  19890  dprdfadd  19919  dprdz  19929  pgpfac1lem3a  19975  ablsimpgprmd  20014  ogrpinv0lt  20040  ogrpinvlt  20041  rng0cl  20066  rnglz  20068  rngrz  20069  ring0cl  20170  zrrnghm  20439  isdomn4  20619  isdrng2  20646  srng0  20757  orngsqr  20769  ornglmulle  20770  orngrmulle  20771  ornglmullt  20772  orngrmullt  20773  orngmullt  20774  lmod0vcl  20812  islmhm2  20960  rnglidl0  21154  frgpcyg  21498  ofldchr  21501  ip0l  21561  ocvlss  21597  ascl0  21809  psr0cl  21877  mplsubglem  21924  mhp0cl  22049  mhpaddcl  22054  evl1gsumd  22260  grpvlinv  22301  matinvgcell  22338  mat0dim0  22370  mdetdiag  22502  mdetuni0  22524  chpdmatlem2  22742  chp0mat  22749  istgp2  23994  cldsubg  24014  tgpconncompeqg  24015  tgpconncomp  24016  snclseqg  24019  tgphaus  24020  tgpt1  24021  qustgphaus  24026  tgptsmscls  24053  nrmmetd  24478  nmfval2  24495  nmval2  24496  nmf2  24497  ngpds3  24512  nmge0  24521  nmeq0  24522  nminv  24525  nmmtri  24526  nmrtri  24528  nm0  24533  tngnm  24555  idnghm  24647  nmcn  24749  clmvz  25027  nmoleub2lem2  25032  nglmle  25218  mdeg0  25991  dchrinv  27188  dchr1re  27190  dchrpt  27194  dchrsum2  27195  dchrhash  27198  rpvmasumlem  27414  rpvmasum2  27439  dchrisum0re  27440  conjga  33125  fxpsubm  33127  isarchi3  33139  archirng  33140  archirngz  33141  archiabllem1b  33144  isarchiofld  33151  rmfsupp2  33188  erler  33215  rlocaddval  33218  rlocmulval  33219  rloc0g  33221  fracfld  33257  qusker  33296  grplsm0l  33350  qus0g  33354  nsgqus0  33357  nsgmgclem  33358  fedgmullem1  33601  irredminply  33682  rtelextdg2lem  33692  qqh0  33950  sconnpi1  35211  lfl0f  39047  lkrlss  39073  lshpkrlem1  39088  lkrin  39142  dvhgrp  41086  primrootscoprmpow  42072  aks5lem7  42173  fsuppind  42563  fsuppssind  42566  mhpind  42567  evl1at0  48364