Theorem grpidcl 18933

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ‘cfv 6486  Basecbs 17171  0_gc0g 17394  Mndcmnd 18694  Grpcgrp 18901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5219  ax-nul 5229  ax-pr 5363

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4263  df-if 4456  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4840  df-br 5074  df-opab 5136  df-mpt 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6442  df-fun 6488  df-fv 6494  df-riota 7314  df-ov 7360  df-0g 17396  df-mgm 18600  df-sgrp 18679  df-mnd 18695  df-grp 18904

This theorem is referenced by:  grpbn0  18934  grprcan  18941  grpid  18943  isgrpid2  18944  grprinv  18958  grpidinv  18966  grpinvid  18967  grpidrcan  18971  grpidlcan  18972  grpidssd  18984  grpinvval2  18991  grpsubid1  18993  imasgrp  19024  mulgcl  19059  mulgz  19070  subg0  19100  subg0cl  19102  issubg4  19113  nmzsubg  19132  eqgid  19147  eqg0el  19150  qusgrp  19153  qus0  19156  ghmid  19189  ghmpreima  19205  f1ghm0to0  19212  kerf1ghm  19214  ghmqusker  19254  gafo  19263  gaid  19266  gass  19268  gaorber  19275  gastacl  19276  lactghmga  19372  cayleylem2  19380  symgsssg  19434  symgfisg  19435  od1  19526  gexdvds  19551  sylow1lem2  19566  sylow3lem1  19594  lsmdisj2  19649  0frgp  19746  odadd1  19815  torsubg  19821  oddvdssubg  19822  0cyg  19860  prmcyg  19861  telgsums  19960  dprdfadd  19989  dprdz  19999  pgpfac1lem3a  20045  ablsimpgprmd  20084  ogrpinv0lt  20110  ogrpinvlt  20111  rng0cl  20136  rnglz  20138  rngrz  20139  ring0cl  20240  zrrnghm  20509  isdomn4  20689  isdrng2  20716  srng0  20827  orngsqr  20839  ornglmulle  20840  orngrmulle  20841  ornglmullt  20842  orngrmullt  20843  orngmullt  20844  lmod0vcl  20882  islmhm2  21029  rnglidl0  21223  frgpcyg  21549  ofldchr  21552  ip0l  21612  ocvlss  21648  ascl0  21860  psr0cl  21928  mplsubglem  21974  mhp0cl  22135  mhpaddcl  22140  evl1gsumd  22344  grpvlinv  22382  matinvgcell  22419  mat0dim0  22451  mdetdiag  22583  mdetuni0  22605  chpdmatlem2  22823  chp0mat  22830  istgp2  24075  cldsubg  24095  tgpconncompeqg  24096  tgpconncomp  24097  snclseqg  24100  tgphaus  24101  tgpt1  24102  qustgphaus  24107  tgptsmscls  24134  nrmmetd  24558  nmfval2  24575  nmval2  24576  nmf2  24577  ngpds3  24592  nmge0  24601  nmeq0  24602  nminv  24605  nmmtri  24606  nmrtri  24608  nm0  24613  tngnm  24635  idnghm  24727  nmcn  24829  clmvz  25097  nmoleub2lem2  25102  nglmle  25288  mdeg0  26054  dchrinv  27243  dchr1re  27245  dchrpt  27249  dchrsum2  27250  dchrhash  27253  rpvmasumlem  27469  rpvmasum2  27494  dchrisum0re  27495  grpidcld  33120  conjga  33252  fxpsubm  33254  fxpsubg  33255  fxpsubrg  33256  isarchi3  33269  archirng  33270  archirngz  33271  archiabllem1b  33274  isarchiofld  33281  rmfsupp2  33320  erler  33347  rlocaddval  33350  rlocmulval  33351  rloc0g  33353  fracfld  33393  qusker  33433  grplsm0l  33487  qus0g  33491  nsgqus0  33494  nsgmgclem  33495  mplvrpmga  33738  mplvrpmmhm  33739  psrmonprod  33745  mplgsum  33746  mplmonprod  33747  esplyind  33768  esplyfvn  33770  fedgmullem1  33822  irredminply  33909  rtelextdg2lem  33919  qqh0  34177  sconnpi1  35476  lfl0f  39570  lkrlss  39596  lshpkrlem1  39611  lkrin  39665  dvhgrp  41608  primrootscoprmpow  42593  aks5lem7  42694  fsuppind  43049  fsuppssind  43052  mhpind  43053  evl1at0  48890