MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ringidval Structured version   Visualization version   GIF version

Theorem ringidval 19173
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
ringidval.g 𝐺 = (mulGrp‘𝑅)
ringidval.u 1 = (1r𝑅)
Assertion
Ref Expression
ringidval 1 = (0g𝐺)

Proof of Theorem ringidval
StepHypRef Expression
1 df-ur 19172 . . . . 5 1r = (0g ∘ mulGrp)
21fveq1i 6668 . . . 4 (1r𝑅) = ((0g ∘ mulGrp)‘𝑅)
3 fnmgp 19161 . . . . 5 mulGrp Fn V
4 fvco2 6755 . . . . 5 ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
53, 4mpan 686 . . . 4 (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
62, 5syl5eq 2873 . . 3 (𝑅 ∈ V → (1r𝑅) = (0g‘(mulGrp‘𝑅)))
7 0g0 17863 . . . 4 ∅ = (0g‘∅)
8 fvprc 6660 . . . 4 𝑅 ∈ V → (1r𝑅) = ∅)
9 fvprc 6660 . . . . 5 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
109fveq2d 6671 . . . 4 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
117, 8, 103eqtr4a 2887 . . 3 𝑅 ∈ V → (1r𝑅) = (0g‘(mulGrp‘𝑅)))
126, 11pm2.61i 183 . 2 (1r𝑅) = (0g‘(mulGrp‘𝑅))
13 ringidval.u . 2 1 = (1r𝑅)
14 ringidval.g . . 3 𝐺 = (mulGrp‘𝑅)
1514fveq2i 6670 . 2 (0g𝐺) = (0g‘(mulGrp‘𝑅))
1612, 13, 153eqtr4i 2859 1 1 = (0g𝐺)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1530  wcel 2107  Vcvv 3500  c0 4295  ccom 5558   Fn wfn 6347  cfv 6352  0gc0g 16703  mulGrpcmgp 19159  1rcur 19171
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6312  df-fun 6354  df-fn 6355  df-fv 6360  df-ov 7151  df-slot 16477  df-base 16479  df-0g 16705  df-mgp 19160  df-ur 19172
This theorem is referenced by:  dfur2  19174  srgidcl  19188  srgidmlem  19190  issrgid  19193  srgpcomp  19202  srg1expzeq1  19209  srgbinom  19215  ringidcl  19238  ringidmlem  19240  isringid  19243  prds1  19284  oppr1  19304  unitsubm  19340  rngidpropd  19365  dfrhm2  19389  isrhm2d  19400  rhm1  19402  subrgsubm  19468  issubrg3  19483  assamulgscmlem1  20047  mplcoe3  20165  mplcoe5  20167  mplbas2  20169  evlslem1  20213  evlsgsummul  20223  ply1scltm  20366  lply1binomsc  20392  evls1gsummul  20405  evl1gsummul  20439  cnfldexp  20494  expmhm  20530  nn0srg  20531  rge0srg  20532  madetsumid  20986  mat1mhm  21009  scmatmhm  21059  mdet0pr  21117  mdetunilem7  21143  smadiadetlem4  21194  mat2pmatmhm  21257  pm2mpmhm  21344  chfacfscmulgsum  21384  chfacfpmmulgsum  21388  cpmadugsumlemF  21400  efsubm  25048  amgmlem  25481  amgm  25482  wilthlem2  25560  wilthlem3  25561  dchrelbas3  25728  dchrzrh1  25734  dchrmulcl  25739  dchrn0  25740  dchrinvcl  25743  dchrfi  25745  dchrabs  25750  sumdchr2  25760  rpvmasum2  26002  psgnid  30653  cnmsgn0g  30702  altgnsg  30705  freshmansdream  30773  iistmd  31031  isdomn3  39669  mon1psubm  39671  deg1mhm  39672  c0rhm  44015  c0rnghm  44016  amgmwlem  44735  amgmlemALT  44736
  Copyright terms: Public domain W3C validator