Theorem grpidcl 18929

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  ‘cfv 6553  Basecbs 17187  0_gc0g 17428  Mndcmnd 18701  Grpcgrp 18897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-iota 6505  df-fun 6555  df-fv 6561  df-riota 7382  df-ov 7429  df-0g 17430  df-mgm 18607  df-sgrp 18686  df-mnd 18702  df-grp 18900

This theorem is referenced by:  grpbn0  18930  grprcan  18937  grpid  18939  isgrpid2  18940  grprinv  18954  grpidinv  18962  grpinvid  18963  grpidrcan  18967  grpidlcan  18968  grpidssd  18979  grpinvval2  18986  grpsubid1  18988  imasgrp  19019  mulgcl  19053  mulgz  19064  subg0  19094  subg0cl  19096  issubg4  19107  0subgOLD  19114  nmzsubg  19127  eqgid  19142  eqg0el  19145  qusgrp  19148  qus0  19151  ghmid  19183  ghmpreima  19199  f1ghm0to0  19206  kerf1ghm  19208  ghmqusker  19245  gafo  19254  gaid  19257  gass  19259  gaorber  19266  gastacl  19267  lactghmga  19367  cayleylem2  19375  symgsssg  19429  symgfisg  19430  od1  19521  gexdvds  19546  sylow1lem2  19561  sylow3lem1  19589  lsmdisj2  19644  0frgp  19741  odadd1  19810  torsubg  19816  oddvdssubg  19817  0cyg  19855  prmcyg  19856  telgsums  19955  dprdfadd  19984  dprdz  19994  pgpfac1lem3a  20040  ablsimpgprmd  20079  rng0cl  20110  rnglz  20112  rngrz  20113  ring0cl  20210  zrrnghm  20480  isdrng2  20645  srng0  20747  lmod0vcl  20781  islmhm2  20930  rnglidl0  21132  isdomn4  21257  frgpcyg  21514  ip0l  21575  ocvlss  21611  ascl0  21824  psr0cl  21902  mplsubglem  21948  mhp0cl  22077  mhpaddcl  22082  evl1gsumd  22283  grpvlinv  22317  matinvgcell  22357  mat0dim0  22389  mdetdiag  22521  mdetuni0  22543  chpdmatlem2  22761  chp0mat  22768  istgp2  24015  cldsubg  24035  tgpconncompeqg  24036  tgpconncomp  24037  snclseqg  24040  tgphaus  24041  tgpt1  24042  qustgphaus  24047  tgptsmscls  24074  nrmmetd  24503  nmfval2  24520  nmval2  24521  nmf2  24522  ngpds3  24537  nmge0  24546  nmeq0  24547  nminv  24550  nmmtri  24551  nmrtri  24553  nm0  24558  tngnm  24588  idnghm  24680  nmcn  24780  clmvz  25058  nmoleub2lem2  25063  nglmle  25250  mdeg0  26026  dchrinv  27214  dchr1re  27216  dchrpt  27220  dchrsum2  27221  dchrhash  27224  rpvmasumlem  27440  rpvmasum2  27465  dchrisum0re  27466  ogrpinv0lt  32823  ogrpinvlt  32824  isarchi3  32916  archirng  32917  archirngz  32918  archiabllem1b  32921  rmfsupp2  32966  erler  33004  rlocaddval  33007  rlocmulval  33008  rloc0g  33010  fracfld  33019  orngsqr  33043  ornglmulle  33044  orngrmulle  33045  ornglmullt  33046  orngrmullt  33047  orngmullt  33048  ofldchr  33053  isarchiofld  33056  qusker  33085  grplsm0l  33137  qus0g  33142  nsgqus0  33145  nsgmgclem  33146  fedgmullem1  33360  irredminply  33417  qqh0  33618  sconnpi1  34882  lfl0f  38573  lkrlss  38599  lshpkrlem1  38614  lkrin  38668  dvhgrp  40612  primrootscoprmpow  41602  fsuppind  41854  fsuppssind  41857  mhpind  41858  evl1at0  47537