Theorem ringidval 20159

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 20158	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6832	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 20118	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6928	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 697	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	eqtrid 2788	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 18627	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6823	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6823	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6835	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2802	. . 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 6834	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2774	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1548   ∈ wcel 2121  Vcvv 3433  ∅c0 4264   ∘ ccom 5625   Fn wfn 6484  ‘cfv 6489  0_gc0g 17397  mulGrpcmgp 20116  1_rcur 20157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-cnex 11089  ax-1cn 11091  ax-addcl 11093

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-nn 12170  df-slot 17147  df-ndx 17159  df-base 17175  df-0g 17399  df-mgp 20117  df-ur 20158

This theorem is referenced by:  dfur2  20160  srgidcl  20175  srgidmlem  20177  issrgid  20180  srgpcomp  20194  srg1expzeq1  20201  srgbinom  20207  ringidcl  20241  ringidmlem  20244  isringid  20247  prds1  20297  pwspjmhmmgpd  20302  pwsgprod  20304  xpsring1d  20308  oppr1  20325  unitsubm  20361  rngidpropd  20390  dfrhm2  20449  isrhm2d  20462  rhm1  20464  c0rhm  20510  c0rnghm  20511  subrgsubm  20561  issubrg3  20576  isdomn3  20691  cnfldexp  21384  expmhm  21415  nn0srg  21416  rge0srg  21417  fermltlchr  21508  freshmansdream  21553  frobrhm  21554  assamulgscmlem1  21878  mplcoe3  22018  mplcoe5  22020  mplbas2  22022  evlslem1  22062  evlsvvvallem  22071  evlsvvval  22073  evlsgsummul  22077  mhppwdeg  22142  psdpw  22162  ply1scltm  22271  ply1idvr1  22284  lply1binomsc  22301  evls1gsummul  22315  evl1gsummul  22350  madetsumid  22448  mat1mhm  22471  scmatmhm  22521  mdet0pr  22579  mdetunilem7  22605  smadiadetlem4  22656  mat2pmatmhm  22720  pm2mpmhm  22807  chfacfscmulgsum  22847  chfacfpmmulgsum  22851  cpmadugsumlemF  22863  efsubm  26537  amgmlem  26975  amgm  26976  wilthlem2  27054  wilthlem3  27055  dchrelbas3  27223  dchrzrh1  27229  dchrmulcl  27234  dchrn0  27235  dchrinvcl  27238  dchrfi  27240  dchrabs  27245  sumdchr2  27255  rpvmasum2  27497  psgnid  33182  cnmsgn0g  33231  altgnsg  33234  urpropd  33316  isunit3  33326  elrgspnlem2  33328  erlbr2d  33349  erler  33350  rloccring  33355  rloc0g  33356  rloc1r  33357  rlocf1  33358  domnprodn0  33360  domnprodeq0  33361  rrgsubm  33369  znfermltl  33453  unitprodclb  33476  ssdifidlprm  33545  rprmdvdspow  33628  rprmdvdsprod  33629  1arithidomlem1  33630  1arithidom  33632  1arithufdlem3  33641  1arithufdlem4  33642  dfufd2lem  33644  zringfrac  33649  ressply1evls1  33660  evl1deg1  33671  evl1deg2  33672  evl1deg3  33673  deg1prod  33678  evlextv  33738  psrmonprod  33748  vieta  33776  assarrginv  33832  evls1fldgencl  33866  iistmd  34098  aks6d1c1p6  42614  evl1gprodd  42617  idomnnzpownz  42632  idomnnzgmulnz  42633  aks6d1c5lem2  42638  deg1gprod  42640  deg1pow  42641  aks5lem2  42687  unitscyglem5  42699  domnexpgn0cl  43024  abvexp  43033  evlselv  43054  mhphf  43062  mon1psubm  43659  deg1mhm  43660  amgmwlem  50306  amgmlemALT  50307