Theorem ringidval 20256

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 20255	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6872	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 20209	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6968	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 702	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	eqtrid 2812	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 18712	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6863	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6863	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6875	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2826	. . 3 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
12	6, 11	pm2.61i 184	. 2 ⊢ (1r‘𝑅) = (0g‘(mulGrp‘𝑅))
13		ringidval.u	. 2 ⊢ 1 = (1r‘𝑅)
14		ringidval.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
15	14	fveq2i 6874	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2798	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1563   ∈ wcel 2145  Vcvv 3457  ∅c0 4288   ∘ ccom 5656   Fn wfn 6520  ‘cfv 6525  0_gc0g 17482  mulGrpcmgp 20207  1_rcur 20254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-cnex 11144  ax-1cn 11146  ax-addcl 11148

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-om 7851  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-nn 12225  df-slot 17232  df-ndx 17244  df-base 17260  df-0g 17484  df-mgp 20208  df-ur 20255

This theorem is referenced by:  dfur2  20257  srgidcl  20272  srgidmlem  20274  issrgid  20277  srgpcomp  20291  srg1expzeq1  20298  srgbinom  20304  ringidcl  20339  ringidmlem  20342  isringid  20345  prds1  20395  pwspjmhmmgpd  20400  pwsgprod  20402  xpsring1d  20406  oppr1  20423  unitsubm  20459  rngidpropd  20488  dfrhm2  20547  isrhm2d  20560  rhm1  20562  c0rhm  20610  c0rnghm  20611  subrgsubm  20661  issubrg3  20676  isdomn3  20790  ssdifidlprm  21446  prmidlsubm  21447  cnfldexp  21515  expmhm  21546  nn0srg  21547  rge0srg  21548  fermltlchr  21639  freshmansdream  21684  frobrhm  21685  assamulgscmlem1  22009  mplcoe3  22149  mplcoe5  22151  mplbas2  22153  evlslem1  22193  evlsvvvallem  22202  evlsvvval  22204  evlsgsummul  22208  mhppwdeg  22273  psdpw  22293  ply1scltm  22402  ply1idvr1  22415  lply1binomsc  22432  evls1gsummul  22446  evl1gsummul  22481  madetsumid  22579  mat1mhm  22602  scmatmhm  22652  mdet0pr  22710  mdetunilem7  22736  smadiadetlem4  22787  mat2pmatmhm  22851  pm2mpmhm  22938  chfacfscmulgsum  22978  chfacfpmmulgsum  22982  cpmadugsumlemF  22994  efsubm  26674  amgmlem  27112  amgm  27113  wilthlem2  27191  wilthlem3  27192  dchrelbas3  27360  dchrzrh1  27366  dchrmulcl  27371  dchrn0  27372  dchrinvcl  27375  dchrfi  27377  dchrabs  27382  sumdchr2  27392  rpvmasum2  27634  psgnid  33330  cnmsgn0g  33379  altgnsg  33382  urpropd  33463  isunit3  33473  elrgspnlem2  33476  erlbr2d  33497  erler  33498  rloccring  33504  rloc0g  33505  rloc1r  33506  rlocf1  33507  rlocinvunit  33508  rlocisunit  33509  domnprodn0  33511  domnprodeq0  33512  rrgsubm  33517  znfermltl  33596  unitprodclb  33618  rprmdvdspow  33740  rprmdvdsprod  33741  1arithidomlem1  33742  1arithidom  33744  1arithufdlem3  33753  1arithufdlem4  33754  dfufd2lem  33756  zringfrac  33761  ressply1evls1  33772  evl1deg1  33783  evl1deg2  33784  evl1deg3  33785  deg1prod  33790  evlextv  33849  psrmonprod  33859  vieta  33887  assarrginv  33943  evls1fldgencl  33977  iistmd  34209  aks6d1c1p6  42743  evl1gprodd  42746  idomnnzpownz  42761  idomnnzgmulnz  42762  aks6d1c5lem2  42767  deg1gprod  42769  deg1pow  42770  aks5lem2  42816  unitscyglem5  42828  domnexpgn0cl  43153  abvexp  43162  evlselv  43183  mhphf  43191  mon1psubm  43788  deg1mhm  43789  amgmwlem  50431  amgmlemALT  50432