Theorem grpidcl 19005

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ‘cfv 6573  Basecbs 17258  0_gc0g 17499  Mndcmnd 18772  Grpcgrp 18973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fv 6581  df-riota 7404  df-ov 7451  df-0g 17501  df-mgm 18678  df-sgrp 18757  df-mnd 18773  df-grp 18976

This theorem is referenced by:  grpbn0  19006  grprcan  19013  grpid  19015  isgrpid2  19016  grprinv  19030  grpidinv  19038  grpinvid  19039  grpidrcan  19043  grpidlcan  19044  grpidssd  19056  grpinvval2  19063  grpsubid1  19065  imasgrp  19096  mulgcl  19131  mulgz  19142  subg0  19172  subg0cl  19174  issubg4  19185  0subgOLD  19192  nmzsubg  19205  eqgid  19220  eqg0el  19223  qusgrp  19226  qus0  19229  ghmid  19262  ghmpreima  19278  f1ghm0to0  19285  kerf1ghm  19287  ghmqusker  19327  gafo  19336  gaid  19339  gass  19341  gaorber  19348  gastacl  19349  lactghmga  19447  cayleylem2  19455  symgsssg  19509  symgfisg  19510  od1  19601  gexdvds  19626  sylow1lem2  19641  sylow3lem1  19669  lsmdisj2  19724  0frgp  19821  odadd1  19890  torsubg  19896  oddvdssubg  19897  0cyg  19935  prmcyg  19936  telgsums  20035  dprdfadd  20064  dprdz  20074  pgpfac1lem3a  20120  ablsimpgprmd  20159  rng0cl  20190  rnglz  20192  rngrz  20193  ring0cl  20290  zrrnghm  20562  isdomn4  20738  isdrng2  20765  srng0  20877  lmod0vcl  20911  islmhm2  21060  rnglidl0  21262  frgpcyg  21615  ip0l  21677  ocvlss  21713  ascl0  21927  psr0cl  21995  mplsubglem  22042  mhp0cl  22173  mhpaddcl  22178  evl1gsumd  22382  grpvlinv  22423  matinvgcell  22462  mat0dim0  22494  mdetdiag  22626  mdetuni0  22648  chpdmatlem2  22866  chp0mat  22873  istgp2  24120  cldsubg  24140  tgpconncompeqg  24141  tgpconncomp  24142  snclseqg  24145  tgphaus  24146  tgpt1  24147  qustgphaus  24152  tgptsmscls  24179  nrmmetd  24608  nmfval2  24625  nmval2  24626  nmf2  24627  ngpds3  24642  nmge0  24651  nmeq0  24652  nminv  24655  nmmtri  24656  nmrtri  24658  nm0  24663  tngnm  24693  idnghm  24785  nmcn  24885  clmvz  25163  nmoleub2lem2  25168  nglmle  25355  mdeg0  26129  dchrinv  27323  dchr1re  27325  dchrpt  27329  dchrsum2  27330  dchrhash  27333  rpvmasumlem  27549  rpvmasum2  27574  dchrisum0re  27575  ogrpinv0lt  33072  ogrpinvlt  33073  isarchi3  33167  archirng  33168  archirngz  33169  archiabllem1b  33172  rmfsupp2  33218  erler  33237  rlocaddval  33240  rlocmulval  33241  rloc0g  33243  fracfld  33275  orngsqr  33299  ornglmulle  33300  orngrmulle  33301  ornglmullt  33302  orngrmullt  33303  orngmullt  33304  ofldchr  33309  isarchiofld  33312  qusker  33342  grplsm0l  33396  qus0g  33400  nsgqus0  33403  nsgmgclem  33404  fedgmullem1  33642  irredminply  33707  rtelextdg2lem  33717  qqh0  33930  sconnpi1  35207  lfl0f  39025  lkrlss  39051  lshpkrlem1  39066  lkrin  39120  dvhgrp  41064  primrootscoprmpow  42056  aks5lem7  42157  fsuppind  42545  fsuppssind  42548  mhpind  42549  evl1at0  48120