Theorem mgpplusg 20141

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 6920	. . . 4 ⊢ · ∈ V
3		plusgid 17324	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17244	. . . 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 20140	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6909	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2795	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17226	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6898	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2789	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6898	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2789	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6910	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2803	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 182	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2108  Vcvv 3480  ∅c0 4333  ⟨cop 4632  ‘cfv 6561  (class class class)co 7431   sSet csts 17200  ndxcnx 17230  +_gcplusg 17297  ._rcmulr 17298  mulGrpcmgp 20137

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-1cn 11213  ax-addcl 11215

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267  df-2 12329  df-sets 17201  df-slot 17219  df-ndx 17231  df-plusg 17310  df-mgp 20138

This theorem is referenced by:  prdsmgp  20148  rngass  20156  rngcl  20161  isrngd  20170  rngpropd  20171  dfur2  20181  srgcl  20190  srgass  20191  srgideu  20192  srgidmlem  20198  issrgid  20201  srg1zr  20212  srgpcomp  20215  srgpcompp  20216  srgbinomlem4  20226  srgbinomlem  20227  csrgbinom  20229  ringcl  20247  crngcom  20248  iscrng2  20249  ringass  20250  ringideu  20251  ringidmlem  20265  isringid  20268  ringidss  20274  isringrng  20284  ringpropd  20285  crngpropd  20286  isringd  20288  iscrngd  20289  ring1  20307  gsummgp0  20315  pwspjmhmmgpd  20325  xpsring1d  20330  oppr1  20350  unitgrp  20383  unitlinv  20393  unitrinv  20394  rdivmuldivd  20413  rngidpropd  20415  invrpropd  20418  isrnghmmul  20442  dfrhm2  20474  rhmmul  20486  isrhm2d  20487  rhmunitinv  20511  rhmimasubrnglem  20565  rhmimasubrng  20566  cntzsubrng  20567  subrgugrp  20591  issubrg3  20600  cntzsubr  20606  rhmpropd  20609  isdomn3  20715  isdrng2  20743  drngmclOLD  20751  drngid2  20752  isdrngd  20765  isdrngdOLD  20767  cntzsdrg  20803  primefld  20806  rlmscaf  21214  rnglidlmmgm  21255  rnglidlmsgrp  21256  rng2idl1cntr  21315  xrsmcmn  21404  cnfldexp  21417  cnmsubglem  21448  expmhm  21454  nn0srg  21455  rge0srg  21456  expghm  21486  frobrhm  21594  psgnghm  21598  psgnco  21601  evpmodpmf1o  21614  sraassab  21888  sraassaOLD  21890  assamulgscmlem2  21920  psrcrng  21992  mplcoe3  22056  mplcoe5lem  22057  mplcoe5  22058  mplcoe2  22059  mplbas2  22060  evlslem1  22106  mpfind  22131  mhppwdeg  22154  psdpw  22174  coe1tm  22276  ply1coe  22302  ringvcl  22404  mamuvs2  22410  mat1mhm  22490  scmatmhm  22540  mdetdiaglem  22604  mdetrlin  22608  mdetrsca  22609  mdetralt  22614  mdetunilem7  22624  mdetuni0  22627  m2detleib  22637  invrvald  22682  mat2pmatmhm  22739  pm2mpmhm  22826  chfacfpmmulgsum2  22871  cpmadugsumlemB  22880  cnmpt1mulr  24190  cnmpt2mulr  24191  reefgim  26494  efabl  26592  efsubm  26593  amgm  27034  wilthlem2  27112  wilthlem3  27113  dchrelbas3  27282  dchrzrhmul  27290  dchrmulcl  27293  dchrn0  27294  dchrinvcl  27297  dchrptlem2  27309  dchrsum2  27312  sum2dchr  27318  lgseisenlem3  27421  lgseisenlem4  27422  urpropd  33236  ringinvval  33239  dvrcan5  33240  isunit3  33245  elrgspnlem2  33247  elrgspnsubrunlem1  33251  elrgspnsubrunlem2  33252  0ringcring  33256  erler  33269  rlocaddval  33272  rlocmulval  33273  rloccring  33274  domnprodn0  33279  rrgsubm  33287  unitprodclb  33417  elringlsm  33421  lsmsnpridl  33426  cringm4  33474  ssdifidlprm  33486  mxidlprm  33498  rprmdvdspow  33561  rprmdvdsprod  33562  1arithidomlem1  33563  1arithidom  33565  1arithufdlem2  33573  1arithufdlem3  33574  1arithufdlem4  33575  dfufd2lem  33577  zringfrac  33582  assarrginv  33687  evls1fldgencl  33720  iistmd  33901  xrge0iifmhm  33938  xrge0pluscn  33939  pl1cn  33954  zrhcntr  33980  aks6d1c1p4  42112  evl1gprodd  42118  idomnnzpownz  42133  idomnnzgmulnz  42134  ringexp0nn  42135  aks6d1c5lem3  42138  aks6d1c5lem2  42139  deg1gprod  42141  deg1pow  42142  unitscyglem5  42200  domnexpgn0cl  42533  abvexp  42542  fidomncyc  42545  selvvvval  42595  evlselv  42597  mhphf  42607  mon1psubm  43211  deg1mhm  43212  amgm2d  44211  amgm3d  44212  amgm4d  44213  2zrngmmgm  48168  2zrngmsgrp  48169  2zrngnring  48174  cznrng  48177  cznnring  48178  mgpsumunsn  48277  invginvrid  48283  elmgpcntrd  48894  amgmlemALT  49322  amgmw2d  49323