Theorem ringidval 18711

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 18710	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6333	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 18699	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6415	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 670	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	syl5eq 2817	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 17471	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6326	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6326	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6336	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2831	. . 3 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
12	6, 11	pm2.61i 176	. 2 ⊢ (1r‘𝑅) = (0g‘(mulGrp‘𝑅))
13		ringidval.u	. 2 ⊢ 1 = (1r‘𝑅)
14		ringidval.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
15	14	fveq2i 6335	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2803	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1631   ∈ wcel 2145  Vcvv 3351  ∅c0 4063   ∘ ccom 5253   Fn wfn 6026  ‘cfv 6031  0_gc0g 16308  mulGrpcmgp 18697  1_rcur 18709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-fv 6039  df-ov 6796  df-slot 16068  df-base 16070  df-0g 16310  df-mgp 18698  df-ur 18710

This theorem is referenced by:  dfur2  18712  srgidcl  18726  srgidmlem  18728  issrgid  18731  srgpcomp  18740  srg1expzeq1  18747  srgbinom  18753  ringidcl  18776  ringidmlem  18778  isringid  18781  prds1  18822  oppr1  18842  unitsubm  18878  rngidpropd  18903  dfrhm2  18927  isrhm2d  18938  rhm1  18940  subrgsubm  19003  issubrg3  19018  assamulgscmlem1  19563  mplcoe3  19681  mplcoe5  19683  mplbas2  19685  evlslem1  19730  ply1scltm  19866  lply1binomsc  19892  evls1gsummul  19905  evl1gsummul  19939  cnfldexp  19994  expmhm  20030  nn0srg  20031  rge0srg  20032  madetsumid  20485  mat1mhm  20508  scmatmhm  20558  mdet0pr  20616  mdetunilem7  20642  smadiadetlem4  20694  mat2pmatmhm  20758  pm2mpmhm  20845  chfacfscmulgsum  20885  chfacfpmmulgsum  20889  cpmadugsumlemF  20901  efsubm  24518  amgmlem  24937  amgm  24938  wilthlem2  25016  wilthlem3  25017  dchrelbas3  25184  dchrzrh1  25190  dchrmulcl  25195  dchrn0  25196  dchrinvcl  25199  dchrfi  25201  dchrabs  25206  sumdchr2  25216  rpvmasum2  25422  psgnid  30187  iistmd  30288  isdomn3  38308  mon1psubm  38310  deg1mhm  38311  c0rhm  42440  c0rnghm  42441  amgmwlem  43079  amgmlemALT  43080