Theorem ringidval 20103

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 20102	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6829	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 20062	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6925	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 690	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	eqtrid 2780	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 18574	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6820	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6820	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6832	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2794	. . 3 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
12	6, 11	pm2.61i 182	. 2 ⊢ (1r‘𝑅) = (0g‘(mulGrp‘𝑅))
13		ringidval.u	. 2 ⊢ 1 = (1r‘𝑅)
14		ringidval.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
15	14	fveq2i 6831	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2766	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2113  Vcvv 3437  ∅c0 4282   ∘ ccom 5623   Fn wfn 6481  ‘cfv 6486  0_gc0g 17345  mulGrpcmgp 20060  1_rcur 20101

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-cnex 11069  ax-1cn 11071  ax-addcl 11073

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7355  df-om 7803  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-nn 12133  df-slot 17095  df-ndx 17107  df-base 17123  df-0g 17347  df-mgp 20061  df-ur 20102

This theorem is referenced by:  dfur2  20104  srgidcl  20119  srgidmlem  20121  issrgid  20124  srgpcomp  20138  srg1expzeq1  20145  srgbinom  20151  ringidcl  20185  ringidmlem  20188  isringid  20191  prds1  20243  pwspjmhmmgpd  20248  xpsring1d  20253  oppr1  20270  unitsubm  20306  rngidpropd  20335  dfrhm2  20394  isrhm2d  20406  rhm1  20408  c0rhm  20451  c0rnghm  20452  subrgsubm  20502  issubrg3  20517  isdomn3  20632  cnfldexp  21343  expmhm  21375  nn0srg  21376  rge0srg  21377  fermltlchr  21468  freshmansdream  21513  frobrhm  21514  assamulgscmlem1  21838  mplcoe3  21974  mplcoe5  21976  mplbas2  21978  evlslem1  22018  evlsgsummul  22028  mhppwdeg  22066  psdpw  22086  ply1scltm  22196  ply1idvr1  22210  lply1binomsc  22227  evls1gsummul  22241  evl1gsummul  22276  madetsumid  22377  mat1mhm  22400  scmatmhm  22450  mdet0pr  22508  mdetunilem7  22534  smadiadetlem4  22585  mat2pmatmhm  22649  pm2mpmhm  22736  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  cpmadugsumlemF  22792  efsubm  26488  amgmlem  26928  amgm  26929  wilthlem2  27007  wilthlem3  27008  dchrelbas3  27177  dchrzrh1  27183  dchrmulcl  27188  dchrn0  27189  dchrinvcl  27192  dchrfi  27194  dchrabs  27199  sumdchr2  27209  rpvmasum2  27451  psgnid  33073  cnmsgn0g  33122  altgnsg  33125  urpropd  33206  isunit3  33215  elrgspnlem2  33217  erlbr2d  33238  erler  33239  rloccring  33244  rloc0g  33245  rloc1r  33246  rlocf1  33247  domnprodn0  33249  rrgsubm  33257  znfermltl  33338  unitprodclb  33361  ssdifidlprm  33430  rprmdvdspow  33505  rprmdvdsprod  33506  1arithidomlem1  33507  1arithidom  33509  1arithufdlem3  33518  1arithufdlem4  33519  dfufd2lem  33521  zringfrac  33526  ressply1evls1  33535  evl1deg1  33546  evl1deg2  33547  evl1deg3  33548  assarrginv  33670  evls1fldgencl  33704  iistmd  33936  aks6d1c1p6  42227  evl1gprodd  42230  idomnnzpownz  42245  idomnnzgmulnz  42246  aks6d1c5lem2  42251  deg1gprod  42253  deg1pow  42254  aks5lem2  42300  unitscyglem5  42312  domnexpgn0cl  42641  abvexp  42650  pwsgprod  42662  evlsvvvallem  42679  evlsvvval  42681  evlselv  42705  mhphf  42715  mon1psubm  43316  deg1mhm  43317  amgmwlem  49927  amgmlemALT  49928