Theorem ringidval 20092

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 20091	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6859	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 20051	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6958	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 690	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	eqtrid 2776	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 18591	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6850	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6850	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6862	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2790	. . 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 6861	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2762	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109  Vcvv 3447  ∅c0 4296   ∘ ccom 5642   Fn wfn 6506  ‘cfv 6511  0_gc0g 17402  mulGrpcmgp 20049  1_rcur 20090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-1cn 11126  ax-addcl 11128

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187  df-slot 17152  df-ndx 17164  df-base 17180  df-0g 17404  df-mgp 20050  df-ur 20091

This theorem is referenced by:  dfur2  20093  srgidcl  20108  srgidmlem  20110  issrgid  20113  srgpcomp  20127  srg1expzeq1  20134  srgbinom  20140  ringidcl  20174  ringidmlem  20177  isringid  20180  prds1  20232  pwspjmhmmgpd  20237  xpsring1d  20242  oppr1  20259  unitsubm  20295  rngidpropd  20324  dfrhm2  20383  isrhm2d  20396  rhm1  20398  c0rhm  20443  c0rnghm  20444  subrgsubm  20494  issubrg3  20509  isdomn3  20624  cnfldexp  21316  expmhm  21353  nn0srg  21354  rge0srg  21355  fermltlchr  21439  freshmansdream  21484  frobrhm  21485  assamulgscmlem1  21808  mplcoe3  21945  mplcoe5  21947  mplbas2  21949  evlslem1  21989  evlsgsummul  21999  mhppwdeg  22037  psdpw  22057  ply1scltm  22167  ply1idvr1  22181  lply1binomsc  22198  evls1gsummul  22212  evl1gsummul  22247  madetsumid  22348  mat1mhm  22371  scmatmhm  22421  mdet0pr  22479  mdetunilem7  22505  smadiadetlem4  22556  mat2pmatmhm  22620  pm2mpmhm  22707  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  cpmadugsumlemF  22763  efsubm  26460  amgmlem  26900  amgm  26901  wilthlem2  26979  wilthlem3  26980  dchrelbas3  27149  dchrzrh1  27155  dchrmulcl  27160  dchrn0  27161  dchrinvcl  27164  dchrfi  27166  dchrabs  27171  sumdchr2  27181  rpvmasum2  27423  psgnid  33054  cnmsgn0g  33103  altgnsg  33106  urpropd  33183  isunit3  33192  elrgspnlem2  33194  erlbr2d  33215  erler  33216  rloccring  33221  rloc0g  33222  rloc1r  33223  rlocf1  33224  domnprodn0  33226  rrgsubm  33234  znfermltl  33337  unitprodclb  33360  ssdifidlprm  33429  rprmdvdspow  33504  rprmdvdsprod  33505  1arithidomlem1  33506  1arithidom  33508  1arithufdlem3  33517  1arithufdlem4  33518  dfufd2lem  33520  zringfrac  33525  ressply1evls1  33534  evl1deg1  33545  evl1deg2  33546  evl1deg3  33547  assarrginv  33632  evls1fldgencl  33665  iistmd  33892  aks6d1c1p6  42102  evl1gprodd  42105  idomnnzpownz  42120  idomnnzgmulnz  42121  aks6d1c5lem2  42126  deg1gprod  42128  deg1pow  42129  aks5lem2  42175  unitscyglem5  42187  domnexpgn0cl  42511  abvexp  42520  pwsgprod  42532  evlsvvvallem  42549  evlsvvval  42551  evlselv  42575  mhphf  42585  mon1psubm  43188  deg1mhm  43189  amgmwlem  49791  amgmlemALT  49792