Theorem ringidval 18549

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 18548	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6230	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 18537	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 6312	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 706	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	syl5eq 2697	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 17310	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6223	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6223	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6233	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2711	. . 3 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
12	6, 11	pm2.61i 176	. 2 ⊢ (1r‘𝑅) = (0g‘(mulGrp‘𝑅))
13		ringidval.u	. 2 ⊢ 1 = (1r‘𝑅)
14		ringidval.g	. . 3 ⊢ 𝐺 = (mulGrp‘𝑅)
15	14	fveq2i 6232	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2683	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1523   ∈ wcel 2030  Vcvv 3231  ∅c0 3948   ∘ ccom 5147   Fn wfn 5921  ‘cfv 5926  0_gc0g 16147  mulGrpcmgp 18535  1_rcur 18547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-fv 5934  df-ov 6693  df-slot 15908  df-base 15910  df-0g 16149  df-mgp 18536  df-ur 18548

This theorem is referenced by:  dfur2  18550  srgidcl  18564  srgidmlem  18566  issrgid  18569  srgpcomp  18578  srg1expzeq1  18585  srgbinom  18591  ringidcl  18614  ringidmlem  18616  isringid  18619  prds1  18660  oppr1  18680  unitsubm  18716  rngidpropd  18741  dfrhm2  18765  isrhm2d  18776  rhm1  18778  subrgsubm  18841  issubrg3  18856  assamulgscmlem1  19396  mplcoe3  19514  mplcoe5  19516  mplbas2  19518  evlslem1  19563  ply1scltm  19699  lply1binomsc  19725  evls1gsummul  19738  evl1gsummul  19772  cnfldexp  19827  expmhm  19863  nn0srg  19864  rge0srg  19865  madetsumid  20315  mat1mhm  20338  scmatmhm  20388  mdet0pr  20446  mdetunilem7  20472  smadiadetlem4  20523  mat2pmatmhm  20586  pm2mpmhm  20673  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  cpmadugsumlemF  20729  efsubm  24342  amgmlem  24761  amgm  24762  wilthlem2  24840  wilthlem3  24841  dchrelbas3  25008  dchrzrh1  25014  dchrmulcl  25019  dchrn0  25020  dchrinvcl  25023  dchrfi  25025  dchrabs  25030  sumdchr2  25040  rpvmasum2  25246  psgnid  29975  iistmd  30076  isdomn3  38099  mon1psubm  38101  deg1mhm  38102  c0rhm  42237  c0rnghm  42238  amgmwlem  42876  amgmlemALT  42877