Theorem ringidval 20266

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 20265	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6884	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 20219	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6980	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 702	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	eqtrid 2810	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 18723	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6875	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6875	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6887	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2824	. . 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 6886	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2796	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1570   ∈ wcel 2143  Vcvv 3455  ∅c0 4287   ∘ ccom 5667   Fn wfn 6533  ‘cfv 6538  0_gc0g 17493  mulGrpcmgp 20217  1_rcur 20264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-1cn 11159  ax-addcl 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-nn 12235  df-slot 17243  df-ndx 17255  df-base 17271  df-0g 17495  df-mgp 20218  df-ur 20265

This theorem is referenced by:  dfur2  20267  srgidcl  20282  srgidmlem  20284  issrgid  20287  srgpcomp  20301  srg1expzeq1  20308  srgbinom  20314  ringidcl  20349  ringidmlem  20352  isringid  20355  prds1  20405  pwspjmhmmgpd  20410  pwsgprod  20412  xpsring1d  20416  oppr1  20433  unitsubm  20469  rngidpropd  20498  dfrhm2  20557  isrhm2d  20570  rhm1  20572  c0rhm  20620  c0rnghm  20621  subrgsubm  20671  issubrg3  20686  isdomn3  20800  ssdifidlprm  21467  prmidlsubm  21468  cnfldexp  21536  expmhm  21567  nn0srg  21568  rge0srg  21569  fermltlchr  21660  freshmansdream  21705  frobrhm  21706  assamulgscmlem1  22030  mplcoe3  22170  mplcoe5  22172  mplbas2  22174  evlslem1  22214  evlsvvvallem  22223  evlsvvval  22225  evlsgsummul  22229  mhppwdeg  22294  psdpw  22314  ply1scltm  22423  ply1idvr1  22436  lply1binomsc  22452  evls1gsummul  22466  evl1gsummul  22501  madetsumid  22599  mat1mhm  22622  scmatmhm  22672  mdet0pr  22730  mdetunilem7  22756  smadiadetlem4  22807  mat2pmatmhm  22871  pm2mpmhm  22958  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  cpmadugsumlemF  23014  efsubm  26694  amgmlem  27132  amgm  27133  wilthlem2  27211  wilthlem3  27212  dchrelbas3  27380  dchrzrh1  27386  dchrmulcl  27391  dchrn0  27392  dchrinvcl  27395  dchrfi  27397  dchrabs  27402  sumdchr2  27412  rpvmasum2  27654  psgnid  33395  cnmsgn0g  33444  altgnsg  33447  urpropd  33528  isunit3  33538  elrgspnlem2  33541  erlbr2d  33562  erler  33563  rloccring  33569  rloc0g  33570  rloc1r  33571  rlocf1  33572  rlocinvunit  33573  rlocisunit  33574  domnprodn0  33576  domnprodeq0  33577  rrgsubm  33582  znfermltl  33659  unitprodclb  33680  rprmdvdspow  33801  rprmdvdsprod  33802  1arithidomlem1  33803  1arithidom  33805  1arithufdlem3  33814  1arithufdlem4  33815  dfufd2lem  33817  zringfrac  33822  ressply1evls1  33833  evl1deg1  33844  evl1deg2  33845  evl1deg3  33846  deg1prod  33851  evlextv  33910  psrmonprod  33920  vieta  33948  assarrginv  34004  evls1fldgencl  34038  iistmd  34270  aks6d1c1p6  42859  evl1gprodd  42862  idomnnzpownz  42877  idomnnzgmulnz  42878  aks6d1c5lem2  42883  deg1gprod  42885  deg1pow  42886  aks5lem2  42932  unitscyglem5  42944  domnexpgn0cl  43271  abvexp  43280  evlselv  43301  mhphf  43309  mon1psubm  43906  deg1mhm  43907  amgmwlem  50579  amgmlemALT  50580