Theorem grpidcl 18983

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

Syntax hints:   → wi 4   = wceq 1554   ∈ wcel 2136  ‘cfv 6510  Basecbs 17221  0_gc0g 17444  Mndcmnd 18744  Grpcgrp 18951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-sep 5240  ax-nul 5250  ax-pr 5384

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ne 2952  df-ral 3071  df-rex 3081  df-rmo 3361  df-reu 3362  df-rab 3409  df-v 3450  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-mpt 5176  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-iota 6466  df-fun 6512  df-fv 6518  df-riota 7342  df-ov 7388  df-0g 17446  df-mgm 18650  df-sgrp 18729  df-mnd 18745  df-grp 18954

This theorem is referenced by:  grpbn0  18984  grprcan  18991  grpid  18993  isgrpid2  18994  grprinv  19008  grpidinv  19016  grpinvid  19017  grpidrcan  19021  grpidlcan  19022  grpidssd  19034  grpinvval2  19041  grpsubid1  19043  imasgrp  19074  mulgcl  19109  mulgz  19120  subg0  19150  subg0cl  19152  issubg4  19163  nmzsubg  19182  eqgid  19197  eqg0el  19200  qusgrp  19203  qus0  19206  ghmid  19238  ghmpreima  19254  f1ghm0to0  19261  kerf1ghm  19263  ghmqusker  19303  gafo  19312  gaid  19315  gass  19317  gaorber  19324  gastacl  19325  lactghmga  19421  cayleylem2  19429  symgsssg  19483  symgfisg  19484  od1  19575  gexdvds  19600  sylow1lem2  19615  sylow3lem1  19643  lsmdisj2  19698  0frgp  19795  odadd1  19864  torsubg  19870  oddvdssubg  19871  0cyg  19909  prmcyg  19910  telgsums  20009  dprdfadd  20038  dprdz  20048  pgpfac1lem3a  20094  ablsimpgprmd  20133  ogrpinv0lt  20159  ogrpinvlt  20160  rng0cl  20185  rnglz  20187  rngrz  20188  ring0cl  20289  zrrnghm  20558  isdomn4  20738  isdrng2  20765  srng0  20876  orngsqr  20888  ornglmulle  20889  orngrmulle  20890  ornglmullt  20891  orngrmullt  20892  orngmullt  20893  lmod0vcl  20931  islmhm2  21078  rnglidl0  21272  frgpcyg  21598  ofldchr  21601  ip0l  21661  ocvlss  21697  ascl0  21909  psr0cl  21977  mplsubglem  22023  mhp0cl  22184  mhpaddcl  22189  evl1gsumd  22393  grpvlinv  22431  matinvgcell  22468  mat0dim0  22500  mdetdiag  22632  mdetuni0  22654  chpdmatlem2  22872  chp0mat  22879  istgp2  24124  cldsubg  24144  tgpconncompeqg  24145  tgpconncomp  24146  snclseqg  24149  tgphaus  24150  tgpt1  24151  qustgphaus  24156  tgptsmscls  24183  nrmmetd  24607  nmfval2  24624  nmval2  24625  nmf2  24626  ngpds3  24641  nmge0  24650  nmeq0  24651  nminv  24654  nmmtri  24655  nmrtri  24657  nm0  24662  tngnm  24684  idnghm  24776  nmcn  24878  clmvz  25146  nmoleub2lem2  25151  nglmle  25337  mdeg0  26103  dchrinv  27295  dchr1re  27297  dchrpt  27301  dchrsum2  27302  dchrhash  27305  rpvmasumlem  27521  rpvmasum2  27546  dchrisum0re  27547  grpidcld  33172  conjga  33304  fxpsubm  33306  fxpsubg  33307  fxpsubrg  33308  isarchi3  33321  archirng  33322  archirngz  33323  archiabllem1b  33326  isarchiofld  33333  rmfsupp2  33372  erler  33400  rlocaddval  33404  rlocmulval  33405  rloc0g  33407  fracfld  33449  qusker  33489  grplsm0l  33543  qus0g  33547  nsgqus0  33550  nsgmgclem  33551  mplvrpmga  33796  mplvrpmmhm  33797  psrmonprod  33803  mplgsum  33804  mplmonprod  33805  esplyind  33826  esplyfvn  33828  fedgmullem1  33880  irredminply  33967  rtelextdg2lem  33977  qqh0  34235  sconnpi1  35537  lfl0f  39641  lkrlss  39667  lshpkrlem1  39682  lkrin  39736  dvhgrp  41679  primrootscoprmpow  42664  aks5lem7  42765  fsuppind  43120  fsuppssind  43123  mhpind  43124  evl1at0  48961