Theorem ringidval 20155

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

Step	Hyp	Ref	Expression
1		df-ur 20154	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6835	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 20114	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6931	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 691	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	eqtrid 2784	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 18623	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6826	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6826	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6838	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2798	. . 3 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
12	6, 11	pm2.61i 182	. 2 ⊢ (1r‘𝑅) = (0g‘(mulGrp‘𝑅))
13		ringidval.u	. 2 ⊢ 1 = (1r‘𝑅)
14		ringidval.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
15	14	fveq2i 6837	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2770	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1542   ∈ wcel 2114  Vcvv 3430  ∅c0 4274   ∘ ccom 5628   Fn wfn 6487  ‘cfv 6492  0_gc0g 17393  mulGrpcmgp 20112  1_rcur 20153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-1cn 11087  ax-addcl 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-nn 12166  df-slot 17143  df-ndx 17155  df-base 17171  df-0g 17395  df-mgp 20113  df-ur 20154

This theorem is referenced by:  dfur2  20156  srgidcl  20171  srgidmlem  20173  issrgid  20176  srgpcomp  20190  srg1expzeq1  20197  srgbinom  20203  ringidcl  20237  ringidmlem  20240  isringid  20243  prds1  20293  pwspjmhmmgpd  20298  pwsgprod  20300  xpsring1d  20304  oppr1  20321  unitsubm  20357  rngidpropd  20386  dfrhm2  20445  isrhm2d  20457  rhm1  20459  c0rhm  20502  c0rnghm  20503  subrgsubm  20553  issubrg3  20568  isdomn3  20683  cnfldexp  21394  expmhm  21426  nn0srg  21427  rge0srg  21428  fermltlchr  21519  freshmansdream  21564  frobrhm  21565  assamulgscmlem1  21889  mplcoe3  22026  mplcoe5  22028  mplbas2  22030  evlslem1  22070  evlsvvvallem  22079  evlsvvval  22081  evlsgsummul  22085  mhppwdeg  22126  psdpw  22146  ply1scltm  22256  ply1idvr1  22269  lply1binomsc  22286  evls1gsummul  22300  evl1gsummul  22335  madetsumid  22436  mat1mhm  22459  scmatmhm  22509  mdet0pr  22567  mdetunilem7  22593  smadiadetlem4  22644  mat2pmatmhm  22708  pm2mpmhm  22795  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  cpmadugsumlemF  22851  efsubm  26528  amgmlem  26967  amgm  26968  wilthlem2  27046  wilthlem3  27047  dchrelbas3  27215  dchrzrh1  27221  dchrmulcl  27226  dchrn0  27227  dchrinvcl  27230  dchrfi  27232  dchrabs  27237  sumdchr2  27247  rpvmasum2  27489  psgnid  33173  cnmsgn0g  33222  altgnsg  33225  urpropd  33307  isunit3  33317  elrgspnlem2  33319  erlbr2d  33340  erler  33341  rloccring  33346  rloc0g  33347  rloc1r  33348  rlocf1  33349  domnprodn0  33351  domnprodeq0  33352  rrgsubm  33360  znfermltl  33441  unitprodclb  33464  ssdifidlprm  33533  rprmdvdspow  33608  rprmdvdsprod  33609  1arithidomlem1  33610  1arithidom  33612  1arithufdlem3  33621  1arithufdlem4  33622  dfufd2lem  33624  zringfrac  33629  ressply1evls1  33640  evl1deg1  33651  evl1deg2  33652  evl1deg3  33653  deg1prod  33658  evlextv  33701  psrmonprod  33711  vieta  33739  assarrginv  33796  evls1fldgencl  33830  iistmd  34062  aks6d1c1p6  42567  evl1gprodd  42570  idomnnzpownz  42585  idomnnzgmulnz  42586  aks6d1c5lem2  42591  deg1gprod  42593  deg1pow  42594  aks5lem2  42640  unitscyglem5  42652  domnexpgn0cl  42982  abvexp  42991  evlselv  43034  mhphf  43044  mon1psubm  43645  deg1mhm  43646  amgmwlem  50289  amgmlemALT  50290