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

Theorem rngidval 16938
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 16937 . . . . 5  |-  1r  =  ( 0g  o. mulGrp )
21fveq1i 5858 . . . 4  |-  ( 1r
`  R )  =  ( ( 0g  o. mulGrp ) `
 R )
3 fnmgp 16926 . . . . 5  |- mulGrp  Fn  _V
4 fvco2 5933 . . . . 5  |-  ( (mulGrp 
Fn  _V  /\  R  e. 
_V )  ->  (
( 0g  o. mulGrp ) `  R )  =  ( 0g `  (mulGrp `  R ) ) )
53, 4mpan 670 . . . 4  |-  ( R  e.  _V  ->  (
( 0g  o. mulGrp ) `  R )  =  ( 0g `  (mulGrp `  R ) ) )
62, 5syl5eq 2513 . . 3  |-  ( R  e.  _V  ->  ( 1r `  R )  =  ( 0g `  (mulGrp `  R ) ) )
7 0g0 15740 . . . 4  |-  (/)  =  ( 0g `  (/) )
8 fvprc 5851 . . . 4  |-  ( -.  R  e.  _V  ->  ( 1r `  R )  =  (/) )
9 fvprc 5851 . . . . 5  |-  ( -.  R  e.  _V  ->  (mulGrp `  R )  =  (/) )
109fveq2d 5861 . . . 4  |-  ( -.  R  e.  _V  ->  ( 0g `  (mulGrp `  R ) )  =  ( 0g `  (/) ) )
117, 8, 103eqtr4a 2527 . . 3  |-  ( -.  R  e.  _V  ->  ( 1r `  R )  =  ( 0g `  (mulGrp `  R ) ) )
126, 11pm2.61i 164 . 2  |-  ( 1r
`  R )  =  ( 0g `  (mulGrp `  R ) )
13 rngidval.u . 2  |-  .1.  =  ( 1r `  R )
14 rngidval.g . . 3  |-  G  =  (mulGrp `  R )
1514fveq2i 5860 . 2  |-  ( 0g
`  G )  =  ( 0g `  (mulGrp `  R ) )
1612, 13, 153eqtr4i 2499 1  |-  .1.  =  ( 0g `  G )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1374    e. wcel 1762   _Vcvv 3106   (/)c0 3778    o. ccom 4996    Fn wfn 5574   ` cfv 5579   0gc0g 14684  mulGrpcmgp 16924   1rcur 16936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-fv 5587  df-ov 6278  df-slot 14483  df-base 14484  df-0g 14686  df-mgp 16925  df-ur 16937
This theorem is referenced by:  dfur2  16939  srgidcl  16952  srgidmlem  16954  issrgid  16957  srgpcomp  16964  srg1expzeq1  16971  srgbinom  16977  rngidcl  16999  rngidmlem  17001  isrngid  17004  prds1  17040  oppr1  17060  unitsubm  17096  rngidpropd  17121  dfrhm2  17143  isrhm2d  17154  rhm1  17156  subrgsubm  17218  issubrg3  17233  assamulgscmlem1  17761  mplcoe3  17892  mplcoe3OLD  17893  mplcoe5  17895  mplcoe2OLD  17897  mplbas2  17898  mplbas2OLD  17899  evlslem1  17948  ply1scltm  18086  lply1binomsc  18113  evls1gsummul  18126  evl1gsummul  18160  cnfldexp  18215  expmhm  18246  nn0srg  18247  rge0srg  18248  madetsumid  18723  mat1mhm  18746  scmatmhm  18796  mdet0pr  18854  mdetunilem7  18880  smadiadetlem4  18931  mat2pmatmhm  18994  pm2mpmhm  19081  chfacfscmulgsum  19121  chfacfpmmulgsum  19125  cpmadugsumlemF  19137  amgmlem  23040  amgm  23041  wilthlem2  23064  wilthlem3  23065  dchrelbas3  23234  dchrzrh1  23240  dchrmulcl  23245  dchrn0  23246  dchrinvcl  23249  dchrfi  23251  dchrabs  23256  sumdchr2  23266  rpvmasum2  23418  iistmd  27506  isdomn3  30758  mon1psubm  30760  deg1mhm  30761
  Copyright terms: Public domain W3C validator