Theorem ringidval 20164

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 20163	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6841	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 20123	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6937	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 691	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	eqtrid 2783	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 18632	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6832	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6832	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6844	. . . 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 6843	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2769	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1542   ∈ wcel 2114  Vcvv 3429  ∅c0 4273   ∘ ccom 5635   Fn wfn 6493  ‘cfv 6498  0_gc0g 17402  mulGrpcmgp 20121  1_rcur 20162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  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 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-nn 12175  df-slot 17152  df-ndx 17164  df-base 17180  df-0g 17404  df-mgp 20122  df-ur 20163

This theorem is referenced by:  dfur2  20165  srgidcl  20180  srgidmlem  20182  issrgid  20185  srgpcomp  20199  srg1expzeq1  20206  srgbinom  20212  ringidcl  20246  ringidmlem  20249  isringid  20252  prds1  20302  pwspjmhmmgpd  20307  pwsgprod  20309  xpsring1d  20313  oppr1  20330  unitsubm  20366  rngidpropd  20395  dfrhm2  20454  isrhm2d  20466  rhm1  20468  c0rhm  20511  c0rnghm  20512  subrgsubm  20562  issubrg3  20577  isdomn3  20692  cnfldexp  21385  expmhm  21416  nn0srg  21417  rge0srg  21418  fermltlchr  21509  freshmansdream  21554  frobrhm  21555  assamulgscmlem1  21879  mplcoe3  22016  mplcoe5  22018  mplbas2  22020  evlslem1  22060  evlsvvvallem  22069  evlsvvval  22071  evlsgsummul  22075  mhppwdeg  22116  psdpw  22136  ply1scltm  22246  ply1idvr1  22259  lply1binomsc  22276  evls1gsummul  22290  evl1gsummul  22325  madetsumid  22426  mat1mhm  22449  scmatmhm  22499  mdet0pr  22557  mdetunilem7  22583  smadiadetlem4  22634  mat2pmatmhm  22698  pm2mpmhm  22785  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  cpmadugsumlemF  22841  efsubm  26515  amgmlem  26953  amgm  26954  wilthlem2  27032  wilthlem3  27033  dchrelbas3  27201  dchrzrh1  27207  dchrmulcl  27212  dchrn0  27213  dchrinvcl  27216  dchrfi  27218  dchrabs  27223  sumdchr2  27233  rpvmasum2  27475  psgnid  33158  cnmsgn0g  33207  altgnsg  33210  urpropd  33292  isunit3  33302  elrgspnlem2  33304  erlbr2d  33325  erler  33326  rloccring  33331  rloc0g  33332  rloc1r  33333  rlocf1  33334  domnprodn0  33336  domnprodeq0  33337  rrgsubm  33345  znfermltl  33426  unitprodclb  33449  ssdifidlprm  33518  rprmdvdspow  33593  rprmdvdsprod  33594  1arithidomlem1  33595  1arithidom  33597  1arithufdlem3  33606  1arithufdlem4  33607  dfufd2lem  33609  zringfrac  33614  ressply1evls1  33625  evl1deg1  33636  evl1deg2  33637  evl1deg3  33638  deg1prod  33643  evlextv  33686  psrmonprod  33696  vieta  33724  assarrginv  33780  evls1fldgencl  33814  iistmd  34046  aks6d1c1p6  42553  evl1gprodd  42556  idomnnzpownz  42571  idomnnzgmulnz  42572  aks6d1c5lem2  42577  deg1gprod  42579  deg1pow  42580  aks5lem2  42626  unitscyglem5  42638  domnexpgn0cl  42968  abvexp  42977  evlselv  43020  mhphf  43030  mon1psubm  43627  deg1mhm  43628  amgmwlem  50277  amgmlemALT  50278