Theorem ringidval 19246

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 19245	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6646	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 19234	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6735	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 689	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	syl5eq 2845	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 17866	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6638	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6638	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6649	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2859	. . 3 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
12	6, 11	pm2.61i 185	. 2 ⊢ (1r‘𝑅) = (0g‘(mulGrp‘𝑅))
13		ringidval.u	. 2 ⊢ 1 = (1r‘𝑅)
14		ringidval.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
15	14	fveq2i 6648	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2831	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1538   ∈ wcel 2111  Vcvv 3441  ∅c0 4243   ∘ ccom 5523   Fn wfn 6319  ‘cfv 6324  0_gc0g 16705  mulGrpcmgp 19232  1_rcur 19244

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-fv 6332  df-ov 7138  df-slot 16479  df-base 16481  df-0g 16707  df-mgp 19233  df-ur 19245

This theorem is referenced by:  dfur2  19247  srgidcl  19261  srgidmlem  19263  issrgid  19266  srgpcomp  19275  srg1expzeq1  19282  srgbinom  19288  ringidcl  19314  ringidmlem  19316  isringid  19319  prds1  19360  oppr1  19380  unitsubm  19416  rngidpropd  19441  dfrhm2  19465  isrhm2d  19476  rhm1  19478  subrgsubm  19541  issubrg3  19556  cnfldexp  20124  expmhm  20160  nn0srg  20161  rge0srg  20162  assamulgscmlem1  20585  mplcoe3  20706  mplcoe5  20708  mplbas2  20710  evlslem1  20754  evlsgsummul  20764  ply1scltm  20910  lply1binomsc  20936  evls1gsummul  20949  evl1gsummul  20984  madetsumid  21066  mat1mhm  21089  scmatmhm  21139  mdet0pr  21197  mdetunilem7  21223  smadiadetlem4  21274  mat2pmatmhm  21338  pm2mpmhm  21425  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  cpmadugsumlemF  21481  efsubm  25143  amgmlem  25575  amgm  25576  wilthlem2  25654  wilthlem3  25655  dchrelbas3  25822  dchrzrh1  25828  dchrmulcl  25833  dchrn0  25834  dchrinvcl  25837  dchrfi  25839  dchrabs  25844  sumdchr2  25854  rpvmasum2  26096  psgnid  30789  cnmsgn0g  30838  altgnsg  30841  freshmansdream  30909  frobrhm  30910  iistmd  31255  isdomn3  40148  mon1psubm  40150  deg1mhm  40151  c0rhm  44536  c0rnghm  44537  amgmwlem  45330  amgmlemALT  45331