Theorem grpidcl 17647

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

Syntax hints:   → wi 4   = wceq 1628   ∈ wcel 2135  ‘cfv 6045  Basecbs 16055  0_gc0g 16298  Mndcmnd 17491  Grpcgrp 17619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4585  df-br 4801  df-opab 4861  df-mpt 4878  df-id 5170  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-iota 6008  df-fun 6047  df-fv 6053  df-riota 6770  df-ov 6812  df-0g 16300  df-mgm 17439  df-sgrp 17481  df-mnd 17492  df-grp 17622

This theorem is referenced by:  grpbn0  17648  grprcan  17652  grpid  17654  isgrpid2  17655  grprinv  17666  grpidinv  17672  grpinvid  17673  grpidrcan  17677  grpidlcan  17678  grpidssd  17688  grpinvval2  17695  grpsubid1  17697  imasgrp  17728  mulgcl  17756  mulgz  17765  subg0  17797  subg0cl  17799  issubg4  17810  0subg  17816  nmzsubg  17832  eqgid  17843  qusgrp  17846  qus0  17849  ghmid  17863  ghmpreima  17879  ghmf1  17886  gafo  17925  gaid  17928  gass  17930  gaorber  17937  gastacl  17938  lactghmga  18020  cayleylem2  18029  symgsssg  18083  symgfisg  18084  od1  18172  gexdvds  18195  sylow1lem2  18210  sylow3lem1  18238  lsmdisj2  18291  0frgp  18388  odadd1  18447  torsubg  18453  oddvdssubg  18454  0cyg  18490  prmcyg  18491  telgsums  18586  dprdfadd  18615  dprdz  18625  pgpfac1lem3a  18671  ring0cl  18765  ringlz  18783  ringrz  18784  kerf1hrm  18941  isdrng2  18955  srng0  19058  lmod0vcl  19090  islmhm2  19236  psr0cl  19592  mplsubglem  19632  evl1gsumd  19919  frgpcyg  20120  ip0l  20179  ocvlss  20214  grpvlinv  20399  matinvgcell  20439  mat0dim0  20471  mdetdiag  20603  mdetuni0  20625  chpdmatlem2  20842  chp0mat  20849  istgp2  22092  cldsubg  22111  tgpconncompeqg  22112  tgpconncomp  22113  snclseqg  22116  tgphaus  22117  tgpt1  22118  qustgphaus  22123  tgptsmscls  22150  nrmmetd  22576  nmfval2  22592  nmval2  22593  nmf2  22594  ngpds3  22609  nmge0  22618  nmeq0  22619  nminv  22622  nmmtri  22623  nmrtri  22625  nm0  22630  tngnm  22652  idnghm  22744  nmcn  22844  clmvz  23107  nmoleub2lem2  23112  nglmle  23296  mdeg0  24025  dchrinv  25181  dchr1re  25183  dchrpt  25187  dchrsum2  25188  dchrhash  25191  rpvmasumlem  25371  rpvmasum2  25396  dchrisum0re  25397  ogrpinvOLD  30020  ogrpinv0lt  30028  ogrpinvlt  30029  isarchi3  30046  archirng  30047  archirngz  30048  archiabllem1b  30051  orngsqr  30109  ornglmulle  30110  orngrmulle  30111  ornglmullt  30112  orngrmullt  30113  orngmullt  30114  ofldchr  30119  isarchiofld  30122  qqh0  30333  sconnpi1  31524  lfl0f  34855  lkrlss  34881  lshpkrlem1  34896  lkrin  34950  dvhgrp  36894  rnglz  42390  zrrnghm  42423  ascl0  42671  evl1at0  42685