Theorem grpidcl 19138

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6527  Basecbs 17349  0_gc0g 17572  Mndcmnd 18885  Grpcgrp 19106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-iota 6483  df-fun 6529  df-fv 6535  df-riota 7365  df-ov 7411  df-0g 17574  df-mgm 18778  df-sgrp 18870  df-mnd 18886  df-grp 19109

This theorem is used by:  grpbn0  19139  grprcan  19146  grpid  19148  isgrpid2  19149  grprinv  19163  grpidinv  19171  grpinvid  19172  grpidrcan  19176  grpidlcan  19177  grpidssd  19188  grpinvval2  19195  grpsubid1  19197  imasgrp  19228  mulgcl  19263  mulgz  19274  subg0  19304  subg0cl  19306  issubg4  19318  nmzsubg  19337  eqgid  19354  eqg0el  19360  qusgrp  19363  qus0  19366  ghmid  19398  ghmpreima  19414  f1ghm0to0  19421  kerf1ghm  19423  ghmqusker  19463  gafo  19472  gaid  19475  gass  19477  gaorber  19484  gastacl  19485  lactghmga  19581  cayleylem2  19589  symgsssg  19643  symgfisg  19644  od1  19735  gexdvds  19760  sylow1lem2  19775  sylow3lem1  19803  lsmdisj2  19858  0frgp  19955  odadd1  20024  torsubg  20030  oddvdssubg  20031  0cyg  20069  prmcyg  20070  telgsums  20169  dprdfadd  20198  dprdz  20208  pgpfac1lem3a  20254  ablsimpgprmd  20293  ogrpinv0lt  20319  ogrpinvlt  20320  rng0cl  20347  rnglz  20349  rngrz  20350  ring0cl  20458  zrrnghm  20750  isdomn4  20929  isdrng2  20959  srng0  21073  orngsqr  21085  ornglmulle  21086  orngrmulle  21087  ornglmullt  21088  orngrmullt  21089  orngmullt  21090  lmod0vcl  21128  islmhm2  21275  rnglidl0  21471  frgpcyg  21841  ofldchr  21844  ip0l  21904  ocvlss  21940  ascl0  22154  psr0cl  22222  mplsubglem  22268  mhp0cl  22429  mhpaddcl  22434  evl1gsumd  22637  grpvlinv  22675  matinvgcell  22712  mat0dim0  22744  mdetdiag  22876  mdetuni0  22898  chpdmatlem2  23119  chp0mat  23126  istgp2  24372  cldsubg  24392  tgpconncompeqg  24393  tgpconncomp  24394  snclseqg  24397  tgphaus  24398  tgpt1  24399  qustgphaus  24404  tgptsmscls  24431  nrmmetd  24855  nmfval2  24872  nmval2  24873  nmf2  24874  ngpds3  24889  nmge0  24898  nmeq0  24899  nminv  24902  nmmtri  24903  nmrtri  24905  nm0  24910  tngnm  24932  idnghm  25024  nmcn  25126  clmvz  25394  nmoleub2lem2  25399  nglmle  25585  mdeg0  26350  dchrinv  27552  dchr1re  27554  dchrpt  27558  dchrsum2  27559  dchrhash  27562  rpvmasumlem  27778  rpvmasum2  27803  dchrisum0re  27804  grpidcld  33534  conjga  33665  fxpsubm  33667  fxpsubg  33668  fxpsubrg  33669  isarchi3  33682  archirng  33683  archirngz  33684  archiabllem1b  33687  isarchiofld  33694  rmfsupp2  33732  erler  33760  rlocaddval  33764  rlocmulval  33765  rloc0g  33767  fracfld  33804  qusker  33844  grplsm0l  33888  qus0g  33892  nsgqus0  33895  nsgmgclem  33896  mplvrpmga  34111  mplgsum  34119  mplmonprod  34120  esplyind  34141  esplyfvn  34143  fedgmullem1  34195  irredminply  34282  rtelextdg2lem  34292  qqh0  34550  sconnpi1  35925  lfl0f  40046  lkrlss  40072  lshpkrlem1  40087  lkrin  40141  dvhgrp  42084  primrootscoprmpow  43069  aks5lem7  43170  fsuppind  43540  fsuppssind  43543  mhpind  43544  evl1at0  49425