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

Theorem grplid 18740
Description: The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.)
Hypotheses
Ref Expression
grpbn0.b 𝐵 = (Base‘𝐺)
grplid.p + = (+g𝐺)
grplid.o 0 = (0g𝐺)
Assertion
Ref Expression
grplid ((𝐺 ∈ Grp ∧ 𝑋𝐵) → ( 0 + 𝑋) = 𝑋)

Proof of Theorem grplid
StepHypRef Expression
1 grpmnd 18715 . 2 (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
2 grpbn0.b . . 3 𝐵 = (Base‘𝐺)
3 grplid.p . . 3 + = (+g𝐺)
4 grplid.o . . 3 0 = (0g𝐺)
52, 3, 4mndlid 18536 . 2 ((𝐺 ∈ Mnd ∧ 𝑋𝐵) → ( 0 + 𝑋) = 𝑋)
61, 5sylan 580 1 ((𝐺 ∈ Grp ∧ 𝑋𝐵) → ( 0 + 𝑋) = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  cfv 6493  (class class class)co 7351  Basecbs 17043  +gcplusg 17093  0gc0g 17281  Mndcmnd 18516  Grpcgrp 18708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pr 5382
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-mpt 5187  df-id 5529  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6445  df-fun 6495  df-fv 6501  df-riota 7307  df-ov 7354  df-0g 17283  df-mgm 18457  df-sgrp 18506  df-mnd 18517  df-grp 18711
This theorem is referenced by:  grprcan  18744  grpid  18746  isgrpid2  18747  grprinv  18760  grpinvid1  18761  grpinvid2  18762  grpidinv2  18765  grpinvid  18767  grplcan  18768  grpasscan1  18769  grpidlcan  18772  grplmulf1o  18780  grpidssd  18782  grpinvadd  18784  grpinvval2  18789  grplactcnv  18809  imasgrp  18822  mulgaddcom  18859  mulgdirlem  18866  subg0  18893  issubg2  18902  issubg4  18906  0subgOLD  18913  isnsg3  18921  nmzsubg  18926  ssnmz  18927  eqger  18939  eqgid  18941  qusgrp  18944  qus0  18947  ghmid  18973  conjghm  18998  conjnmz  19001  subgga  19039  cntzsubg  19076  sylow1lem2  19340  sylow2blem2  19362  sylow2blem3  19363  sylow3lem1  19368  lsmmod  19416  lsmdisj2  19423  pj1rid  19443  abladdsub4  19551  ablpncan2  19553  ablpnpcan  19557  ablnncan  19558  odadd1  19585  odadd2  19586  oddvdssubg  19592  dprdfadd  19758  pgpfac1lem3a  19814  ringlz  19964  ringrz  19965  isabvd  20232  lmod0vlid  20305  lmod0vs  20308  evpmodpmf1o  20953  ocvlss  21029  lsmcss  21049  psr0lid  21316  mplsubglem  21357  mplcoe1  21390  mhpaddcl  21493  mdetunilem6  21918  mdetunilem9  21921  ghmcnp  23418  tgpt0  23422  qustgpopn  23423  mdegaddle  25391  ply1rem  25480  gsumsubg  31714  ogrpinv0le  31749  ogrpaddltrbid  31754  ogrpinv0lt  31756  ogrpinvlt  31757  cyc3genpmlem  31826  isarchi3  31849  archirngz  31851  archiabllem1b  31854  freshmansdream  31893  orngsqr  31925  ornglmulle  31926  orngrmulle  31927  ofldchr  31935  qusker  31967  grplsm0l  32010  quslsm  32012  mxidlprm  32059  dimkerim  32142  matunitlindflem1  36012  lfl0f  37469  lfladd0l  37474  lkrlss  37495  lkrin  37564  dvhgrp  39508  baerlem3lem1  40108  mapdh6bN  40138  hdmap1l6b  40212  hdmapinvlem3  40321  hdmapinvlem4  40322  hdmapglem7b  40329  sn-grplidd  40625  fsuppind  40674  fsuppssind  40677  rnglz  46083
  Copyright terms: Public domain W3C validator