Theorem mgpplusg 20278

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 6896	. . . 4 ⊢ · ∈ V
3		plusgid 17373	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17303	. . . 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 20277	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6885	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2815	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17285	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6874	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2809	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6874	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2809	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6886	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2823	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 184	1 ⊢ · = (+g‘𝑀)

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2145  Vcvv 3453  ∅c0 4282  ⟨cop 4593  ‘cfv 6537  (class class class)co 7416   sSet csts 17259  ndxcnx 17289  +_gcplusg 17346  ._rcmulr 17347  mulGrpcmgp 20274

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-cnex 11183  ax-1cn 11185  ax-addcl 11187

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7866  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-nn 12261  df-2 12330  df-sets 17260  df-slot 17278  df-ndx 17290  df-plusg 17359  df-mgp 20275

This theorem is used by:  prdsmgp  20285  elmgplsm  20286  rngass  20295  rngcl  20300  isrngd  20309  rngpropd  20310  rng1zrlem  20317  dfur2  20324  srgcl  20333  srgass  20334  srgideu  20335  srgidmlem  20341  issrgid  20344  srgpcomp  20358  srgpcompp  20359  srgbinomlem4  20369  srgbinomlem  20370  csrgbinom  20372  ringcl  20390  crngcom  20391  iscrng2  20392  ringass  20393  ringideu  20394  ringidmlem  20410  isringid  20413  ringidss  20419  isringrng  20429  ringpropd  20431  crngpropd  20432  isringd  20434  iscrngd  20435  ring1  20453  gsummgp0  20459  pwspjmhmmgpd  20469  xpsring1d  20475  oppr1  20492  unitgrp  20525  unitlinv  20535  unitrinv  20536  rdivmuldivd  20555  rngidpropd  20557  invrpropd  20560  isrnghmmul  20584  dfrhm2  20616  rhmmul  20632  isrhm2d  20633  rhmunitinv  20672  rhmimasubrnglem  20728  rhmimasubrng  20729  cntzsubrng  20730  subrgugrp  20754  issubrg3  20763  cntzsubr  20769  rhmpropd  20772  isdomn3  20877  isdrng2  20907  isdrng3lem1  20915  isdrng3lem2  20916  drngid2  20920  isdrngd  20932  isdrngdOLD  20934  cntzsdrg  20969  primefld  20972  rlmscaf  21392  rnglidlmmgm  21443  rnglidlmsgrp  21444  rng2idl1cntr  21509  cringm4  21535  ssdifidlprm  21550  prmidlsubm  21551  xrsmcmn  21609  cnfldexp  21619  cnmsubglem  21644  expmhm  21650  nn0srg  21651  rge0srg  21652  expghm  21689  frobrhm  21789  psgnghm  21794  psgnco  21797  evpmodpmf1o  21810  sraassab  22084  assamulgscmlem2  22116  psrcrng  22187  mplcoe3  22255  mplcoe5lem  22256  mplcoe5  22257  mplcoe2  22258  mplbas2  22259  evlslem1  22299  mpfind  22332  selvvvval  22359  mhppwdeg  22379  psdpw  22399  coe1tm  22500  ply1coe  22524  ringvcl  22623  mamuvs2  22629  mat1mhm  22707  scmatmhm  22757  mdetdiaglem  22821  mdetrlin  22825  mdetrsca  22826  mdetralt  22831  mdetunilem7  22841  mdetuni0  22844  m2detleib  22854  invrvald  22899  mat2pmatmhm  22959  pm2mpmhm  23046  chfacfpmmulgsum2  23091  cpmadugsumlemB  23100  cnmpt1mulr  24409  cnmpt2mulr  24410  reefgim  26683  efabl  26785  efsubm  26786  amgm  27225  wilthlem2  27303  wilthlem3  27304  dchrelbas3  27472  dchrzrhmul  27480  dchrmulcl  27483  dchrn0  27484  dchrinvcl  27487  dchrptlem2  27499  dchrsum2  27502  sum2dchr  27508  lgseisenlem3  27611  lgseisenlem4  27612  zsoring  28672  urpropd  33657  ringm1expp1  33660  ringinvval  33661  dvrcan5  33662  isunit3  33667  elrgspnlem2  33670  elrgspnsubrunlem1  33674  elrgspnsubrunlem2  33675  0ringcring  33679  erler  33692  rlocaddval  33696  rlocmulval  33697  rloccring  33698  rlocisunit  33703  domnprodn0  33705  domnprodeq0  33706  rrgsubm  33711  unitprodclb  33809  lsmsnpridl  33816  mxidlprm  33860  rprmdvdspow  33930  rprmdvdsprod  33931  1arithidomlem1  33932  1arithidom  33934  1arithufdlem2  33942  1arithufdlem3  33943  1arithufdlem4  33944  dfufd2lem  33946  zringfrac  33951  deg1prod  33980  psrmonprod  34049  mplmonprod  34051  vietalem  34076  srapwov  34086  assarrginv  34133  evls1fldgencl  34167  iistmd  34399  xrge0iifmhm  34436  xrge0pluscn  34437  pl1cn  34452  zrhcntr  34476  aks6d1c1p4  42964  evl1gprodd  42970  idomnnzpownz  42985  idomnnzgmulnz  42986  ringexp0nn  42987  aks6d1c5lem3  42990  aks6d1c5lem2  42991  deg1gprod  42993  deg1pow  42994  unitscyglem5  43052  domnexpgn0cl  43392  abvexp  43401  fidomncyc  43404  evlselv  43422  mhphf  43430  mon1psubm  44027  deg1mhm  44028  amgm2d  45025  amgm3d  45026  amgm4d  45027  2zrngmmgm  49154  2zrngmsgrp  49155  2zrngnring  49160  cznrng  49163  cznnring  49164  mgpsumunsn  49278  invginvrid  49284  elmgpcntrd  49918  amgmlemALT  50808  amgmw2d  50809