Theorem ringidval 19253

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 19252	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6671	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 19241	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6758	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 688	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	syl5eq 2868	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 17874	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6663	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6663	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6674	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2882	. . 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 6673	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2854	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1537   ∈ wcel 2114  Vcvv 3494  ∅c0 4291   ∘ ccom 5559   Fn wfn 6350  ‘cfv 6355  0_gc0g 16713  mulGrpcmgp 19239  1_rcur 19251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-fv 6363  df-ov 7159  df-slot 16487  df-base 16489  df-0g 16715  df-mgp 19240  df-ur 19252

This theorem is referenced by:  dfur2  19254  srgidcl  19268  srgidmlem  19270  issrgid  19273  srgpcomp  19282  srg1expzeq1  19289  srgbinom  19295  ringidcl  19318  ringidmlem  19320  isringid  19323  prds1  19364  oppr1  19384  unitsubm  19420  rngidpropd  19445  dfrhm2  19469  isrhm2d  19480  rhm1  19482  subrgsubm  19548  issubrg3  19563  assamulgscmlem1  20128  mplcoe3  20247  mplcoe5  20249  mplbas2  20251  evlslem1  20295  evlsgsummul  20305  ply1scltm  20449  lply1binomsc  20475  evls1gsummul  20488  evl1gsummul  20523  cnfldexp  20578  expmhm  20614  nn0srg  20615  rge0srg  20616  madetsumid  21070  mat1mhm  21093  scmatmhm  21143  mdet0pr  21201  mdetunilem7  21227  smadiadetlem4  21278  mat2pmatmhm  21341  pm2mpmhm  21428  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  cpmadugsumlemF  21484  efsubm  25135  amgmlem  25567  amgm  25568  wilthlem2  25646  wilthlem3  25647  dchrelbas3  25814  dchrzrh1  25820  dchrmulcl  25825  dchrn0  25826  dchrinvcl  25829  dchrfi  25831  dchrabs  25836  sumdchr2  25846  rpvmasum2  26088  psgnid  30739  cnmsgn0g  30788  altgnsg  30791  freshmansdream  30859  iistmd  31145  isdomn3  39824  mon1psubm  39826  deg1mhm  39827  c0rhm  44203  c0rnghm  44204  amgmwlem  44923  amgmlemALT  44924