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 6850	. . . 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 692	. . 3 ⊢ (𝑅 ∈ V → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
6		mgpval.1	. . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅)
7	6, 1	mgpval 20119	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6839	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2790	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17154	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6828	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2784	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6828	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2784	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6840	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2798	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 182	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1542   ∈ wcel 2114  Vcvv 3430  ∅c0 4274  ⟨cop 4574  ‘cfv 6494  (class class class)co 7362   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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684  ax-cnex 11089  ax-1cn 11091  ax-addcl 11093

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5521  df-eprel 5526  df-po 5534  df-so 5535  df-fr 5579  df-we 5581  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-pred 6261  df-ord 6322  df-on 6323  df-lim 6324  df-suc 6325  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7813  df-2nd 7938  df-frecs 8226  df-wrecs 8257  df-recs 8306  df-rdg 8344  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  20460  isrhm2d  20461  rhmunitinv  20483  rhmimasubrnglem  20537  rhmimasubrng  20538  cntzsubrng  20539  subrgugrp  20563  issubrg3  20572  cntzsubr  20578  rhmpropd  20581  isdomn3  20687  isdrng2  20715  drngmclOLD  20723  drngid2  20724  isdrngd  20737  isdrngdOLD  20739  cntzsdrg  20774  primefld  20777  rlmscaf  21198  rnglidlmmgm  21239  rnglidlmsgrp  21240  rng2idl1cntr  21299  xrsmcmn  21385  cnfldexp  21398  cnmsubglem  21424  expmhm  21430  nn0srg  21431  rge0srg  21432  expghm  21469  frobrhm  21569  psgnghm  21574  psgnco  21577  evpmodpmf1o  21590  sraassab  21862  assamulgscmlem2  21894  psrcrng  21964  mplcoe3  22030  mplcoe5lem  22031  mplcoe5  22032  mplcoe2  22033  mplbas2  22034  evlslem1  22074  mpfind  22107  mhppwdeg  22130  psdpw  22150  coe1tm  22252  ply1coe  22277  ringvcl  22379  mamuvs2  22385  mat1mhm  22463  scmatmhm  22513  mdetdiaglem  22577  mdetrlin  22581  mdetrsca  22582  mdetralt  22587  mdetunilem7  22597  mdetuni0  22600  m2detleib  22610  invrvald  22655  mat2pmatmhm  22712  pm2mpmhm  22799  chfacfpmmulgsum2  22844  cpmadugsumlemB  22853  cnmpt1mulr  24161  cnmpt2mulr  24162  reefgim  26432  efabl  26531  efsubm  26532  amgm  26972  wilthlem2  27050  wilthlem3  27051  dchrelbas3  27219  dchrzrhmul  27227  dchrmulcl  27230  dchrn0  27231  dchrinvcl  27234  dchrptlem2  27246  dchrsum2  27249  sum2dchr  27255  lgseisenlem3  27358  lgseisenlem4  27359  zsoring  28419  urpropd  33311  ringm1expp1  33314  ringinvval  33315  dvrcan5  33316  isunit3  33321  elrgspnlem2  33323  elrgspnsubrunlem1  33327  elrgspnsubrunlem2  33328  0ringcring  33332  erler  33345  rlocaddval  33348  rlocmulval  33349  rloccring  33350  domnprodn0  33355  domnprodeq0  33356  rrgsubm  33364  unitprodclb  33468  elringlsm  33472  lsmsnpridl  33477  cringm4  33525  ssdifidlprm  33537  mxidlprm  33549  rprmdvdspow  33612  rprmdvdsprod  33613  1arithidomlem1  33614  1arithidom  33616  1arithufdlem2  33624  1arithufdlem3  33625  1arithufdlem4  33626  dfufd2lem  33628  zringfrac  33633  deg1prod  33662  psrmonprod  33715  mplmonprod  33717  vietalem  33742  srapwov  33752  assarrginv  33800  evls1fldgencl  33834  iistmd  34066  xrge0iifmhm  34103  xrge0pluscn  34104  pl1cn  34119  zrhcntr  34143  aks6d1c1p4  42570  evl1gprodd  42576  idomnnzpownz  42591  idomnnzgmulnz  42592  ringexp0nn  42593  aks6d1c5lem3  42596  aks6d1c5lem2  42597  deg1gprod  42599  deg1pow  42600  unitscyglem5  42658  domnexpgn0cl  42988  abvexp  42997  fidomncyc  43000  selvvvval  43038  evlselv  43040  mhphf  43050  mon1psubm  43651  deg1mhm  43652  amgm2d  44649  amgm3d  44650  amgm4d  44651  2zrngmmgm  48746  2zrngmsgrp  48747  2zrngnring  48752  cznrng  48755  cznnring  48756  mgpsumunsn  48855  invginvrid  48861  elmgpcntrd  49498  amgmlemALT  50296  amgmw2d  50297