Theorem mgpplusg 20364

Description: Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.)

Hypotheses

Ref	Expression
mgpval.1	⊢ 𝑀 = (mulGrp‘𝑅)
mgpval.2	⊢ · = (.r‘𝑅)

Assertion

Ref	Expression
mgpplusg	⊢ · = (+g‘𝑀)

Proof of Theorem mgpplusg

Step	Hyp	Ref	Expression
1		mgpval.2	. . . . 5 ⊢ · = (.r‘𝑅)
2	1	fvexi 6899	. . . 4 ⊢ · ∈ V
3		plusgid 17455	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17385	. . . 4 ⊢ ((𝑅 ∈ V ∧ · ∈ V) → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
5	2, 4	mpan2 704	. . 3 ⊢ (𝑅 ∈ V → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
6		mgpval.1	. . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅)
7	6, 1	mgpval 20363	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6888	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2813	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17367	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6877	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2807	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6877	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2807	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6889	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2821	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 184	1 ⊢ · = (+g‘𝑀)

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1569   ∈ wcel 2144  Vcvv 3450  ∅c0 4278  ⟨cop 4589  ‘cfv 6538  (class class class)co 7420   sSet csts 17341  ndxcnx 17371  +_gcplusg 17428  ._rcmulr 17429  mulGrpcmgp 20360

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-1cn 11258  ax-addcl 11260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418  df-nn 12336  df-2 12405  df-sets 17342  df-slot 17360  df-ndx 17372  df-plusg 17441  df-mgp 20361

This theorem is used by:  prdsmgp  20371  elmgplsm  20372  rngass  20381  rngcl  20386  isrngd  20395  rngpropd  20396  rng1zrlem  20403  dfur2  20410  srgcl  20419  srgass  20420  srgideu  20421  srgidmlem  20427  issrgid  20430  srgpcomp  20444  srgpcompp  20445  srgbinomlem4  20455  srgbinomlem  20456  csrgbinom  20458  ringcl  20477  crngcom  20478  iscrng2  20479  ringass  20480  ringideu  20481  ringidmlem  20497  isringid  20500  ringidss  20506  isringrng  20516  dfring3  20518  ringpropd  20519  crngpropd  20520  isringd  20522  iscrngd  20523  ring1  20541  gsummgp0  20547  pwspjmhmmgpd  20557  xpsring1d  20563  oppr1  20580  unitgrp  20613  unitlinv  20623  unitrinv  20624  rdivmuldivd  20643  rngidpropd  20645  invrpropd  20648  isrnghmmul  20672  dfrhm2  20704  rhmmul  20720  isrhm2d  20721  rhmunitinv  20761  rhmimasubrnglem  20817  rhmimasubrng  20818  cntzsubrng  20819  subrgugrp  20843  issubrg3  20852  cntzsubr  20858  rhmpropd  20861  isdomn3  20966  isdrng2  20997  isdrng3lem1  21005  isdrng3lem2  21006  drngid2  21010  isdrngd  21022  isdrngdOLD  21024  cntzsdrg  21059  primefld  21062  rlmscaf  21482  rnglidlmmgm  21533  rnglidlmsgrp  21534  rng2idl1cntr  21601  cringm4  21627  ssdifidlprm  21642  prmidlsubm  21643  xrsmcmn  21701  cnfldexp  21711  cnmsubglem  21736  expmhm  21742  nn0srg  21743  rge0srg  21744  expghm  21781  frobrhm  21881  psgnghm  21886  psgnco  21889  evpmodpmf1o  21902  sraassab  22176  assamulgscmlem2  22208  psrcrng  22279  mplcoe3  22347  mplcoe5lem  22348  mplcoe5  22349  mplcoe2  22350  mplbas2  22351  evlslem1  22391  mpfind  22424  selvvvval  22451  mhppwdeg  22471  psdpw  22491  coe1tm  22592  ply1coe  22616  ringvcl  22715  mamuvs2  22721  mat1mhm  22799  scmatmhm  22849  mdetdiaglem  22913  mdetrlin  22917  mdetrsca  22918  mdetralt  22923  mdetunilem7  22933  mdetuni0  22936  m2detleib  22946  invrvald  22991  mat2pmatmhm  23051  pm2mpmhm  23138  chfacfpmmulgsum2  23183  cpmadugsumlemB  23192  cnmpt1mulr  24501  cnmpt2mulr  24502  reefgim  26777  efabl  26878  efsubm  26879  amgm  27318  wilthlem2  27396  wilthlem3  27397  dchrelbas3  27565  dchrzrhmul  27573  dchrmulcl  27576  dchrn0  27577  dchrinvcl  27580  dchrptlem2  27592  dchrsum2  27595  sum2dchr  27601  lgseisenlem3  27704  lgseisenlem4  27705  zsoring  28795  urpropd  33791  ringm1expp1  33794  ringinvval  33795  dvrcan5  33796  isunit3  33801  elrgspnlem2  33804  elrgspnsubrunlem1  33808  elrgspnsubrunlem2  33809  0ringcring  33813  erler  33826  rlocaddval  33830  rlocmulval  33831  rloccring  33832  rlocisunit  33837  domnprodn0  33839  domnprodeq0  33840  rrgsubm  33845  unitprodclb  33944  lsmsnpridl  33951  mxidlprm  33995  rprmdvdspow  34065  rprmdvdsprod  34066  1arithidomlem1  34067  1arithidom  34069  1arithufdlem2  34077  1arithufdlem3  34078  1arithufdlem4  34079  dfufd2lem  34081  zringfrac  34086  deg1prod  34115  psrmonprod  34184  mplmonprod  34186  vietalem  34211  srapwov  34221  assarrginv  34268  evls1fldgencl  34302  iistmd  34534  xrge0iifmhm  34571  xrge0pluscn  34572  pl1cn  34587  zrhcntr  34611  aks6d1c1p4  43162  evl1gprodd  43168  idomnnzpownz  43183  idomnnzgmulnz  43184  ringexp0nn  43185  aks6d1c5lem3  43188  aks6d1c5lem2  43189  deg1gprod  43191  deg1pow  43192  unitscyglem5  43250  domnexpgn0cl  43585  abvexp  43597  fidomncyc  43600  evlselv  43618  mhphf  43626  mon1psubm  44201  deg1mhm  44202  amgm2d  45198  amgm3d  45199  amgm4d  45200  2zrngmmgm  49349  2zrngmsgrp  49350  2zrngnring  49355  cznrng  49358  cznnring  49359  mgpsumunsn  49473  invginvrid  49479  elmgpcntrd  50113  amgmlemALT  50988  amgmw2d  50989