Theorem ringidval 19321

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 19320	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6659	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 19309	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6749	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 689	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	syl5eq 2805	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 17940	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6650	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6650	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6662	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2819	. . 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 6661	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2791	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1538   ∈ wcel 2111  Vcvv 3409  ∅c0 4225   ∘ ccom 5528   Fn wfn 6330  ‘cfv 6335  0_gc0g 16771  mulGrpcmgp 19307  1_rcur 19319

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 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-fv 6343  df-ov 7153  df-slot 16545  df-base 16547  df-0g 16773  df-mgp 19308  df-ur 19320

This theorem is referenced by:  dfur2  19322  srgidcl  19336  srgidmlem  19338  issrgid  19341  srgpcomp  19350  srg1expzeq1  19357  srgbinom  19363  ringidcl  19389  ringidmlem  19391  isringid  19394  prds1  19435  oppr1  19455  unitsubm  19491  rngidpropd  19516  dfrhm2  19540  isrhm2d  19551  rhm1  19553  subrgsubm  19616  issubrg3  19631  cnfldexp  20199  expmhm  20235  nn0srg  20236  rge0srg  20237  assamulgscmlem1  20662  mplcoe3  20798  mplcoe5  20800  mplbas2  20802  evlslem1  20845  evlsgsummul  20855  mhppwdeg  20893  ply1scltm  21005  lply1binomsc  21031  evls1gsummul  21044  evl1gsummul  21079  madetsumid  21161  mat1mhm  21184  scmatmhm  21234  mdet0pr  21292  mdetunilem7  21318  smadiadetlem4  21369  mat2pmatmhm  21433  pm2mpmhm  21520  chfacfscmulgsum  21560  chfacfpmmulgsum  21564  cpmadugsumlemF  21576  efsubm  25242  amgmlem  25674  amgm  25675  wilthlem2  25753  wilthlem3  25754  dchrelbas3  25921  dchrzrh1  25927  dchrmulcl  25932  dchrn0  25933  dchrinvcl  25936  dchrfi  25938  dchrabs  25943  sumdchr2  25953  rpvmasum2  26195  psgnid  30890  cnmsgn0g  30939  altgnsg  30942  freshmansdream  31010  frobrhm  31011  znfermltl  31083  iistmd  31373  pwspjmhmmgpd  39774  pwsgprod  39776  evlsbagval  39780  mhphf  39790  isdomn3  40521  mon1psubm  40523  deg1mhm  40524  c0rhm  44903  c0rnghm  44904  amgmwlem  45721  amgmlemALT  45722