Theorem ringidval 20296

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 20295	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6889	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 20249	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6985	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 703	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	eqtrid 2813	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 18747	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6880	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6880	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6892	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2827	. . 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 6891	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2799	1 ⊢ 1 = (0g‘𝐺)

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2146  Vcvv 3458  ∅c0 4289   ∘ ccom 5670   Fn wfn 6538  ‘cfv 6543  0_gc0g 17517  mulGrpcmgp 20247  1_rcur 20294

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-1cn 11176  ax-addcl 11178

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 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-nn 12252  df-slot 17267  df-ndx 17279  df-base 17295  df-0g 17519  df-mgp 20248  df-ur 20295

This theorem is used by:  dfur2  20297  srgidcl  20312  srgidmlem  20314  issrgid  20317  srgpcomp  20331  srg1expzeq1  20338  srgbinom  20344  ringidcl  20380  ringidmlem  20383  isringid  20386  prds1  20437  pwspjmhmmgpd  20442  pwsgprod  20444  xpsring1d  20448  oppr1  20465  unitsubm  20501  rngidpropd  20530  dfrhm2  20589  isrhm2d  20606  rhm1  20609  c0rhm  20670  c0rnghm  20671  subrgsubm  20721  issubrg3  20736  isdomn3  20850  isdrng3lem1  20888  ssdifidlprm  21523  prmidlsubm  21524  cnfldexp  21592  expmhm  21623  nn0srg  21624  rge0srg  21625  fermltlchr  21716  freshmansdream  21761  frobrhm  21762  assamulgscmlem1  22086  mplcoe3  22226  mplcoe5  22228  mplbas2  22230  evlslem1  22270  evlsvvvallem  22279  evlsvvval  22281  evlsgsummul  22285  mhppwdeg  22350  psdpw  22370  ply1scltm  22479  ply1idvr1  22492  lply1binomsc  22508  evls1gsummul  22522  evl1gsummul  22557  madetsumid  22655  mat1mhm  22678  scmatmhm  22728  mdet0pr  22786  mdetunilem7  22812  smadiadetlem4  22863  mat2pmatmhm  22927  pm2mpmhm  23014  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  cpmadugsumlemF  23070  efsubm  26753  amgmlem  27191  amgm  27192  wilthlem2  27270  wilthlem3  27271  dchrelbas3  27439  dchrzrh1  27445  dchrmulcl  27450  dchrn0  27451  dchrinvcl  27454  dchrfi  27456  dchrabs  27461  sumdchr2  27471  rpvmasum2  27713  psgnid  33448  cnmsgn0g  33497  altgnsg  33500  urpropd  33581  isunit3  33591  elrgspnlem2  33594  erlbr2d  33615  erler  33616  rloccring  33622  rloc0g  33623  rloc1r  33624  rlocf1  33625  rlocinvunit  33626  rlocisunit  33627  domnprodn0  33629  domnprodeq0  33630  rrgsubm  33635  znfermltl  33712  unitprodclb  33733  rprmdvdspow  33854  rprmdvdsprod  33855  1arithidomlem1  33856  1arithidom  33858  1arithufdlem3  33867  1arithufdlem4  33868  dfufd2lem  33870  zringfrac  33875  ressply1evls1  33886  evl1deg1  33897  evl1deg2  33898  evl1deg3  33899  deg1prod  33904  evlextv  33963  psrmonprod  33973  vieta  34001  assarrginv  34057  evls1fldgencl  34091  iistmd  34323  aks6d1c1p6  42921  evl1gprodd  42924  idomnnzpownz  42939  idomnnzgmulnz  42940  aks6d1c5lem2  42945  deg1gprod  42947  deg1pow  42948  aks5lem2  42994  unitscyglem5  43006  domnexpgn0cl  43331  abvexp  43340  evlselv  43361  mhphf  43369  mon1psubm  43966  deg1mhm  43967  amgmwlem  50690  amgmlemALT  50691