Theorem grpidcl 18899

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6493  Basecbs 17140  0_gc0g 17363  Mndcmnd 18663  Grpcgrp 18867

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 5242  ax-nul 5252  ax-pr 5378

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 3062  df-rmo 3351  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6449  df-fun 6495  df-fv 6501  df-riota 7317  df-ov 7363  df-0g 17365  df-mgm 18569  df-sgrp 18648  df-mnd 18664  df-grp 18870

This theorem is referenced by:  grpbn0  18900  grprcan  18907  grpid  18909  isgrpid2  18910  grprinv  18924  grpidinv  18932  grpinvid  18933  grpidrcan  18937  grpidlcan  18938  grpidssd  18950  grpinvval2  18957  grpsubid1  18959  imasgrp  18990  mulgcl  19025  mulgz  19036  subg0  19066  subg0cl  19068  issubg4  19079  nmzsubg  19098  eqgid  19113  eqg0el  19116  qusgrp  19119  qus0  19122  ghmid  19155  ghmpreima  19171  f1ghm0to0  19178  kerf1ghm  19180  ghmqusker  19220  gafo  19229  gaid  19232  gass  19234  gaorber  19241  gastacl  19242  lactghmga  19338  cayleylem2  19346  symgsssg  19400  symgfisg  19401  od1  19492  gexdvds  19517  sylow1lem2  19532  sylow3lem1  19560  lsmdisj2  19615  0frgp  19712  odadd1  19781  torsubg  19787  oddvdssubg  19788  0cyg  19826  prmcyg  19827  telgsums  19926  dprdfadd  19955  dprdz  19965  pgpfac1lem3a  20011  ablsimpgprmd  20050  ogrpinv0lt  20076  ogrpinvlt  20077  rng0cl  20102  rnglz  20104  rngrz  20105  ring0cl  20206  zrrnghm  20473  isdomn4  20653  isdrng2  20680  srng0  20791  orngsqr  20803  ornglmulle  20804  orngrmulle  20805  ornglmullt  20806  orngrmullt  20807  orngmullt  20808  lmod0vcl  20846  islmhm2  20994  rnglidl0  21188  frgpcyg  21532  ofldchr  21535  ip0l  21595  ocvlss  21631  ascl0  21844  psr0cl  21912  mplsubglem  21958  mhp0cl  22093  mhpaddcl  22098  evl1gsumd  22305  grpvlinv  22346  matinvgcell  22383  mat0dim0  22415  mdetdiag  22547  mdetuni0  22569  chpdmatlem2  22787  chp0mat  22794  istgp2  24039  cldsubg  24059  tgpconncompeqg  24060  tgpconncomp  24061  snclseqg  24064  tgphaus  24065  tgpt1  24066  qustgphaus  24071  tgptsmscls  24098  nrmmetd  24522  nmfval2  24539  nmval2  24540  nmf2  24541  ngpds3  24556  nmge0  24565  nmeq0  24566  nminv  24569  nmmtri  24570  nmrtri  24572  nm0  24577  tngnm  24599  idnghm  24691  nmcn  24793  clmvz  25071  nmoleub2lem2  25076  nglmle  25262  mdeg0  26035  dchrinv  27232  dchr1re  27234  dchrpt  27238  dchrsum2  27239  dchrhash  27242  rpvmasumlem  27458  rpvmasum2  27483  dchrisum0re  27484  conjga  33233  fxpsubm  33235  fxpsubg  33236  fxpsubrg  33237  isarchi3  33250  archirng  33251  archirngz  33252  archiabllem1b  33255  isarchiofld  33262  rmfsupp2  33301  erler  33328  rlocaddval  33331  rlocmulval  33332  rloc0g  33334  fracfld  33371  qusker  33411  grplsm0l  33465  qus0g  33469  nsgqus0  33472  nsgmgclem  33473  mplvrpmga  33691  mplvrpmmhm  33692  esplyind  33712  esplyfvn  33714  fedgmullem1  33767  irredminply  33854  rtelextdg2lem  33864  qqh0  34122  sconnpi1  35414  lfl0f  39366  lkrlss  39392  lshpkrlem1  39407  lkrin  39461  dvhgrp  41404  primrootscoprmpow  42390  aks5lem7  42491  fsuppind  42869  fsuppssind  42872  mhpind  42873  evl1at0  48673