Theorem mgpplusg 19990

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 6905	. . . 4 ⊢ · ∈ V
3		plusgid 17223	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17140	. . . 4 ⊢ ((𝑅 ∈ V ∧ · ∈ V) → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
5	2, 4	mpan2 689	. . 3 ⊢ (𝑅 ∈ V → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
6		mgpval.1	. . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅)
7	6, 1	mgpval 19989	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6894	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2790	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17121	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6883	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2784	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6883	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2784	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6895	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2798	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 182	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2106  Vcvv 3474  ∅c0 4322  ⟨cop 4634  ‘cfv 6543  (class class class)co 7408   sSet csts 17095  ndxcnx 17125  +_gcplusg 17196  ._rcmulr 17197  mulGrpcmgp 19986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-1cn 11167  ax-addcl 11169

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-nn 12212  df-2 12274  df-sets 17096  df-slot 17114  df-ndx 17126  df-plusg 17209  df-mgp 19987

This theorem is referenced by:  dfur2  20006  srgcl  20015  srgass  20016  srgideu  20017  srgidmlem  20023  issrgid  20026  srg1zr  20037  srgpcomp  20040  srgpcompp  20041  srgbinomlem4  20051  srgbinomlem  20052  csrgbinom  20054  ringcl  20072  crngcom  20073  iscrng2  20074  ringass  20075  ringideu  20076  ringidmlem  20084  isringid  20087  ringidss  20093  ringpropd  20101  crngpropd  20102  isringd  20104  iscrngd  20105  ring1  20121  gsummgp0  20129  prdsmgp  20131  pwspjmhmmgpd  20140  xpsring1d  20145  oppr1  20163  unitgrp  20196  unitlinv  20206  unitrinv  20207  rdivmuldivd  20226  rngidpropd  20228  invrpropd  20231  dfrhm2  20252  rhmmul  20263  isrhm2d  20264  rhmunitinv  20289  subrgugrp  20337  issubrg3  20346  cntzsubr  20352  rhmpropd  20355  isdrng2  20370  drngmcl  20373  drngid2  20377  isdrngd  20389  isdrngdOLD  20391  cntzsdrg  20417  primefld  20420  rlmscaf  20830  xrsmcmn  20967  cnfldexp  20977  cnmsubglem  21007  expmhm  21013  nn0srg  21014  rge0srg  21015  expghm  21044  psgnghm  21132  psgnco  21135  evpmodpmf1o  21148  sraassab  21421  sraassaOLD  21423  assamulgscmlem2  21453  psrcrng  21532  mplcoe3  21592  mplcoe5lem  21593  mplcoe5  21594  mplcoe2  21595  mplbas2  21596  evlslem1  21644  mpfind  21669  mhppwdeg  21692  coe1tm  21794  ply1coe  21819  ringvcl  21899  mamuvs2  21905  mat1mhm  21985  scmatmhm  22035  mdetdiaglem  22099  mdetrlin  22103  mdetrsca  22104  mdetralt  22109  mdetunilem7  22119  mdetuni0  22122  m2detleib  22132  invrvald  22177  mat2pmatmhm  22234  pm2mpmhm  22321  chfacfpmmulgsum2  22366  cpmadugsumlemB  22375  cnmpt1mulr  23685  cnmpt2mulr  23686  reefgim  25961  efabl  26058  efsubm  26059  amgm  26492  wilthlem2  26570  wilthlem3  26571  dchrelbas3  26738  dchrzrhmul  26746  dchrmulcl  26749  dchrn0  26750  dchrinvcl  26753  dchrptlem2  26765  dchrsum2  26768  sum2dchr  26774  lgseisenlem3  26877  lgseisenlem4  26878  urpropd  32373  frobrhm  32377  ringinvval  32379  dvrcan5  32380  elringlsm  32498  lsmsnpridl  32503  cringm4  32560  mxidlprm  32581  iistmd  32877  xrge0iifmhm  32914  xrge0pluscn  32915  pl1cn  32930  selvvvval  41159  evlselv  41161  mhphf  41171  isdomn3  41936  mon1psubm  41938  deg1mhm  41939  amgm2d  42940  amgm3d  42941  amgm4d  42942  isringrng  46647  rngass  46648  rngcl  46653  isrngd  46662  rngpropd  46663  isrnghmmul  46681  rhmimasubrnglem  46734  rhmimasubrng  46735  cntzsubrng  46736  rnglidlmmgm  46746  rnglidlmsgrp  46747  rng2idl1cntr  46780  2zrngmmgm  46834  2zrngmsgrp  46835  2zrngnring  46840  cznrng  46843  cznnring  46844  mgpsumunsn  47027  invginvrid  47033  amgmlemALT  47840  amgmw2d  47841