Theorem grpidcl 18995

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  ‘cfv 6562  Basecbs 17244  0_gc0g 17485  Mndcmnd 18759  Grpcgrp 18963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fv 6570  df-riota 7387  df-ov 7433  df-0g 17487  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-grp 18966

This theorem is referenced by:  grpbn0  18996  grprcan  19003  grpid  19005  isgrpid2  19006  grprinv  19020  grpidinv  19028  grpinvid  19029  grpidrcan  19033  grpidlcan  19034  grpidssd  19046  grpinvval2  19053  grpsubid1  19055  imasgrp  19086  mulgcl  19121  mulgz  19132  subg0  19162  subg0cl  19164  issubg4  19175  0subgOLD  19182  nmzsubg  19195  eqgid  19210  eqg0el  19213  qusgrp  19216  qus0  19219  ghmid  19252  ghmpreima  19268  f1ghm0to0  19275  kerf1ghm  19277  ghmqusker  19317  gafo  19326  gaid  19329  gass  19331  gaorber  19338  gastacl  19339  lactghmga  19437  cayleylem2  19445  symgsssg  19499  symgfisg  19500  od1  19591  gexdvds  19616  sylow1lem2  19631  sylow3lem1  19659  lsmdisj2  19714  0frgp  19811  odadd1  19880  torsubg  19886  oddvdssubg  19887  0cyg  19925  prmcyg  19926  telgsums  20025  dprdfadd  20054  dprdz  20064  pgpfac1lem3a  20110  ablsimpgprmd  20149  rng0cl  20180  rnglz  20182  rngrz  20183  ring0cl  20280  zrrnghm  20552  isdomn4  20732  isdrng2  20759  srng0  20871  lmod0vcl  20905  islmhm2  21054  rnglidl0  21256  frgpcyg  21609  ip0l  21671  ocvlss  21707  ascl0  21921  psr0cl  21989  mplsubglem  22036  mhp0cl  22167  mhpaddcl  22172  evl1gsumd  22376  grpvlinv  22417  matinvgcell  22456  mat0dim0  22488  mdetdiag  22620  mdetuni0  22642  chpdmatlem2  22860  chp0mat  22867  istgp2  24114  cldsubg  24134  tgpconncompeqg  24135  tgpconncomp  24136  snclseqg  24139  tgphaus  24140  tgpt1  24141  qustgphaus  24146  tgptsmscls  24173  nrmmetd  24602  nmfval2  24619  nmval2  24620  nmf2  24621  ngpds3  24636  nmge0  24645  nmeq0  24646  nminv  24649  nmmtri  24650  nmrtri  24652  nm0  24657  tngnm  24687  idnghm  24779  nmcn  24879  clmvz  25157  nmoleub2lem2  25162  nglmle  25349  mdeg0  26123  dchrinv  27319  dchr1re  27321  dchrpt  27325  dchrsum2  27326  dchrhash  27329  rpvmasumlem  27545  rpvmasum2  27570  dchrisum0re  27571  ogrpinv0lt  33081  ogrpinvlt  33082  isarchi3  33176  archirng  33177  archirngz  33178  archiabllem1b  33181  rmfsupp2  33227  erler  33251  rlocaddval  33254  rlocmulval  33255  rloc0g  33257  fracfld  33289  orngsqr  33313  ornglmulle  33314  orngrmulle  33315  ornglmullt  33316  orngrmullt  33317  orngmullt  33318  ofldchr  33323  isarchiofld  33326  qusker  33356  grplsm0l  33410  qus0g  33414  nsgqus0  33417  nsgmgclem  33418  fedgmullem1  33656  irredminply  33721  rtelextdg2lem  33731  qqh0  33946  sconnpi1  35223  lfl0f  39050  lkrlss  39076  lshpkrlem1  39091  lkrin  39145  dvhgrp  41089  primrootscoprmpow  42080  aks5lem7  42181  fsuppind  42576  fsuppssind  42579  mhpind  42580  evl1at0  48236