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

Theorem grprid 15671
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 15652 . 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 15544 . 2  |-  ( ( G  e.  Mnd  /\  X  e.  B )  ->  ( X  .+  .0.  )  =  X )
61, 5sylan 471 1  |-  ( ( G  e.  Grp  /\  X  e.  B )  ->  ( X  .+  .0.  )  =  X )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370    e. wcel 1758   ` cfv 5516  (class class class)co 6190   Basecbs 14276   +g cplusg 14340   0gc0g 14480   Mndcmnd 15511   Grpcgrp 15512
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-iota 5479  df-fun 5518  df-fv 5524  df-riota 6151  df-ov 6193  df-0g 14482  df-mnd 15517  df-grp 15647
This theorem is referenced by:  grprcan  15673  grpinvid1  15688  grpinvid2  15689  grpidrcan  15693  grpsubid1  15713  grpsubadd  15715  grppncan  15718  mulgdirlem  15753  nmzsubg  15824  0nsg  15828  cntzsubg  15956  cayleylem2  16020  odbezout  16163  lsmdisj2  16283  pj1lid  16302  frgpuplem  16373  abladdsub4  16407  odadd2  16435  gex2abl  16437  rnglz  16787  isabvd  17011  lmod0vrid  17085  islmhm2  17225  mplcoe1  17651  lsmcss  18226  mdetero  18532  mdetunilem6  18539  opnsubg  19794  tgpconcompeqg  19798  snclseqg  19802  deg1add  21691  ogrpaddltbi  26316  ogrpinvlt  26321  archiabllem2a  26345  archiabllem2c  26346  lflmul  33019  cdlemn4  35149  mapdh6cN  35689  hdmap1l6c  35764  hdmapinvlem3  35874  hdmapinvlem4  35875  hdmapglem7b  35882
  Copyright terms: Public domain W3C validator