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

Theorem rngidval 15621
Description: The value of the unity element of a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
Hypotheses
Ref Expression
rngidval.g  |-  G  =  (mulGrp `  R )
rngidval.u  |-  .1.  =  ( 1r `  R )
Assertion
Ref Expression
rngidval  |-  .1.  =  ( 0g `  G )

Proof of Theorem rngidval
StepHypRef Expression
1 df-ur 15620 . . . . 5  |-  1r  =  ( 0g  o. mulGrp )
21fveq1i 5688 . . . 4  |-  ( 1r
`  R )  =  ( ( 0g  o. mulGrp ) `
 R )
3 fnmgp 15605 . . . . 5  |- mulGrp  Fn  _V
4 fvco2 5757 . . . . 5  |-  ( (mulGrp 
Fn  _V  /\  R  e. 
_V )  ->  (
( 0g  o. mulGrp ) `  R )  =  ( 0g `  (mulGrp `  R ) ) )
53, 4mpan 652 . . . 4  |-  ( R  e.  _V  ->  (
( 0g  o. mulGrp ) `  R )  =  ( 0g `  (mulGrp `  R ) ) )
62, 5syl5eq 2448 . . 3  |-  ( R  e.  _V  ->  ( 1r `  R )  =  ( 0g `  (mulGrp `  R ) ) )
7 0g0 14664 . . . 4  |-  (/)  =  ( 0g `  (/) )
8 fvprc 5681 . . . 4  |-  ( -.  R  e.  _V  ->  ( 1r `  R )  =  (/) )
9 fvprc 5681 . . . . 5  |-  ( -.  R  e.  _V  ->  (mulGrp `  R )  =  (/) )
109fveq2d 5691 . . . 4  |-  ( -.  R  e.  _V  ->  ( 0g `  (mulGrp `  R ) )  =  ( 0g `  (/) ) )
117, 8, 103eqtr4a 2462 . . 3  |-  ( -.  R  e.  _V  ->  ( 1r `  R )  =  ( 0g `  (mulGrp `  R ) ) )
126, 11pm2.61i 158 . 2  |-  ( 1r
`  R )  =  ( 0g `  (mulGrp `  R ) )
13 rngidval.u . 2  |-  .1.  =  ( 1r `  R )
14 rngidval.g . . 3  |-  G  =  (mulGrp `  R )
1514fveq2i 5690 . 2  |-  ( 0g
`  G )  =  ( 0g `  (mulGrp `  R ) )
1612, 13, 153eqtr4i 2434 1  |-  .1.  =  ( 0g `  G )
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1649    e. wcel 1721   _Vcvv 2916   (/)c0 3588    o. ccom 4841    Fn wfn 5408   ` cfv 5413   0gc0g 13678  mulGrpcmgp 15603   1rcur 15617
This theorem is referenced by:  dfur2  15622  rngidcl  15639  rngidmlem  15641  isrngid  15644  prds1  15675  oppr1  15694  unitsubm  15730  rngidpropd  15755  dfrhm2  15776  isrhm2d  15784  rhm1  15786  subrgsubm  15836  issubrg3  15851  mplcoe3  16484  mplcoe2  16485  mplbas2  16486  ply1scltm  16628  cnfldexp  16689  expmhm  16731  evlslem1  19889  amgmlem  20781  amgm  20782  wilthlem2  20805  wilthlem3  20806  dchrelbas3  20975  dchrzrh1  20981  dchrmulcl  20986  dchrn0  20987  dchrinvcl  20990  dchrfi  20992  dchrabs  20997  sumdchr2  21007  rpvmasum2  21159  iistmd  24253  isdomn3  27391  mon1psubm  27393  deg1mhm  27394
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 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363
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 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-fv 5421  df-ov 6043  df-slot 13428  df-base 13429  df-0g 13682  df-mgp 15604  df-ur 15620
  Copyright terms: Public domain W3C validator