Theorem ringidval 20077

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 20076	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6891	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 20030	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6987	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 686	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	eqtrid 2782	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 18589	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6882	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6882	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6894	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2796	. . 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 6893	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2768	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2104  Vcvv 3472  ∅c0 4321   ∘ ccom 5679   Fn wfn 6537  ‘cfv 6542  0_gc0g 17389  mulGrpcmgp 20028  1_rcur 20075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-1cn 11170  ax-addcl 11172

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-nn 12217  df-slot 17119  df-ndx 17131  df-base 17149  df-0g 17391  df-mgp 20029  df-ur 20076

This theorem is referenced by:  dfur2  20078  srgidcl  20093  srgidmlem  20095  issrgid  20098  srgpcomp  20112  srg1expzeq1  20119  srgbinom  20125  ringidcl  20154  ringidmlem  20156  isringid  20159  prds1  20211  pwspjmhmmgpd  20216  xpsring1d  20221  oppr1  20241  unitsubm  20277  rngidpropd  20306  dfrhm2  20365  isrhm2d  20378  rhm1  20380  c0rhm  20423  c0rnghm  20424  subrgsubm  20475  issubrg3  20490  cnfldexp  21178  expmhm  21214  nn0srg  21215  rge0srg  21216  assamulgscmlem1  21672  mplcoe3  21812  mplcoe5  21814  mplbas2  21816  evlslem1  21864  evlsgsummul  21874  mhppwdeg  21912  ply1scltm  22023  lply1binomsc  22051  evls1gsummul  22064  evl1gsummul  22099  madetsumid  22183  mat1mhm  22206  scmatmhm  22256  mdet0pr  22314  mdetunilem7  22340  smadiadetlem4  22391  mat2pmatmhm  22455  pm2mpmhm  22542  chfacfscmulgsum  22582  chfacfpmmulgsum  22586  cpmadugsumlemF  22598  efsubm  26296  amgmlem  26730  amgm  26731  wilthlem2  26809  wilthlem3  26810  dchrelbas3  26977  dchrzrh1  26983  dchrmulcl  26988  dchrn0  26989  dchrinvcl  26992  dchrfi  26994  dchrabs  26999  sumdchr2  27009  rpvmasum2  27251  psgnid  32526  cnmsgn0g  32575  altgnsg  32578  urpropd  32648  freshmansdream  32651  frobrhm  32652  fermltlchr  32752  znfermltl  32753  evls1fldgencl  33033  iistmd  33180  pwsgprod  41416  evlsvvvallem  41435  evlsvvval  41437  evlselv  41461  mhphf  41471  isdomn3  42248  mon1psubm  42250  deg1mhm  42251  amgmwlem  47936  amgmlemALT  47937