Theorem ringidval 20439

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 20438	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6909	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 20392	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 7005	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 703	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	eqtrid 2810	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 18873	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6900	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6900	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6912	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2824	. . 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 6911	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2796	1 ⊢ 1 = (0g‘𝐺)

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2147  Vcvv 3454  ∅c0 4281   ∘ ccom 5659   Fn wfn 6553  ‘cfv 6558  0_gc0g 17639  mulGrpcmgp 20390  1_rcur 20437

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7775  ax-cnex 11283  ax-1cn 11285  ax-addcl 11287

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6322  df-ord 6383  df-on 6384  df-lim 6385  df-suc 6386  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-ov 7446  df-om 7902  df-2nd 8026  df-frecs 8327  df-wrecs 8358  df-recs 8407  df-rdg 8446  df-nn 12363  df-slot 17389  df-ndx 17401  df-base 17417  df-0g 17641  df-mgp 20391  df-ur 20438

This theorem is used by:  dfur2  20440  srgidcl  20455  srgidmlem  20457  issrgid  20460  srgpcomp  20474  srg1expzeq1  20481  srgbinom  20487  ringidcl  20524  ringidmlem  20527  isringid  20530  prds1  20582  pwspjmhmmgpd  20587  pwsgprod  20589  xpsring1d  20593  oppr1  20610  unitsubm  20646  rngidpropd  20675  dfrhm2  20734  isrhm2d  20751  rhm1  20754  c0rhm  20816  c0rnghm  20817  subrgsubm  20867  issubrg3  20882  isdomn3  20996  isdrng3lem1  21035  ssdifidlprm  21672  prmidlsubm  21673  cnfldexp  21741  expmhm  21772  nn0srg  21773  rge0srg  21774  fermltlchr  21865  freshmansdream  21910  frobrhm  21911  assamulgscmlem1  22237  mplcoe3  22377  mplcoe5  22379  mplbas2  22381  evlslem1  22421  evlsvvvallem  22430  evlsvvval  22432  evlsgsummul  22436  mhppwdeg  22501  psdpw  22521  ply1scltm  22630  ply1idvr1  22643  lply1binomsc  22659  evls1gsummul  22673  evl1gsummul  22708  madetsumid  22806  mat1mhm  22829  scmatmhm  22879  mdet0pr  22937  mdetunilem7  22963  smadiadetlem4  23014  mat2pmatmhm  23081  pm2mpmhm  23168  chfacfscmulgsum  23208  chfacfpmmulgsum  23212  cpmadugsumlemF  23224  efsubm  26909  amgmlem  27347  amgm  27348  wilthlem2  27426  wilthlem3  27427  dchrelbas3  27595  dchrzrh1  27601  dchrmulcl  27606  dchrn0  27607  dchrinvcl  27610  dchrfi  27612  dchrabs  27617  sumdchr2  27627  rpvmasum2  27869  psgnid  33728  cnmsgn0g  33777  altgnsg  33780  urpropd  33861  isunit3  33871  elrgspnlem2  33874  erlbr2d  33895  erler  33896  rloccring  33902  rloc0g  33903  rloc1r  33904  rlocf1  33905  rlocinvunit  33906  rlocisunit  33907  domnprodn0  33909  domnprodeq0  33910  rrgsubm  33915  znfermltl  33992  unitprodclb  34014  rprmdvdspow  34135  rprmdvdsprod  34136  1arithidomlem1  34137  1arithidom  34139  1arithufdlem3  34148  1arithufdlem4  34149  dfufd2lem  34151  zringfrac  34156  ressply1evls1  34167  evl1deg1  34178  evl1deg2  34179  evl1deg3  34180  deg1prod  34185  evlextv  34244  psrmonprod  34254  vieta  34282  assarrginv  34338  evls1fldgencl  34372  iistmd  34604  aks6d1c1p6  43356  evl1gprodd  43359  idomnnzpownz  43374  idomnnzgmulnz  43375  aks6d1c5lem2  43380  deg1gprod  43382  deg1pow  43383  aks5lem2  43429  unitscyglem5  43441  domnexpgn0cl  43777  abvexp  43789  evlselv  43810  mhphf  43818  mon1psubm  44393  deg1mhm  44394  amgmwlem  51267  amgmlemALT  51268