Theorem mgpplusg 20029

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 6836	. . . 4 ⊢ · ∈ V
3		plusgid 17188	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17118	. . . 4 ⊢ ((𝑅 ∈ V ∧ · ∈ V) → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
5	2, 4	mpan2 691	. . 3 ⊢ (𝑅 ∈ V → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
6		mgpval.1	. . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅)
7	6, 1	mgpval 20028	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6825	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2782	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17100	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6814	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2776	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6814	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2776	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6826	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2790	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 182	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109  Vcvv 3436  ∅c0 4284  ⟨cop 4583  ‘cfv 6482  (class class class)co 7349   sSet csts 17074  ndxcnx 17104  +_gcplusg 17161  ._rcmulr 17162  mulGrpcmgp 20025

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-1cn 11067  ax-addcl 11069

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-nn 12129  df-2 12191  df-sets 17075  df-slot 17093  df-ndx 17105  df-plusg 17174  df-mgp 20026

This theorem is referenced by:  prdsmgp  20036  rngass  20044  rngcl  20049  isrngd  20058  rngpropd  20059  dfur2  20069  srgcl  20078  srgass  20079  srgideu  20080  srgidmlem  20086  issrgid  20089  srg1zr  20100  srgpcomp  20103  srgpcompp  20104  srgbinomlem4  20114  srgbinomlem  20115  csrgbinom  20117  ringcl  20135  crngcom  20136  iscrng2  20137  ringass  20138  ringideu  20139  ringidmlem  20153  isringid  20156  ringidss  20162  isringrng  20172  ringpropd  20173  crngpropd  20174  isringd  20176  iscrngd  20177  ring1  20195  gsummgp0  20203  pwspjmhmmgpd  20213  xpsring1d  20218  oppr1  20235  unitgrp  20268  unitlinv  20278  unitrinv  20279  rdivmuldivd  20298  rngidpropd  20300  invrpropd  20303  isrnghmmul  20327  dfrhm2  20359  rhmmul  20371  isrhm2d  20372  rhmunitinv  20396  rhmimasubrnglem  20450  rhmimasubrng  20451  cntzsubrng  20452  subrgugrp  20476  issubrg3  20485  cntzsubr  20491  rhmpropd  20494  isdomn3  20600  isdrng2  20628  drngmclOLD  20636  drngid2  20637  isdrngd  20650  isdrngdOLD  20652  cntzsdrg  20687  primefld  20690  rlmscaf  21111  rnglidlmmgm  21152  rnglidlmsgrp  21153  rng2idl1cntr  21212  xrsmcmn  21298  cnfldexp  21311  cnmsubglem  21337  expmhm  21343  nn0srg  21344  rge0srg  21345  expghm  21382  frobrhm  21482  psgnghm  21487  psgnco  21490  evpmodpmf1o  21503  sraassab  21775  sraassaOLD  21777  assamulgscmlem2  21807  psrcrng  21879  mplcoe3  21943  mplcoe5lem  21944  mplcoe5  21945  mplcoe2  21946  mplbas2  21947  evlslem1  21987  mpfind  22012  mhppwdeg  22035  psdpw  22055  coe1tm  22157  ply1coe  22183  ringvcl  22285  mamuvs2  22291  mat1mhm  22369  scmatmhm  22419  mdetdiaglem  22483  mdetrlin  22487  mdetrsca  22488  mdetralt  22493  mdetunilem7  22503  mdetuni0  22506  m2detleib  22516  invrvald  22561  mat2pmatmhm  22618  pm2mpmhm  22705  chfacfpmmulgsum2  22750  cpmadugsumlemB  22759  cnmpt1mulr  24067  cnmpt2mulr  24068  reefgim  26358  efabl  26457  efsubm  26458  amgm  26899  wilthlem2  26977  wilthlem3  26978  dchrelbas3  27147  dchrzrhmul  27155  dchrmulcl  27158  dchrn0  27159  dchrinvcl  27162  dchrptlem2  27174  dchrsum2  27177  sum2dchr  27183  lgseisenlem3  27286  lgseisenlem4  27287  zsoring  28301  urpropd  33173  ringinvval  33176  dvrcan5  33177  isunit3  33182  elrgspnlem2  33184  elrgspnsubrunlem1  33188  elrgspnsubrunlem2  33189  0ringcring  33193  erler  33206  rlocaddval  33209  rlocmulval  33210  rloccring  33211  domnprodn0  33216  rrgsubm  33224  unitprodclb  33327  elringlsm  33331  lsmsnpridl  33336  cringm4  33384  ssdifidlprm  33396  mxidlprm  33408  rprmdvdspow  33471  rprmdvdsprod  33472  1arithidomlem1  33473  1arithidom  33475  1arithufdlem2  33483  1arithufdlem3  33484  1arithufdlem4  33485  dfufd2lem  33487  zringfrac  33492  srapwov  33561  assarrginv  33609  evls1fldgencl  33643  iistmd  33875  xrge0iifmhm  33912  xrge0pluscn  33913  pl1cn  33928  zrhcntr  33952  aks6d1c1p4  42094  evl1gprodd  42100  idomnnzpownz  42115  idomnnzgmulnz  42116  ringexp0nn  42117  aks6d1c5lem3  42120  aks6d1c5lem2  42121  deg1gprod  42123  deg1pow  42124  unitscyglem5  42182  domnexpgn0cl  42506  abvexp  42515  fidomncyc  42518  selvvvval  42568  evlselv  42570  mhphf  42580  mon1psubm  43182  deg1mhm  43183  amgm2d  44181  amgm3d  44182  amgm4d  44183  2zrngmmgm  48246  2zrngmsgrp  48247  2zrngnring  48252  cznrng  48255  cznnring  48256  mgpsumunsn  48355  invginvrid  48361  elmgpcntrd  48999  amgmlemALT  49798  amgmw2d  49799