Theorem mgpplusg 20120

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 6845	. . . 4 ⊢ · ∈ V
3		plusgid 17242	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17172	. . . 4 ⊢ ((𝑅 ∈ V ∧ · ∈ V) → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
5	2, 4	mpan2 698	. . 3 ⊢ (𝑅 ∈ V → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
6		mgpval.1	. . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅)
7	6, 1	mgpval 20119	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6834	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2794	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17154	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6823	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2788	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6823	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2788	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6835	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2802	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 183	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1548   ∈ wcel 2121  Vcvv 3433  ∅c0 4264  ⟨cop 4564  ‘cfv 6489  (class class class)co 7360   sSet csts 17128  ndxcnx 17158  +_gcplusg 17215  ._rcmulr 17216  mulGrpcmgp 20116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-cnex 11089  ax-1cn 11091  ax-addcl 11093

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-nn 12170  df-2 12239  df-sets 17129  df-slot 17147  df-ndx 17159  df-plusg 17228  df-mgp 20117

This theorem is referenced by:  prdsmgp  20127  rngass  20135  rngcl  20140  isrngd  20149  rngpropd  20150  dfur2  20160  srgcl  20169  srgass  20170  srgideu  20171  srgidmlem  20177  issrgid  20180  srg1zr  20191  srgpcomp  20194  srgpcompp  20195  srgbinomlem4  20205  srgbinomlem  20206  csrgbinom  20208  ringcl  20226  crngcom  20227  iscrng2  20228  ringass  20229  ringideu  20230  ringidmlem  20244  isringid  20247  ringidss  20253  isringrng  20263  ringpropd  20264  crngpropd  20265  isringd  20267  iscrngd  20268  ring1  20286  gsummgp0  20292  pwspjmhmmgpd  20302  xpsring1d  20308  oppr1  20325  unitgrp  20358  unitlinv  20368  unitrinv  20369  rdivmuldivd  20388  rngidpropd  20390  invrpropd  20393  isrnghmmul  20417  dfrhm2  20449  rhmmul  20461  isrhm2d  20462  rhmunitinv  20487  rhmimasubrnglem  20541  rhmimasubrng  20542  cntzsubrng  20543  subrgugrp  20567  issubrg3  20576  cntzsubr  20582  rhmpropd  20585  isdomn3  20691  isdrng2  20719  drngmclOLD  20727  drngid2  20728  isdrngd  20741  isdrngdOLD  20743  cntzsdrg  20778  primefld  20781  rlmscaf  21201  rnglidlmmgm  21242  rnglidlmsgrp  21243  rng2idl1cntr  21302  xrsmcmn  21374  cnfldexp  21384  cnmsubglem  21409  expmhm  21415  nn0srg  21416  rge0srg  21417  expghm  21454  frobrhm  21554  psgnghm  21559  psgnco  21562  evpmodpmf1o  21575  sraassab  21847  assamulgscmlem2  21879  psrcrng  21950  mplcoe3  22018  mplcoe5lem  22019  mplcoe5  22020  mplcoe2  22021  mplbas2  22022  evlslem1  22062  mpfind  22095  selvvvval  22122  mhppwdeg  22142  psdpw  22162  coe1tm  22263  ply1coe  22288  ringvcl  22387  mamuvs2  22393  mat1mhm  22471  scmatmhm  22521  mdetdiaglem  22585  mdetrlin  22589  mdetrsca  22590  mdetralt  22595  mdetunilem7  22605  mdetuni0  22608  m2detleib  22618  invrvald  22663  mat2pmatmhm  22720  pm2mpmhm  22807  chfacfpmmulgsum2  22852  cpmadugsumlemB  22861  cnmpt1mulr  24169  cnmpt2mulr  24170  reefgim  26437  efabl  26536  efsubm  26537  amgm  26976  wilthlem2  27054  wilthlem3  27055  dchrelbas3  27223  dchrzrhmul  27231  dchrmulcl  27234  dchrn0  27235  dchrinvcl  27238  dchrptlem2  27250  dchrsum2  27253  sum2dchr  27259  lgseisenlem3  27362  lgseisenlem4  27363  zsoring  28423  urpropd  33316  ringm1expp1  33319  ringinvval  33320  dvrcan5  33321  isunit3  33326  elrgspnlem2  33328  elrgspnsubrunlem1  33332  elrgspnsubrunlem2  33333  0ringcring  33337  erler  33350  rlocaddval  33353  rlocmulval  33354  rloccring  33355  domnprodn0  33360  domnprodeq0  33361  rrgsubm  33369  unitprodclb  33476  elringlsm  33480  lsmsnpridl  33485  cringm4  33533  ssdifidlprm  33545  mxidlprm  33557  rprmdvdspow  33628  rprmdvdsprod  33629  1arithidomlem1  33630  1arithidom  33632  1arithufdlem2  33640  1arithufdlem3  33641  1arithufdlem4  33642  dfufd2lem  33644  zringfrac  33649  deg1prod  33678  psrmonprod  33748  mplmonprod  33750  vietalem  33775  srapwov  33785  assarrginv  33832  evls1fldgencl  33866  iistmd  34098  xrge0iifmhm  34135  xrge0pluscn  34136  pl1cn  34151  zrhcntr  34175  aks6d1c1p4  42611  evl1gprodd  42617  idomnnzpownz  42632  idomnnzgmulnz  42633  ringexp0nn  42634  aks6d1c5lem3  42637  aks6d1c5lem2  42638  deg1gprod  42640  deg1pow  42641  unitscyglem5  42699  domnexpgn0cl  43024  abvexp  43033  fidomncyc  43036  evlselv  43054  mhphf  43062  mon1psubm  43659  deg1mhm  43660  amgm2d  44657  amgm3d  44658  amgm4d  44659  2zrngmmgm  48757  2zrngmsgrp  48758  2zrngnring  48763  cznrng  48766  cznnring  48767  mgpsumunsn  48866  invginvrid  48872  elmgpcntrd  49509  amgmlemALT  50307  amgmw2d  50308