Theorem grpidcl 19031

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  ‘cfv 6536  Basecbs 17268  0_gc0g 17491  Mndcmnd 18791  Grpcgrp 18999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3744  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-iota 6492  df-fun 6538  df-fv 6544  df-riota 7367  df-ov 7413  df-0g 17493  df-mgm 18697  df-sgrp 18776  df-mnd 18792  df-grp 19002

This theorem is referenced by:  grpbn0  19032  grprcan  19039  grpid  19041  isgrpid2  19042  grprinv  19056  grpidinv  19064  grpinvid  19065  grpidrcan  19069  grpidlcan  19070  grpidssd  19081  grpinvval2  19088  grpsubid1  19090  imasgrp  19121  mulgcl  19156  mulgz  19167  subg0  19197  subg0cl  19199  issubg4  19211  nmzsubg  19230  eqgid  19247  eqg0el  19253  qusgrp  19256  qus0  19259  ghmid  19291  ghmpreima  19307  f1ghm0to0  19314  kerf1ghm  19316  ghmqusker  19356  gafo  19365  gaid  19368  gass  19370  gaorber  19377  gastacl  19378  lactghmga  19474  cayleylem2  19482  symgsssg  19536  symgfisg  19537  od1  19628  gexdvds  19653  sylow1lem2  19668  sylow3lem1  19696  lsmdisj2  19751  0frgp  19848  odadd1  19917  torsubg  19923  oddvdssubg  19924  0cyg  19962  prmcyg  19963  telgsums  20062  dprdfadd  20091  dprdz  20101  pgpfac1lem3a  20147  ablsimpgprmd  20186  ogrpinv0lt  20212  ogrpinvlt  20213  rng0cl  20240  rnglz  20242  rngrz  20243  ring0cl  20349  zrrnghm  20620  isdomn4  20799  isdrng2  20828  srng0  20936  orngsqr  20948  ornglmulle  20949  orngrmulle  20950  ornglmullt  20951  orngrmullt  20952  orngmullt  20953  lmod0vcl  20991  islmhm2  21138  rnglidl0  21334  frgpcyg  21702  ofldchr  21705  ip0l  21765  ocvlss  21801  ascl0  22013  psr0cl  22081  mplsubglem  22127  mhp0cl  22288  mhpaddcl  22293  evl1gsumd  22496  grpvlinv  22534  matinvgcell  22571  mat0dim0  22603  mdetdiag  22735  mdetuni0  22757  chpdmatlem2  22975  chp0mat  22982  istgp2  24227  cldsubg  24247  tgpconncompeqg  24248  tgpconncomp  24249  snclseqg  24252  tgphaus  24253  tgpt1  24254  qustgphaus  24259  tgptsmscls  24286  nrmmetd  24710  nmfval2  24727  nmval2  24728  nmf2  24729  ngpds3  24744  nmge0  24753  nmeq0  24754  nminv  24757  nmmtri  24758  nmrtri  24760  nm0  24765  tngnm  24787  idnghm  24879  nmcn  24981  clmvz  25249  nmoleub2lem2  25254  nglmle  25440  mdeg0  26206  dchrinv  27401  dchr1re  27403  dchrpt  27407  dchrsum2  27408  dchrhash  27411  rpvmasumlem  27627  rpvmasum2  27652  dchrisum0re  27653  grpidcld  33325  conjga  33456  fxpsubm  33458  fxpsubg  33459  fxpsubrg  33460  isarchi3  33473  archirng  33474  archirngz  33475  archiabllem1b  33478  isarchiofld  33485  rmfsupp2  33523  erler  33551  rlocaddval  33555  rlocmulval  33556  rloc0g  33558  fracfld  33595  qusker  33635  grplsm0l  33678  qus0g  33682  nsgqus0  33685  nsgmgclem  33686  mplvrpmga  33901  mplvrpmmhm  33902  psrmonprod  33908  mplgsum  33909  mplmonprod  33910  esplyind  33931  esplyfvn  33933  fedgmullem1  33985  irredminply  34072  rtelextdg2lem  34082  qqh0  34340  sconnpi1  35697  lfl0f  39811  lkrlss  39837  lshpkrlem1  39852  lkrin  39906  dvhgrp  41849  primrootscoprmpow  42834  aks5lem7  42935  fsuppind  43292  fsuppssind  43295  mhpind  43296  evl1at0  49138