Theorem ringidval 20143

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 20142	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6877	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 20102	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6976	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 690	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	eqtrid 2782	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 18642	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6868	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6868	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6880	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2796	. . 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 6879	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2768	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2108  Vcvv 3459  ∅c0 4308   ∘ ccom 5658   Fn wfn 6526  ‘cfv 6531  0_gc0g 17453  mulGrpcmgp 20100  1_rcur 20141

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-cnex 11185  ax-1cn 11187  ax-addcl 11189

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7408  df-om 7862  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-nn 12241  df-slot 17201  df-ndx 17213  df-base 17229  df-0g 17455  df-mgp 20101  df-ur 20142

This theorem is referenced by:  dfur2  20144  srgidcl  20159  srgidmlem  20161  issrgid  20164  srgpcomp  20178  srg1expzeq1  20185  srgbinom  20191  ringidcl  20225  ringidmlem  20228  isringid  20231  prds1  20283  pwspjmhmmgpd  20288  xpsring1d  20293  oppr1  20310  unitsubm  20346  rngidpropd  20375  dfrhm2  20434  isrhm2d  20447  rhm1  20449  c0rhm  20494  c0rnghm  20495  subrgsubm  20545  issubrg3  20560  isdomn3  20675  cnfldexp  21367  expmhm  21404  nn0srg  21405  rge0srg  21406  fermltlchr  21490  freshmansdream  21535  frobrhm  21536  assamulgscmlem1  21859  mplcoe3  21996  mplcoe5  21998  mplbas2  22000  evlslem1  22040  evlsgsummul  22050  mhppwdeg  22088  psdpw  22108  ply1scltm  22218  ply1idvr1  22232  lply1binomsc  22249  evls1gsummul  22263  evl1gsummul  22298  madetsumid  22399  mat1mhm  22422  scmatmhm  22472  mdet0pr  22530  mdetunilem7  22556  smadiadetlem4  22607  mat2pmatmhm  22671  pm2mpmhm  22758  chfacfscmulgsum  22798  chfacfpmmulgsum  22802  cpmadugsumlemF  22814  efsubm  26512  amgmlem  26952  amgm  26953  wilthlem2  27031  wilthlem3  27032  dchrelbas3  27201  dchrzrh1  27207  dchrmulcl  27212  dchrn0  27213  dchrinvcl  27216  dchrfi  27218  dchrabs  27223  sumdchr2  27233  rpvmasum2  27475  psgnid  33108  cnmsgn0g  33157  altgnsg  33160  urpropd  33227  isunit3  33236  elrgspnlem2  33238  erlbr2d  33259  erler  33260  rloccring  33265  rloc0g  33266  rloc1r  33267  rlocf1  33268  domnprodn0  33270  rrgsubm  33278  znfermltl  33381  unitprodclb  33404  ssdifidlprm  33473  rprmdvdspow  33548  rprmdvdsprod  33549  1arithidomlem1  33550  1arithidom  33552  1arithufdlem3  33561  1arithufdlem4  33562  dfufd2lem  33564  zringfrac  33569  ressply1evls1  33578  evl1deg1  33589  evl1deg2  33590  evl1deg3  33591  assarrginv  33676  evls1fldgencl  33711  iistmd  33933  aks6d1c1p6  42127  evl1gprodd  42130  idomnnzpownz  42145  idomnnzgmulnz  42146  aks6d1c5lem2  42151  deg1gprod  42153  deg1pow  42154  aks5lem2  42200  unitscyglem5  42212  domnexpgn0cl  42546  abvexp  42555  pwsgprod  42567  evlsvvvallem  42584  evlsvvval  42586  evlselv  42610  mhphf  42620  mon1psubm  43223  deg1mhm  43224  amgmwlem  49666  amgmlemALT  49667