Theorem ringidval 20180

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 20179	. . . . 5 ⊢ 1r = (0g ∘ mulGrp)
2	1	fveq1i 6907	. . . 4 ⊢ (1r‘𝑅) = ((0g ∘ mulGrp)‘𝑅)
3		fnmgp 20139	. . . . 5 ⊢ mulGrp Fn V
4		fvco2 7006	. . . . 5 ⊢ ((mulGrp Fn V ∧ 𝑅 ∈ V) → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
5	3, 4	mpan 690	. . . 4 ⊢ (𝑅 ∈ V → ((0g ∘ mulGrp)‘𝑅) = (0g‘(mulGrp‘𝑅)))
6	2, 5	eqtrid 2789	. . 3 ⊢ (𝑅 ∈ V → (1r‘𝑅) = (0g‘(mulGrp‘𝑅)))
7		0g0 18677	. . . 4 ⊢ ∅ = (0g‘∅)
8		fvprc 6898	. . . 4 ⊢ (¬ 𝑅 ∈ V → (1r‘𝑅) = ∅)
9		fvprc 6898	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
10	9	fveq2d 6910	. . . 4 ⊢ (¬ 𝑅 ∈ V → (0g‘(mulGrp‘𝑅)) = (0g‘∅))
11	7, 8, 10	3eqtr4a 2803	. . 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 6909	. 2 ⊢ (0g‘𝐺) = (0g‘(mulGrp‘𝑅))
16	12, 13, 15	3eqtr4i 2775	1 ⊢ 1 = (0g‘𝐺)

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2108  Vcvv 3480  ∅c0 4333   ∘ ccom 5689   Fn wfn 6556  ‘cfv 6561  0_gc0g 17484  mulGrpcmgp 20137  1_rcur 20178

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-1cn 11213  ax-addcl 11215

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267  df-slot 17219  df-ndx 17231  df-base 17248  df-0g 17486  df-mgp 20138  df-ur 20179

This theorem is referenced by:  dfur2  20181  srgidcl  20196  srgidmlem  20198  issrgid  20201  srgpcomp  20215  srg1expzeq1  20222  srgbinom  20228  ringidcl  20262  ringidmlem  20265  isringid  20268  prds1  20320  pwspjmhmmgpd  20325  xpsring1d  20330  oppr1  20350  unitsubm  20386  rngidpropd  20415  dfrhm2  20474  isrhm2d  20487  rhm1  20489  c0rhm  20534  c0rnghm  20535  subrgsubm  20585  issubrg3  20600  isdomn3  20715  cnfldexp  21417  expmhm  21454  nn0srg  21455  rge0srg  21456  fermltlchr  21544  freshmansdream  21593  frobrhm  21594  assamulgscmlem1  21919  mplcoe3  22056  mplcoe5  22058  mplbas2  22060  evlslem1  22106  evlsgsummul  22116  mhppwdeg  22154  psdpw  22174  ply1scltm  22284  ply1idvr1  22298  lply1binomsc  22315  evls1gsummul  22329  evl1gsummul  22364  madetsumid  22467  mat1mhm  22490  scmatmhm  22540  mdet0pr  22598  mdetunilem7  22624  smadiadetlem4  22675  mat2pmatmhm  22739  pm2mpmhm  22826  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  cpmadugsumlemF  22882  efsubm  26593  amgmlem  27033  amgm  27034  wilthlem2  27112  wilthlem3  27113  dchrelbas3  27282  dchrzrh1  27288  dchrmulcl  27293  dchrn0  27294  dchrinvcl  27297  dchrfi  27299  dchrabs  27304  sumdchr2  27314  rpvmasum2  27556  psgnid  33117  cnmsgn0g  33166  altgnsg  33169  urpropd  33236  isunit3  33245  elrgspnlem2  33247  erlbr2d  33268  erler  33269  rloccring  33274  rloc0g  33275  rloc1r  33276  rlocf1  33277  domnprodn0  33279  rrgsubm  33287  znfermltl  33394  unitprodclb  33417  ssdifidlprm  33486  rprmdvdspow  33561  rprmdvdsprod  33562  1arithidomlem1  33563  1arithidom  33565  1arithufdlem3  33574  1arithufdlem4  33575  dfufd2lem  33577  zringfrac  33582  evl1deg1  33601  evl1deg2  33602  evl1deg3  33603  assarrginv  33687  evls1fldgencl  33720  iistmd  33901  aks6d1c1p6  42115  evl1gprodd  42118  idomnnzpownz  42133  idomnnzgmulnz  42134  aks6d1c5lem2  42139  deg1gprod  42141  deg1pow  42142  aks5lem2  42188  unitscyglem5  42200  domnexpgn0cl  42533  abvexp  42542  pwsgprod  42554  evlsvvvallem  42571  evlsvvval  42573  evlselv  42597  mhphf  42607  mon1psubm  43211  deg1mhm  43212  amgmwlem  49321  amgmlemALT  49322