Theorem grpidcl 18939

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ‘cfv 6492  Basecbs 17177  0_gc0g 17400  Mndcmnd 18700  Grpcgrp 18907

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 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

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 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-riota 7320  df-ov 7366  df-0g 17402  df-mgm 18606  df-sgrp 18685  df-mnd 18701  df-grp 18910

This theorem is referenced by:  grpbn0  18940  grprcan  18947  grpid  18949  isgrpid2  18950  grprinv  18964  grpidinv  18972  grpinvid  18973  grpidrcan  18977  grpidlcan  18978  grpidssd  18990  grpinvval2  18997  grpsubid1  18999  imasgrp  19030  mulgcl  19065  mulgz  19076  subg0  19106  subg0cl  19108  issubg4  19119  nmzsubg  19138  eqgid  19153  eqg0el  19156  qusgrp  19159  qus0  19162  ghmid  19195  ghmpreima  19211  f1ghm0to0  19218  kerf1ghm  19220  ghmqusker  19260  gafo  19269  gaid  19272  gass  19274  gaorber  19281  gastacl  19282  lactghmga  19378  cayleylem2  19386  symgsssg  19440  symgfisg  19441  od1  19532  gexdvds  19557  sylow1lem2  19572  sylow3lem1  19600  lsmdisj2  19655  0frgp  19752  odadd1  19821  torsubg  19827  oddvdssubg  19828  0cyg  19866  prmcyg  19867  telgsums  19966  dprdfadd  19995  dprdz  20005  pgpfac1lem3a  20051  ablsimpgprmd  20090  ogrpinv0lt  20116  ogrpinvlt  20117  rng0cl  20142  rnglz  20144  rngrz  20145  ring0cl  20246  zrrnghm  20515  isdomn4  20695  isdrng2  20722  srng0  20833  orngsqr  20845  ornglmulle  20846  orngrmulle  20847  ornglmullt  20848  orngrmullt  20849  orngmullt  20850  lmod0vcl  20888  islmhm2  21035  rnglidl0  21229  frgpcyg  21555  ofldchr  21558  ip0l  21618  ocvlss  21654  ascl0  21866  psr0cl  21934  mplsubglem  21980  mhp0cl  22141  mhpaddcl  22146  evl1gsumd  22350  grpvlinv  22388  matinvgcell  22425  mat0dim0  22457  mdetdiag  22589  mdetuni0  22611  chpdmatlem2  22829  chp0mat  22836  istgp2  24081  cldsubg  24101  tgpconncompeqg  24102  tgpconncomp  24103  snclseqg  24106  tgphaus  24107  tgpt1  24108  qustgphaus  24113  tgptsmscls  24140  nrmmetd  24564  nmfval2  24581  nmval2  24582  nmf2  24583  ngpds3  24598  nmge0  24607  nmeq0  24608  nminv  24611  nmmtri  24612  nmrtri  24614  nm0  24619  tngnm  24641  idnghm  24733  nmcn  24835  clmvz  25103  nmoleub2lem2  25108  nglmle  25294  mdeg0  26060  dchrinv  27249  dchr1re  27251  dchrpt  27255  dchrsum2  27256  dchrhash  27259  rpvmasumlem  27475  rpvmasum2  27500  dchrisum0re  27501  grpidcld  33126  conjga  33258  fxpsubm  33260  fxpsubg  33261  fxpsubrg  33262  isarchi3  33275  archirng  33276  archirngz  33277  archiabllem1b  33280  isarchiofld  33287  rmfsupp2  33326  erler  33353  rlocaddval  33356  rlocmulval  33357  rloc0g  33359  fracfld  33399  qusker  33439  grplsm0l  33493  qus0g  33497  nsgqus0  33500  nsgmgclem  33501  mplvrpmga  33736  mplvrpmmhm  33737  psrmonprod  33743  mplgsum  33744  mplmonprod  33745  esplyind  33766  esplyfvn  33768  fedgmullem1  33820  irredminply  33907  rtelextdg2lem  33917  qqh0  34175  sconnpi1  35468  lfl0f  39562  lkrlss  39588  lshpkrlem1  39603  lkrin  39657  dvhgrp  41600  primrootscoprmpow  42585  aks5lem7  42686  fsuppind  43041  fsuppssind  43044  mhpind  43045  evl1at0  48883