Theorem ringidval 18503

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 18502	. . . . 5 |- 1r = ( 0g o. mulGrp )
2	1	fveq1i 6192	. . . 4 |- ( 1r ` R ) = ( ( 0g o. mulGrp ) ` R )
3		fnmgp 18491	. . . . 5 |- mulGrp Fn _V
4		fvco2 6273	. . . . 5 |- ( (mulGrp Fn _V /\ R e. _V ) -> ( ( 0g o. mulGrp ) ` R ) = ( 0g ` (mulGrp ` R ) ) )
5	3, 4	mpan 706	. . . 4 |- ( R e. _V -> ( ( 0g o. mulGrp ) ` R ) = ( 0g ` (mulGrp ` R ) ) )
6	2, 5	syl5eq 2668	. . 3 |- ( R e. _V -> ( 1r ` R ) = ( 0g ` (mulGrp ` R ) ) )
7		0g0 17263	. . . 4 |- (/) = ( 0g ` (/) )
8		fvprc 6185	. . . 4 |- ( -. R e. _V -> ( 1r ` R ) = (/) )
9		fvprc 6185	. . . . 5 |- ( -. R e. _V -> (mulGrp ` R ) = (/) )
10	9	fveq2d 6195	. . . 4 |- ( -. R e. _V -> ( 0g ` (mulGrp ` R ) ) = ( 0g ` (/) ) )
11	7, 8, 10	3eqtr4a 2682	. . 3 |- ( -. R e. _V -> ( 1r ` R ) = ( 0g ` (mulGrp ` R ) ) )
12	6, 11	pm2.61i 176	. 2 |- ( 1r ` R ) = ( 0g ` (mulGrp ` R ) )
13		ringidval.u	. 2 |- .1. = ( 1r ` R )
14		ringidval.g	. . 3 |- G = (mulGrp ` R )
15	14	fveq2i 6194	. 2 |- ( 0g ` G ) = ( 0g ` (mulGrp ` R ) )
16	12, 13, 15	3eqtr4i 2654	1 |- .1. = ( 0g ` G )

Syntax hints:   -. wn 3   = wceq 1483   e. wcel 1990   _Vcvv 3200   (/)c0 3915   o. ccom 5118   Fn wfn 5883   ` cfv 5888   0gc0g 16100  mulGrpcmgp 18489   1rcur 18501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-fv 5896  df-ov 6653  df-slot 15861  df-base 15863  df-0g 16102  df-mgp 18490  df-ur 18502

This theorem is referenced by:  dfur2  18504  srgidcl  18518  srgidmlem  18520  issrgid  18523  srgpcomp  18532  srg1expzeq1  18539  srgbinom  18545  ringidcl  18568  ringidmlem  18570  isringid  18573  prds1  18614  oppr1  18634  unitsubm  18670  rngidpropd  18695  dfrhm2  18717  isrhm2d  18728  rhm1  18730  subrgsubm  18793  issubrg3  18808  assamulgscmlem1  19348  mplcoe3  19466  mplcoe5  19468  mplbas2  19470  evlslem1  19515  ply1scltm  19651  lply1binomsc  19677  evls1gsummul  19690  evl1gsummul  19724  cnfldexp  19779  expmhm  19815  nn0srg  19816  rge0srg  19817  madetsumid  20267  mat1mhm  20290  scmatmhm  20340  mdet0pr  20398  mdetunilem7  20424  smadiadetlem4  20475  mat2pmatmhm  20538  pm2mpmhm  20625  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  cpmadugsumlemF  20681  efsubm  24297  amgmlem  24716  amgm  24717  wilthlem2  24795  wilthlem3  24796  dchrelbas3  24963  dchrzrh1  24969  dchrmulcl  24974  dchrn0  24975  dchrinvcl  24978  dchrfi  24980  dchrabs  24985  sumdchr2  24995  rpvmasum2  25201  psgnid  29847  iistmd  29948  isdomn3  37782  mon1psubm  37784  deg1mhm  37785  c0rhm  41912  c0rnghm  41913  amgmwlem  42548  amgmlemALT  42549