Theorem ringidval 19247

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 19246	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6665	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 19235	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6752	. . . . 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 17868	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6657	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6657	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6668	. . . 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 6667	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2854	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1533   ∈ wcel 2110  Vcvv 3494  ∅c0 4290   ∘ ccom 5553   Fn wfn 6344  ‘cfv 6349  0_gc0g 16707  mulGrpcmgp 19233  1_rcur 19245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  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 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-fv 6357  df-ov 7153  df-slot 16481  df-base 16483  df-0g 16709  df-mgp 19234  df-ur 19246

This theorem is referenced by:  dfur2  19248  srgidcl  19262  srgidmlem  19264  issrgid  19267  srgpcomp  19276  srg1expzeq1  19283  srgbinom  19289  ringidcl  19312  ringidmlem  19314  isringid  19317  prds1  19358  oppr1  19378  unitsubm  19414  rngidpropd  19439  dfrhm2  19463  isrhm2d  19474  rhm1  19476  subrgsubm  19542  issubrg3  19557  assamulgscmlem1  20122  mplcoe3  20241  mplcoe5  20243  mplbas2  20245  evlslem1  20289  evlsgsummul  20299  ply1scltm  20443  lply1binomsc  20469  evls1gsummul  20482  evl1gsummul  20517  cnfldexp  20572  expmhm  20608  nn0srg  20609  rge0srg  20610  madetsumid  21064  mat1mhm  21087  scmatmhm  21137  mdet0pr  21195  mdetunilem7  21221  smadiadetlem4  21272  mat2pmatmhm  21335  pm2mpmhm  21422  chfacfscmulgsum  21462  chfacfpmmulgsum  21466  cpmadugsumlemF  21478  efsubm  25129  amgmlem  25561  amgm  25562  wilthlem2  25640  wilthlem3  25641  dchrelbas3  25808  dchrzrh1  25814  dchrmulcl  25819  dchrn0  25820  dchrinvcl  25823  dchrfi  25825  dchrabs  25830  sumdchr2  25840  rpvmasum2  26082  psgnid  30734  cnmsgn0g  30783  altgnsg  30786  freshmansdream  30854  iistmd  31140  isdomn3  39797  mon1psubm  39799  deg1mhm  39800  c0rhm  44177  c0rnghm  44178  amgmwlem  44897  amgmlemALT  44898