Theorem grpidcl 17371

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

Syntax hints:   → wi 4   = wceq 1480   ∈ wcel 1987  ‘cfv 5847  Basecbs 15781  0_gc0g 16021  Mndcmnd 17215  Grpcgrp 17343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-iota 5810  df-fun 5849  df-fv 5855  df-riota 6565  df-ov 6607  df-0g 16023  df-mgm 17163  df-sgrp 17205  df-mnd 17216  df-grp 17346

This theorem is referenced by:  grpbn0  17372  grprcan  17376  grpid  17378  isgrpid2  17379  grprinv  17390  grpidinv  17396  grpinvid  17397  grpidrcan  17401  grpidlcan  17402  grpidssd  17412  grpinvval2  17419  grpsubid1  17421  imasgrp  17452  mulgcl  17480  mulgz  17489  subg0  17521  subg0cl  17523  issubg4  17534  0subg  17540  nmzsubg  17556  eqgid  17567  qusgrp  17570  qus0  17573  ghmid  17587  ghmpreima  17603  ghmf1  17610  gafo  17650  gaid  17653  gass  17655  gaorber  17662  gastacl  17663  lactghmga  17745  cayleylem2  17754  symgsssg  17808  symgfisg  17809  od1  17897  gexdvds  17920  sylow1lem2  17935  sylow3lem1  17963  lsmdisj2  18016  0frgp  18113  odadd1  18172  torsubg  18178  oddvdssubg  18179  0cyg  18215  prmcyg  18216  telgsums  18311  dprdfadd  18340  dprdz  18350  pgpfac1lem3a  18396  ring0cl  18490  ringlz  18508  ringrz  18509  kerf1hrm  18664  isdrng2  18678  srng0  18781  lmod0vcl  18813  islmhm2  18957  psr0cl  19313  mplsubglem  19353  evl1gsumd  19640  frgpcyg  19841  ip0l  19900  ocvlss  19935  grpvlinv  20120  matinvgcell  20160  mat0dim0  20192  mdetdiag  20324  mdetuni0  20346  chpdmatlem2  20563  chp0mat  20570  istgp2  21805  cldsubg  21824  tgpconncompeqg  21825  tgpconncomp  21826  snclseqg  21829  tgphaus  21830  tgpt1  21831  qustgphaus  21836  tgptsmscls  21863  nrmmetd  22289  nmfval2  22305  nmval2  22306  nmf2  22307  ngpds3  22322  nmge0  22331  nmeq0  22332  nminv  22335  nmmtri  22336  nmrtri  22338  nm0  22343  tngnm  22365  idnghm  22457  nmcn  22555  clmvz  22819  nmoleub2lem2  22824  nglmle  23008  mdeg0  23734  dchrinv  24886  dchr1re  24888  dchrpt  24892  dchrsum2  24893  dchrhash  24896  rpvmasumlem  25076  rpvmasum2  25101  dchrisum0re  25102  ogrpinvOLD  29497  ogrpinv0lt  29505  ogrpinvlt  29506  isarchi3  29523  archirng  29524  archirngz  29525  archiabllem1b  29528  orngsqr  29586  ornglmulle  29587  orngrmulle  29588  ornglmullt  29589  orngrmullt  29590  orngmullt  29591  ofldchr  29596  isarchiofld  29599  qqh0  29807  sconnpi1  30926  lfl0f  33833  lkrlss  33859  lshpkrlem1  33874  lkrin  33928  dvhgrp  35873  rnglz  41169  zrrnghm  41202  ascl0  41450  evl1at0  41464