Theorem grpidcl 18211

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  ‘cfv 6340  Basecbs 16554  0_gc0g 16784  Mndcmnd 17990  Grpcgrp 18182

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pr 5302

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-opab 5099  df-mpt 5117  df-id 5434  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-iota 6299  df-fun 6342  df-fv 6348  df-riota 7114  df-ov 7159  df-0g 16786  df-mgm 17931  df-sgrp 17980  df-mnd 17991  df-grp 18185

This theorem is referenced by:  grpbn0  18212  grprcan  18217  grpid  18219  isgrpid2  18220  grprinv  18233  grpidinv  18239  grpinvid  18240  grpidrcan  18244  grpidlcan  18245  grpidssd  18255  grpinvval2  18262  grpsubid1  18264  imasgrp  18295  mulgcl  18325  mulgz  18335  subg0  18365  subg0cl  18367  issubg4  18378  0subg  18384  nmzsubg  18397  eqgid  18412  qusgrp  18415  qus0  18418  ghmid  18444  ghmpreima  18460  ghmf1  18467  gafo  18506  gaid  18509  gass  18511  gaorber  18518  gastacl  18519  lactghmga  18613  cayleylem2  18621  symgsssg  18675  symgfisg  18676  od1  18766  gexdvds  18789  sylow1lem2  18804  sylow3lem1  18832  lsmdisj2  18888  0frgp  18985  odadd1  19049  torsubg  19055  oddvdssubg  19056  0cyg  19094  prmcyg  19095  telgsums  19194  dprdfadd  19223  dprdz  19233  pgpfac1lem3a  19279  ablsimpgprmd  19318  ring0cl  19403  ringlz  19421  ringrz  19422  f1ghm0to0  19576  kerf1ghm  19579  isdrng2  19593  srng0  19712  lmod0vcl  19744  islmhm2  19891  frgpcyg  20354  ip0l  20414  ocvlss  20450  ascl0  20659  psr0cl  20735  mplsubglem  20777  mhp0cl  20902  mhpaddcl  20907  evl1gsumd  21089  grpvlinv  21110  matinvgcell  21148  mat0dim0  21180  mdetdiag  21312  mdetuni0  21334  chpdmatlem2  21552  chp0mat  21559  istgp2  22804  cldsubg  22824  tgpconncompeqg  22825  tgpconncomp  22826  snclseqg  22829  tgphaus  22830  tgpt1  22831  qustgphaus  22836  tgptsmscls  22863  nrmmetd  23289  nmfval2  23306  nmval2  23307  nmf2  23308  ngpds3  23323  nmge0  23332  nmeq0  23333  nminv  23336  nmmtri  23337  nmrtri  23339  nm0  23344  tngnm  23366  idnghm  23458  nmcn  23558  clmvz  23825  nmoleub2lem2  23830  nglmle  24015  mdeg0  24783  dchrinv  25957  dchr1re  25959  dchrpt  25963  dchrsum2  25964  dchrhash  25967  rpvmasumlem  26183  rpvmasum2  26208  dchrisum0re  26209  ogrpinv0lt  30886  ogrpinvlt  30887  isarchi3  30979  archirng  30980  archirngz  30981  archiabllem1b  30984  rmfsupp2  31030  orngsqr  31041  ornglmulle  31042  orngrmulle  31043  ornglmullt  31044  orngrmullt  31045  orngmullt  31046  ofldchr  31051  isarchiofld  31054  qusker  31082  eqg0el  31090  grplsm0l  31124  nsgqus0  31128  nsgmgclem  31129  fedgmullem1  31243  qqh0  31465  sconnpi1  32729  lfl0f  36679  lkrlss  36705  lshpkrlem1  36720  lkrin  36774  dvhgrp  38717  fsuppind  39819  fsuppssind  39822  mhpind  39823  rnglz  44924  zrrnghm  44957  evl1at0  45214