Theorem mgpplusg 20083

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 6849	. . . 4 ⊢ · ∈ V
3		plusgid 17208	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17138	. . . 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 20082	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6838	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2790	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17120	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6827	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2784	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6827	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2784	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6839	. . 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 3441  ∅c0 4286  ⟨cop 4587  ‘cfv 6493  (class class class)co 7360   sSet csts 17094  ndxcnx 17124  +_gcplusg 17181  ._rcmulr 17182  mulGrpcmgp 20079

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 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-cnex 11086  ax-1cn 11088  ax-addcl 11090

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 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  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 12150  df-2 12212  df-sets 17095  df-slot 17113  df-ndx 17125  df-plusg 17194  df-mgp 20080

This theorem is referenced by:  prdsmgp  20090  rngass  20098  rngcl  20103  isrngd  20112  rngpropd  20113  dfur2  20123  srgcl  20132  srgass  20133  srgideu  20134  srgidmlem  20140  issrgid  20143  srg1zr  20154  srgpcomp  20157  srgpcompp  20158  srgbinomlem4  20168  srgbinomlem  20169  csrgbinom  20171  ringcl  20189  crngcom  20190  iscrng2  20191  ringass  20192  ringideu  20193  ringidmlem  20207  isringid  20210  ringidss  20216  isringrng  20226  ringpropd  20227  crngpropd  20228  isringd  20230  iscrngd  20231  ring1  20249  gsummgp0  20257  pwspjmhmmgpd  20267  xpsring1d  20273  oppr1  20290  unitgrp  20323  unitlinv  20333  unitrinv  20334  rdivmuldivd  20353  rngidpropd  20355  invrpropd  20358  isrnghmmul  20382  dfrhm2  20414  rhmmul  20425  isrhm2d  20426  rhmunitinv  20448  rhmimasubrnglem  20502  rhmimasubrng  20503  cntzsubrng  20504  subrgugrp  20528  issubrg3  20537  cntzsubr  20543  rhmpropd  20546  isdomn3  20652  isdrng2  20680  drngmclOLD  20688  drngid2  20689  isdrngd  20702  isdrngdOLD  20704  cntzsdrg  20739  primefld  20742  rlmscaf  21163  rnglidlmmgm  21204  rnglidlmsgrp  21205  rng2idl1cntr  21264  xrsmcmn  21350  cnfldexp  21363  cnmsubglem  21389  expmhm  21395  nn0srg  21396  rge0srg  21397  expghm  21434  frobrhm  21534  psgnghm  21539  psgnco  21542  evpmodpmf1o  21555  sraassab  21827  sraassaOLD  21829  assamulgscmlem2  21860  psrcrng  21931  mplcoe3  21997  mplcoe5lem  21998  mplcoe5  21999  mplcoe2  22000  mplbas2  22001  evlslem1  22041  mpfind  22074  mhppwdeg  22097  psdpw  22117  coe1tm  22219  ply1coe  22246  ringvcl  22348  mamuvs2  22354  mat1mhm  22432  scmatmhm  22482  mdetdiaglem  22546  mdetrlin  22550  mdetrsca  22551  mdetralt  22556  mdetunilem7  22566  mdetuni0  22569  m2detleib  22579  invrvald  22624  mat2pmatmhm  22681  pm2mpmhm  22768  chfacfpmmulgsum2  22813  cpmadugsumlemB  22822  cnmpt1mulr  24130  cnmpt2mulr  24131  reefgim  26420  efabl  26519  efsubm  26520  amgm  26961  wilthlem2  27039  wilthlem3  27040  dchrelbas3  27209  dchrzrhmul  27217  dchrmulcl  27220  dchrn0  27221  dchrinvcl  27224  dchrptlem2  27236  dchrsum2  27239  sum2dchr  27245  lgseisenlem3  27348  lgseisenlem4  27349  zsoring  28409  urpropd  33315  ringm1expp1  33318  ringinvval  33319  dvrcan5  33320  isunit3  33325  elrgspnlem2  33327  elrgspnsubrunlem1  33331  elrgspnsubrunlem2  33332  0ringcring  33336  erler  33349  rlocaddval  33352  rlocmulval  33353  rloccring  33354  domnprodn0  33359  domnprodeq0  33360  rrgsubm  33368  unitprodclb  33472  elringlsm  33476  lsmsnpridl  33481  cringm4  33529  ssdifidlprm  33541  mxidlprm  33553  rprmdvdspow  33616  rprmdvdsprod  33617  1arithidomlem1  33618  1arithidom  33620  1arithufdlem2  33628  1arithufdlem3  33629  1arithufdlem4  33630  dfufd2lem  33632  zringfrac  33637  deg1prod  33666  vietalem  33737  srapwov  33747  assarrginv  33795  evls1fldgencl  33829  iistmd  34061  xrge0iifmhm  34098  xrge0pluscn  34099  pl1cn  34114  zrhcntr  34138  aks6d1c1p4  42433  evl1gprodd  42439  idomnnzpownz  42454  idomnnzgmulnz  42455  ringexp0nn  42456  aks6d1c5lem3  42459  aks6d1c5lem2  42460  deg1gprod  42462  deg1pow  42463  unitscyglem5  42521  domnexpgn0cl  42845  abvexp  42854  fidomncyc  42857  selvvvval  42895  evlselv  42897  mhphf  42907  mon1psubm  43508  deg1mhm  43509  amgm2d  44506  amgm3d  44507  amgm4d  44508  2zrngmmgm  48565  2zrngmsgrp  48566  2zrngnring  48571  cznrng  48574  cznnring  48575  mgpsumunsn  48674  invginvrid  48680  elmgpcntrd  49317  amgmlemALT  50115  amgmw2d  50116