MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  grpidcl Structured version   Visualization version   GIF version

Theorem grpidcl 17649
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
StepHypRef Expression
1 grpmnd 17628 . 2 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2 grpidcl.b . . 3 𝐵 = (Base‘𝐺)
3 grpidcl.o . . 3 0 = (0g𝐺)
42, 3mndidcl 17507 . 2 (𝐺 ∈ Mnd → 0𝐵)
51, 4syl 17 1 (𝐺 ∈ Grp → 0𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1630  wcel 2137  cfv 6047  Basecbs 16057  0gc0g 16300  Mndcmnd 17493  Grpcgrp 17621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-br 4803  df-opab 4863  df-mpt 4880  df-id 5172  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-iota 6010  df-fun 6049  df-fv 6055  df-riota 6772  df-ov 6814  df-0g 16302  df-mgm 17441  df-sgrp 17483  df-mnd 17494  df-grp 17624
This theorem is referenced by:  grpbn0  17650  grprcan  17654  grpid  17656  isgrpid2  17657  grprinv  17668  grpidinv  17674  grpinvid  17675  grpidrcan  17679  grpidlcan  17680  grpidssd  17690  grpinvval2  17697  grpsubid1  17699  imasgrp  17730  mulgcl  17758  mulgz  17767  subg0  17799  subg0cl  17801  issubg4  17812  0subg  17818  nmzsubg  17834  eqgid  17845  qusgrp  17848  qus0  17851  ghmid  17865  ghmpreima  17881  ghmf1  17888  gafo  17927  gaid  17930  gass  17932  gaorber  17939  gastacl  17940  lactghmga  18022  cayleylem2  18031  symgsssg  18085  symgfisg  18086  od1  18174  gexdvds  18197  sylow1lem2  18212  sylow3lem1  18240  lsmdisj2  18293  0frgp  18390  odadd1  18449  torsubg  18455  oddvdssubg  18456  0cyg  18492  prmcyg  18493  telgsums  18588  dprdfadd  18617  dprdz  18627  pgpfac1lem3a  18673  ring0cl  18767  ringlz  18785  ringrz  18786  kerf1hrm  18943  isdrng2  18957  srng0  19060  lmod0vcl  19092  islmhm2  19238  psr0cl  19594  mplsubglem  19634  evl1gsumd  19921  frgpcyg  20122  ip0l  20181  ocvlss  20216  grpvlinv  20401  matinvgcell  20441  mat0dim0  20473  mdetdiag  20605  mdetuni0  20627  chpdmatlem2  20844  chp0mat  20851  istgp2  22094  cldsubg  22113  tgpconncompeqg  22114  tgpconncomp  22115  snclseqg  22118  tgphaus  22119  tgpt1  22120  qustgphaus  22125  tgptsmscls  22152  nrmmetd  22578  nmfval2  22594  nmval2  22595  nmf2  22596  ngpds3  22611  nmge0  22620  nmeq0  22621  nminv  22624  nmmtri  22625  nmrtri  22627  nm0  22632  tngnm  22654  idnghm  22746  nmcn  22846  clmvz  23109  nmoleub2lem2  23114  nglmle  23298  mdeg0  24027  dchrinv  25183  dchr1re  25185  dchrpt  25189  dchrsum2  25190  dchrhash  25193  rpvmasumlem  25373  rpvmasum2  25398  dchrisum0re  25399  ogrpinvOLD  30022  ogrpinv0lt  30030  ogrpinvlt  30031  isarchi3  30048  archirng  30049  archirngz  30050  archiabllem1b  30053  orngsqr  30111  ornglmulle  30112  orngrmulle  30113  ornglmullt  30114  orngrmullt  30115  orngmullt  30116  ofldchr  30121  isarchiofld  30124  qqh0  30335  sconnpi1  31526  lfl0f  34857  lkrlss  34883  lshpkrlem1  34898  lkrin  34952  dvhgrp  36896  rnglz  42392  zrrnghm  42425  ascl0  42673  evl1at0  42687
  Copyright terms: Public domain W3C validator