MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  grprid Unicode version

Theorem grprid 14799
Description: The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011.)
Hypotheses
Ref Expression
grpbn0.b  |-  B  =  ( Base `  G
)
grplid.p  |-  .+  =  ( +g  `  G )
grplid.o  |-  .0.  =  ( 0g `  G )
Assertion
Ref Expression
grprid  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  ( X  .+  .0.  )  =  X )

Proof of Theorem grprid
StepHypRef Expression
1 grpmnd 14780 . 2  |-  ( G  e.  Grp  ->  G  e.  Mnd )
2 grpbn0.b . . 3  |-  B  =  ( Base `  G
)
3 grplid.p . . 3  |-  .+  =  ( +g  `  G )
4 grplid.o . . 3  |-  .0.  =  ( 0g `  G )
52, 3, 4mndrid 14680 . 2  |-  ( ( G  e.  Mnd  /\  X  e.  B )  ->  ( X  .+  .0.  )  =  X )
61, 5sylan 458 1  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  ( X  .+  .0.  )  =  X )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721   ` cfv 5421  (class class class)co 6048   Basecbs 13432   +g cplusg 13492   0gc0g 13686   Mndcmnd 14647   Grpcgrp 14648
This theorem is referenced by:  grprcan  14801  grpinvid1  14816  grpinvid2  14817  grpsubid1  14837  grpsubadd  14839  grppncan  14842  mulgdirlem  14877  nmzsubg  14944  0nsg  14948  cayleylem2  15074  cntzsubg  15098  odbezout  15157  lsmdisj2  15277  pj1lid  15296  frgpuplem  15367  abladdsub4  15401  odadd2  15427  gex2abl  15429  rnglz  15663  isabvd  15871  lmod0vrid  15944  islmhm2  16077  mplcoe1  16491  lsmcss  16882  opnsubg  18098  tgpconcompeqg  18102  snclseqg  18106  deg1add  19987  lflmul  29563  cdlemn4  31693  mapdh6cN  32233  hdmap1l6c  32308  hdmapinvlem3  32418  hdmapinvlem4  32419  hdmapglem7b  32426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-reu 2681  df-rmo 2682  df-rab 2683  df-v 2926  df-sbc 3130  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-mpt 4236  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-iota 5385  df-fun 5423  df-fv 5429  df-ov 6051  df-riota 6516  df-0g 13690  df-mnd 14653  df-grp 14775
  Copyright terms: Public domain W3C validator