Theorem ringidval 20162

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 20161	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6835	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 20121	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6931	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 696	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	eqtrid 2787	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 18630	. . . 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 2801	. . 3 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
12	6, 11	pm2.61i 183	. 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 2773	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1547   ∈ wcel 2119  Vcvv 3432  ∅c0 4268   ∘ ccom 5629   Fn wfn 6487  ‘cfv 6492  0_gc0g 17400  mulGrpcmgp 20119  1_rcur 20160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-cnex 11092  ax-1cn 11094  ax-addcl 11096

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  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 7366  df-om 7814  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-nn 12173  df-slot 17150  df-ndx 17162  df-base 17178  df-0g 17402  df-mgp 20120  df-ur 20161

This theorem is referenced by:  dfur2  20163  srgidcl  20178  srgidmlem  20180  issrgid  20183  srgpcomp  20197  srg1expzeq1  20204  srgbinom  20210  ringidcl  20244  ringidmlem  20247  isringid  20250  prds1  20300  pwspjmhmmgpd  20305  pwsgprod  20307  xpsring1d  20311  oppr1  20328  unitsubm  20364  rngidpropd  20393  dfrhm2  20452  isrhm2d  20465  rhm1  20467  c0rhm  20513  c0rnghm  20514  subrgsubm  20564  issubrg3  20579  isdomn3  20694  cnfldexp  21387  expmhm  21418  nn0srg  21419  rge0srg  21420  fermltlchr  21511  freshmansdream  21556  frobrhm  21557  assamulgscmlem1  21881  mplcoe3  22021  mplcoe5  22023  mplbas2  22025  evlslem1  22065  evlsvvvallem  22074  evlsvvval  22076  evlsgsummul  22080  mhppwdeg  22145  psdpw  22165  ply1scltm  22274  ply1idvr1  22287  lply1binomsc  22304  evls1gsummul  22318  evl1gsummul  22353  madetsumid  22451  mat1mhm  22474  scmatmhm  22524  mdet0pr  22582  mdetunilem7  22608  smadiadetlem4  22659  mat2pmatmhm  22723  pm2mpmhm  22810  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  cpmadugsumlemF  22866  efsubm  26540  amgmlem  26978  amgm  26979  wilthlem2  27057  wilthlem3  27058  dchrelbas3  27226  dchrzrh1  27232  dchrmulcl  27237  dchrn0  27238  dchrinvcl  27241  dchrfi  27243  dchrabs  27248  sumdchr2  27258  rpvmasum2  27500  psgnid  33185  cnmsgn0g  33234  altgnsg  33237  urpropd  33319  isunit3  33329  elrgspnlem2  33331  erlbr2d  33352  erler  33353  rloccring  33358  rloc0g  33359  rloc1r  33360  rlocf1  33361  domnprodn0  33363  domnprodeq0  33364  rrgsubm  33372  znfermltl  33456  unitprodclb  33479  ssdifidlprm  33548  rprmdvdspow  33623  rprmdvdsprod  33624  1arithidomlem1  33625  1arithidom  33627  1arithufdlem3  33636  1arithufdlem4  33637  dfufd2lem  33639  zringfrac  33644  ressply1evls1  33655  evl1deg1  33666  evl1deg2  33667  evl1deg3  33668  deg1prod  33673  evlextv  33733  psrmonprod  33743  vieta  33771  assarrginv  33827  evls1fldgencl  33861  iistmd  34093  aks6d1c1p6  42606  evl1gprodd  42609  idomnnzpownz  42624  idomnnzgmulnz  42625  aks6d1c5lem2  42630  deg1gprod  42632  deg1pow  42633  aks5lem2  42679  unitscyglem5  42691  domnexpgn0cl  43016  abvexp  43025  evlselv  43046  mhphf  43054  mon1psubm  43651  deg1mhm  43652  amgmwlem  50299  amgmlemALT  50300