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

Theorem rngidval 16591
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 16590 . . . . 5  |-  1r  =  ( 0g  o. mulGrp )
21fveq1i 5685 . . . 4  |-  ( 1r
`  R )  =  ( ( 0g  o. mulGrp ) `
 R )
3 fnmgp 16579 . . . . 5  |- mulGrp  Fn  _V
4 fvco2 5759 . . . . 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 2481 . . 3  |-  ( R  e.  _V  ->  ( 1r `  R )  =  ( 0g `  (mulGrp `  R ) ) )
7 0g0 15426 . . . 4  |-  (/)  =  ( 0g `  (/) )
8 fvprc 5678 . . . 4  |-  ( -.  R  e.  _V  ->  ( 1r `  R )  =  (/) )
9 fvprc 5678 . . . . 5  |-  ( -.  R  e.  _V  ->  (mulGrp `  R )  =  (/) )
109fveq2d 5688 . . . 4  |-  ( -.  R  e.  _V  ->  ( 0g `  (mulGrp `  R ) )  =  ( 0g `  (/) ) )
117, 8, 103eqtr4a 2495 . . 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 5687 . 2  |-  ( 0g
`  G )  =  ( 0g `  (mulGrp `  R ) )
1612, 13, 153eqtr4i 2467 1  |-  .1.  =  ( 0g `  G )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1369    e. wcel 1756   _Vcvv 2966   (/)c0 3630    o. ccom 4836    Fn wfn 5406   ` cfv 5411   0gc0g 14370  mulGrpcmgp 16577   1rcur 16589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-opab 4344  df-mpt 4345  df-id 4628  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-fv 5419  df-ov 6089  df-slot 14170  df-base 14171  df-0g 14372  df-mgp 16578  df-ur 16590
This theorem is referenced by:  dfur2  16592  srgidcl  16605  srgidmlem  16607  issrgid  16610  srgpcomp  16617  srgbinom  16629  rngidcl  16651  rngidmlem  16653  isrngid  16656  prds1  16692  oppr1  16712  unitsubm  16748  rngidpropd  16773  dfrhm2  16794  isrhm2d  16802  rhm1  16804  subrgsubm  16854  issubrg3  16869  mplcoe3  17519  mplcoe3OLD  17520  mplcoe2  17521  mplcoe2OLD  17522  mplbas2  17523  mplbas2OLD  17524  evlslem1  17573  ply1scltm  17705  evls1gsummul  17729  evl1gsummul  17763  cnfldexp  17818  expmhm  17849  nn0srg  17850  rge0srg  17851  madetsumid  18315  mdet0pr  18372  mdet1  18377  mdetunilem7  18393  smadiadetlem4  18444  amgmlem  22352  amgm  22353  wilthlem2  22376  wilthlem3  22377  dchrelbas3  22546  dchrzrh1  22552  dchrmulcl  22557  dchrn0  22558  dchrinvcl  22561  dchrfi  22563  dchrabs  22568  sumdchr2  22578  rpvmasum2  22730  iistmd  26280  isdomn3  29515  mon1psubm  29517  deg1mhm  29518  assamulgscmlem1  30739  lply1binomsc  30755
  Copyright terms: Public domain W3C validator