Theorem mgpplusg 20077

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 6846	. . . 4 ⊢ · ∈ V
3		plusgid 17202	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17132	. . . 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 20076	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6835	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2787	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17114	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6824	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2781	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6824	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2781	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6836	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2795	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 182	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2113  Vcvv 3438  ∅c0 4283  ⟨cop 4584  ‘cfv 6490  (class class class)co 7356   sSet csts 17088  ndxcnx 17118  +_gcplusg 17175  ._rcmulr 17176  mulGrpcmgp 20073

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-1cn 11082  ax-addcl 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12144  df-2 12206  df-sets 17089  df-slot 17107  df-ndx 17119  df-plusg 17188  df-mgp 20074

This theorem is referenced by:  prdsmgp  20084  rngass  20092  rngcl  20097  isrngd  20106  rngpropd  20107  dfur2  20117  srgcl  20126  srgass  20127  srgideu  20128  srgidmlem  20134  issrgid  20137  srg1zr  20148  srgpcomp  20151  srgpcompp  20152  srgbinomlem4  20162  srgbinomlem  20163  csrgbinom  20165  ringcl  20183  crngcom  20184  iscrng2  20185  ringass  20186  ringideu  20187  ringidmlem  20201  isringid  20204  ringidss  20210  isringrng  20220  ringpropd  20221  crngpropd  20222  isringd  20224  iscrngd  20225  ring1  20243  gsummgp0  20251  pwspjmhmmgpd  20261  xpsring1d  20267  oppr1  20284  unitgrp  20317  unitlinv  20327  unitrinv  20328  rdivmuldivd  20347  rngidpropd  20349  invrpropd  20352  isrnghmmul  20376  dfrhm2  20408  rhmmul  20419  isrhm2d  20420  rhmunitinv  20442  rhmimasubrnglem  20496  rhmimasubrng  20497  cntzsubrng  20498  subrgugrp  20522  issubrg3  20531  cntzsubr  20537  rhmpropd  20540  isdomn3  20646  isdrng2  20674  drngmclOLD  20682  drngid2  20683  isdrngd  20696  isdrngdOLD  20698  cntzsdrg  20733  primefld  20736  rlmscaf  21157  rnglidlmmgm  21198  rnglidlmsgrp  21199  rng2idl1cntr  21258  xrsmcmn  21344  cnfldexp  21357  cnmsubglem  21383  expmhm  21389  nn0srg  21390  rge0srg  21391  expghm  21428  frobrhm  21528  psgnghm  21533  psgnco  21536  evpmodpmf1o  21549  sraassab  21821  sraassaOLD  21823  assamulgscmlem2  21854  psrcrng  21925  mplcoe3  21991  mplcoe5lem  21992  mplcoe5  21993  mplcoe2  21994  mplbas2  21995  evlslem1  22035  mpfind  22068  mhppwdeg  22091  psdpw  22111  coe1tm  22213  ply1coe  22240  ringvcl  22342  mamuvs2  22348  mat1mhm  22426  scmatmhm  22476  mdetdiaglem  22540  mdetrlin  22544  mdetrsca  22545  mdetralt  22550  mdetunilem7  22560  mdetuni0  22563  m2detleib  22573  invrvald  22618  mat2pmatmhm  22675  pm2mpmhm  22762  chfacfpmmulgsum2  22807  cpmadugsumlemB  22816  cnmpt1mulr  24124  cnmpt2mulr  24125  reefgim  26414  efabl  26513  efsubm  26514  amgm  26955  wilthlem2  27033  wilthlem3  27034  dchrelbas3  27203  dchrzrhmul  27211  dchrmulcl  27214  dchrn0  27215  dchrinvcl  27218  dchrptlem2  27230  dchrsum2  27233  sum2dchr  27239  lgseisenlem3  27342  lgseisenlem4  27343  zsoring  28367  urpropd  33262  ringm1expp1  33265  ringinvval  33266  dvrcan5  33267  isunit3  33272  elrgspnlem2  33274  elrgspnsubrunlem1  33278  elrgspnsubrunlem2  33279  0ringcring  33283  erler  33296  rlocaddval  33299  rlocmulval  33300  rloccring  33301  domnprodn0  33306  domnprodeq0  33307  rrgsubm  33315  unitprodclb  33419  elringlsm  33423  lsmsnpridl  33428  cringm4  33476  ssdifidlprm  33488  mxidlprm  33500  rprmdvdspow  33563  rprmdvdsprod  33564  1arithidomlem1  33565  1arithidom  33567  1arithufdlem2  33575  1arithufdlem3  33576  1arithufdlem4  33577  dfufd2lem  33579  zringfrac  33584  deg1prod  33613  vietalem  33684  srapwov  33694  assarrginv  33742  evls1fldgencl  33776  iistmd  34008  xrge0iifmhm  34045  xrge0pluscn  34046  pl1cn  34061  zrhcntr  34085  aks6d1c1p4  42304  evl1gprodd  42310  idomnnzpownz  42325  idomnnzgmulnz  42326  ringexp0nn  42327  aks6d1c5lem3  42330  aks6d1c5lem2  42331  deg1gprod  42333  deg1pow  42334  unitscyglem5  42392  domnexpgn0cl  42720  abvexp  42729  fidomncyc  42732  selvvvval  42770  evlselv  42772  mhphf  42782  mon1psubm  43383  deg1mhm  43384  amgm2d  44381  amgm3d  44382  amgm4d  44383  2zrngmmgm  48440  2zrngmsgrp  48441  2zrngnring  48446  cznrng  48449  cznnring  48450  mgpsumunsn  48549  invginvrid  48555  elmgpcntrd  49192  amgmlemALT  49990  amgmw2d  49991