Theorem grpidcl 17766

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

Syntax hints:   → wi 4   = wceq 1653   ∈ wcel 2157  ‘cfv 6101  Basecbs 16184  0_gc0g 16415  Mndcmnd 17609  Grpcgrp 17738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5097

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ne 2972  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3387  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-opab 4906  df-mpt 4923  df-id 5220  df-xp 5318  df-rel 5319  df-cnv 5320  df-co 5321  df-dm 5322  df-iota 6064  df-fun 6103  df-fv 6109  df-riota 6839  df-ov 6881  df-0g 16417  df-mgm 17557  df-sgrp 17599  df-mnd 17610  df-grp 17741

This theorem is referenced by:  grpbn0  17767  grprcan  17771  grpid  17773  isgrpid2  17774  grprinv  17785  grpidinv  17791  grpinvid  17792  grpidrcan  17796  grpidlcan  17797  grpidssd  17807  grpinvval2  17814  grpsubid1  17816  imasgrp  17847  mulgcl  17874  mulgz  17883  subg0  17913  subg0cl  17915  issubg4  17926  0subg  17932  nmzsubg  17948  eqgid  17959  qusgrp  17962  qus0  17965  ghmid  17979  ghmpreima  17995  ghmf1  18002  gafo  18041  gaid  18044  gass  18046  gaorber  18053  gastacl  18054  lactghmga  18136  cayleylem2  18145  symgsssg  18199  symgfisg  18200  od1  18289  gexdvds  18312  sylow1lem2  18327  sylow3lem1  18355  lsmdisj2  18408  0frgp  18507  odadd1  18566  torsubg  18572  oddvdssubg  18573  0cyg  18609  prmcyg  18610  telgsums  18706  dprdfadd  18735  dprdz  18745  pgpfac1lem3a  18791  ring0cl  18885  ringlz  18903  ringrz  18904  kerf1hrm  19061  isdrng2  19075  srng0  19178  lmod0vcl  19210  islmhm2  19359  psr0cl  19717  mplsubglem  19757  evl1gsumd  20043  frgpcyg  20243  ip0l  20305  ocvlss  20341  grpvlinv  20526  matinvgcell  20566  mat0dim0  20599  mdetdiag  20731  mdetuni0  20753  chpdmatlem2  20972  chp0mat  20979  istgp2  22223  cldsubg  22242  tgpconncompeqg  22243  tgpconncomp  22244  snclseqg  22247  tgphaus  22248  tgpt1  22249  qustgphaus  22254  tgptsmscls  22281  nrmmetd  22707  nmfval2  22723  nmval2  22724  nmf2  22725  ngpds3  22740  nmge0  22749  nmeq0  22750  nminv  22753  nmmtri  22754  nmrtri  22756  nm0  22761  tngnm  22783  idnghm  22875  nmcn  22975  clmvz  23238  nmoleub2lem2  23243  nglmle  23428  mdeg0  24171  dchrinv  25338  dchr1re  25340  dchrpt  25344  dchrsum2  25345  dchrhash  25348  rpvmasumlem  25528  rpvmasum2  25553  dchrisum0re  25554  ogrpinvOLD  30231  ogrpinv0lt  30239  ogrpinvlt  30240  isarchi3  30257  archirng  30258  archirngz  30259  archiabllem1b  30262  orngsqr  30320  ornglmulle  30321  orngrmulle  30322  ornglmullt  30323  orngrmullt  30324  orngmullt  30325  ofldchr  30330  isarchiofld  30333  qqh0  30544  sconnpi1  31738  lfl0f  35090  lkrlss  35116  lshpkrlem1  35131  lkrin  35185  dvhgrp  37128  rnglz  42683  zrrnghm  42716  ascl0  42964  evl1at0  42978