Theorem ringidval 17785

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	|- G = (mulGrp ` R )
ringidval.u	|- .1. = ( 1r ` R )

Assertion

Ref	Expression
ringidval	|- .1. = ( 0g ` G )

Proof of Theorem ringidval

Step	Hyp	Ref	Expression
1		df-ur 17784	. . . . 5 |- 1r = ( 0g o. mulGrp )
2	1	fveq1i 5888	. . . 4 |- ( 1r ` R ) = ( ( 0g o. mulGrp ) ` R )
3		fnmgp 17773	. . . . 5 |- mulGrp Fn _V
4		fvco2 5962	. . . . 5 |- ( (mulGrp Fn _V /\ R e. _V ) -> ( ( 0g o. mulGrp ) ` R ) = ( 0g ` (mulGrp ` R ) ) )
5	3, 4	mpan 681	. . . 4 |- ( R e. _V -> ( ( 0g o. mulGrp ) ` R ) = ( 0g ` (mulGrp ` R ) ) )
6	2, 5	syl5eq 2507	. . 3 |- ( R e. _V -> ( 1r ` R ) = ( 0g ` (mulGrp ` R ) ) )
7		0g0 16554	. . . 4 |- (/) = ( 0g ` (/) )
8		fvprc 5881	. . . 4 |- ( -. R e. _V -> ( 1r ` R ) = (/) )
9		fvprc 5881	. . . . 5 |- ( -. R e. _V -> (mulGrp ` R ) = (/) )
10	9	fveq2d 5891	. . . 4 |- ( -. R e. _V -> ( 0g ` (mulGrp ` R ) ) = ( 0g ` (/) ) )
11	7, 8, 10	3eqtr4a 2521	. . 3 |- ( -. R e. _V -> ( 1r ` R ) = ( 0g ` (mulGrp ` R ) ) )
12	6, 11	pm2.61i 169	. 2 |- ( 1r ` R ) = ( 0g ` (mulGrp ` R ) )
13		ringidval.u	. 2 |- .1. = ( 1r ` R )
14		ringidval.g	. . 3 |- G = (mulGrp ` R )
15	14	fveq2i 5890	. 2 |- ( 0g ` G ) = ( 0g ` (mulGrp ` R ) )
16	12, 13, 15	3eqtr4i 2493	1 |- .1. = ( 0g ` G )

Syntax hints:   -. wn 3   = wceq 1454   e. wcel 1897   _Vcvv 3056   (/)c0 3742   o. ccom 4856   Fn wfn 5595   ` cfv 5600   0gc0g 15386  mulGrpcmgp 17771   1rcur 17783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-sbc 3279  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-br 4416  df-opab 4475  df-mpt 4476  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-fv 5608  df-ov 6317  df-slot 15173  df-base 15174  df-0g 15388  df-mgp 17772  df-ur 17784

This theorem is referenced by:  dfur2  17786  srgidcl  17799  srgidmlem  17801  issrgid  17804  srgpcomp  17813  srg1expzeq1  17820  srgbinom  17826  ringidcl  17849  ringidmlem  17851  isringid  17854  prds1  17890  oppr1  17910  unitsubm  17946  rngidpropd  17971  dfrhm2  17993  isrhm2d  18004  rhm1  18006  subrgsubm  18069  issubrg3  18084  assamulgscmlem1  18620  mplcoe3  18738  mplcoe5  18740  mplbas2  18742  evlslem1  18786  ply1scltm  18922  lply1binomsc  18949  evls1gsummul  18962  evl1gsummul  18996  cnfldexp  19049  expmhm  19084  nn0srg  19085  rge0srg  19086  madetsumid  19534  mat1mhm  19557  scmatmhm  19607  mdet0pr  19665  mdetunilem7  19691  smadiadetlem4  19742  mat2pmatmhm  19805  pm2mpmhm  19892  chfacfscmulgsum  19932  chfacfpmmulgsum  19936  cpmadugsumlemF  19948  efsubm  23548  amgmlem  23963  amgm  23964  wilthlem2  24042  wilthlem3  24043  dchrelbas3  24214  dchrzrh1  24220  dchrmulcl  24225  dchrn0  24226  dchrinvcl  24229  dchrfi  24231  dchrabs  24236  sumdchr2  24246  rpvmasum2  24398  psgnid  28658  iistmd  28756  isdomn3  36125  mon1psubm  36127  deg1mhm  36128  c0rhm  40184  c0rnghm  40185