Theorem ringidval 20118

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 20117	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6835	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 20077	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6931	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 690	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	eqtrid 2783	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 18589	. . . 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 2797	. . 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 2769	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2113  Vcvv 3440  ∅c0 4285   ∘ ccom 5628   Fn wfn 6487  ‘cfv 6492  0_gc0g 17359  mulGrpcmgp 20075  1_rcur 20116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-1cn 11084  ax-addcl 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  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 7361  df-om 7809  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-nn 12146  df-slot 17109  df-ndx 17121  df-base 17137  df-0g 17361  df-mgp 20076  df-ur 20117

This theorem is referenced by:  dfur2  20119  srgidcl  20134  srgidmlem  20136  issrgid  20139  srgpcomp  20153  srg1expzeq1  20160  srgbinom  20166  ringidcl  20200  ringidmlem  20203  isringid  20206  prds1  20258  pwspjmhmmgpd  20263  pwsgprod  20265  xpsring1d  20269  oppr1  20286  unitsubm  20322  rngidpropd  20351  dfrhm2  20410  isrhm2d  20422  rhm1  20424  c0rhm  20467  c0rnghm  20468  subrgsubm  20518  issubrg3  20533  isdomn3  20648  cnfldexp  21359  expmhm  21391  nn0srg  21392  rge0srg  21393  fermltlchr  21484  freshmansdream  21529  frobrhm  21530  assamulgscmlem1  21855  mplcoe3  21993  mplcoe5  21995  mplbas2  21997  evlslem1  22037  evlsvvvallem  22046  evlsvvval  22048  evlsgsummul  22052  mhppwdeg  22093  psdpw  22113  ply1scltm  22223  ply1idvr1  22238  lply1binomsc  22255  evls1gsummul  22269  evl1gsummul  22304  madetsumid  22405  mat1mhm  22428  scmatmhm  22478  mdet0pr  22536  mdetunilem7  22562  smadiadetlem4  22613  mat2pmatmhm  22677  pm2mpmhm  22764  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  cpmadugsumlemF  22820  efsubm  26516  amgmlem  26956  amgm  26957  wilthlem2  27035  wilthlem3  27036  dchrelbas3  27205  dchrzrh1  27211  dchrmulcl  27216  dchrn0  27217  dchrinvcl  27220  dchrfi  27222  dchrabs  27227  sumdchr2  27237  rpvmasum2  27479  psgnid  33179  cnmsgn0g  33228  altgnsg  33231  urpropd  33313  isunit3  33323  elrgspnlem2  33325  erlbr2d  33346  erler  33347  rloccring  33352  rloc0g  33353  rloc1r  33354  rlocf1  33355  domnprodn0  33357  domnprodeq0  33358  rrgsubm  33366  znfermltl  33447  unitprodclb  33470  ssdifidlprm  33539  rprmdvdspow  33614  rprmdvdsprod  33615  1arithidomlem1  33616  1arithidom  33618  1arithufdlem3  33627  1arithufdlem4  33628  dfufd2lem  33630  zringfrac  33635  ressply1evls1  33646  evl1deg1  33657  evl1deg2  33658  evl1deg3  33659  deg1prod  33664  evlextv  33707  vieta  33736  assarrginv  33793  evls1fldgencl  33827  iistmd  34059  aks6d1c1p6  42364  evl1gprodd  42367  idomnnzpownz  42382  idomnnzgmulnz  42383  aks6d1c5lem2  42388  deg1gprod  42390  deg1pow  42391  aks5lem2  42437  unitscyglem5  42449  domnexpgn0cl  42774  abvexp  42783  evlselv  42826  mhphf  42836  mon1psubm  43437  deg1mhm  43438  amgmwlem  50043  amgmlemALT  50044