Theorem mgpplusg 20155

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 17241	. . . 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 20154	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6909	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2792	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17222	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6898	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2786	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6898	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2786	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6910	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2800	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 182	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1536   ∈ wcel 2105  Vcvv 3477  ∅c0 4338  ⟨cop 4636  ‘cfv 6562  (class class class)co 7430   sSet csts 17196  ndxcnx 17226  +_gcplusg 17297  ._rcmulr 17298  mulGrpcmgp 20151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-1cn 11210  ax-addcl 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-nn 12264  df-2 12326  df-sets 17197  df-slot 17215  df-ndx 17227  df-plusg 17310  df-mgp 20152

This theorem is referenced by:  prdsmgp  20168  rngass  20176  rngcl  20181  isrngd  20190  rngpropd  20191  dfur2  20201  srgcl  20210  srgass  20211  srgideu  20212  srgidmlem  20218  issrgid  20221  srg1zr  20232  srgpcomp  20235  srgpcompp  20236  srgbinomlem4  20246  srgbinomlem  20247  csrgbinom  20249  ringcl  20267  crngcom  20268  iscrng2  20269  ringass  20270  ringideu  20271  ringidmlem  20281  isringid  20284  ringidss  20290  isringrng  20300  ringpropd  20301  crngpropd  20302  isringd  20304  iscrngd  20305  ring1  20323  gsummgp0  20331  pwspjmhmmgpd  20341  xpsring1d  20346  oppr1  20366  unitgrp  20399  unitlinv  20409  unitrinv  20410  rdivmuldivd  20429  rngidpropd  20431  invrpropd  20434  isrnghmmul  20458  dfrhm2  20490  rhmmul  20502  isrhm2d  20503  rhmunitinv  20527  rhmimasubrnglem  20581  rhmimasubrng  20582  cntzsubrng  20583  subrgugrp  20607  issubrg3  20616  cntzsubr  20622  rhmpropd  20625  isdomn3  20731  isdrng2  20759  drngmclOLD  20767  drngid2  20768  isdrngd  20781  isdrngdOLD  20783  cntzsdrg  20819  primefld  20822  rlmscaf  21231  rnglidlmmgm  21272  rnglidlmsgrp  21273  rng2idl1cntr  21332  xrsmcmn  21421  cnfldexp  21434  cnmsubglem  21465  expmhm  21471  nn0srg  21472  rge0srg  21473  expghm  21503  frobrhm  21611  psgnghm  21615  psgnco  21618  evpmodpmf1o  21631  sraassab  21905  sraassaOLD  21907  assamulgscmlem2  21937  psrcrng  22009  mplcoe3  22073  mplcoe5lem  22074  mplcoe5  22075  mplcoe2  22076  mplbas2  22077  evlslem1  22123  mpfind  22148  mhppwdeg  22171  coe1tm  22291  ply1coe  22317  ringvcl  22419  mamuvs2  22425  mat1mhm  22505  scmatmhm  22555  mdetdiaglem  22619  mdetrlin  22623  mdetrsca  22624  mdetralt  22629  mdetunilem7  22639  mdetuni0  22642  m2detleib  22652  invrvald  22697  mat2pmatmhm  22754  pm2mpmhm  22841  chfacfpmmulgsum2  22886  cpmadugsumlemB  22895  cnmpt1mulr  24205  cnmpt2mulr  24206  reefgim  26508  efabl  26606  efsubm  26607  amgm  27048  wilthlem2  27126  wilthlem3  27127  dchrelbas3  27296  dchrzrhmul  27304  dchrmulcl  27307  dchrn0  27308  dchrinvcl  27311  dchrptlem2  27323  dchrsum2  27326  sum2dchr  27332  lgseisenlem3  27435  lgseisenlem4  27436  urpropd  33221  ringinvval  33224  dvrcan5  33225  isunit3  33230  elrgspnlem2  33232  0ringcring  33238  erler  33251  rlocaddval  33254  rlocmulval  33255  rloccring  33256  domnprodn0  33261  rrgsubm  33267  unitprodclb  33396  elringlsm  33400  lsmsnpridl  33405  cringm4  33453  ssdifidlprm  33465  mxidlprm  33477  rprmdvdspow  33540  rprmdvdsprod  33541  1arithidomlem1  33542  1arithidom  33544  1arithufdlem2  33552  1arithufdlem3  33553  1arithufdlem4  33554  dfufd2lem  33556  zringfrac  33561  assarrginv  33663  evls1fldgencl  33694  iistmd  33862  xrge0iifmhm  33899  xrge0pluscn  33900  pl1cn  33915  zrhcntr  33941  aks6d1c1p4  42092  evl1gprodd  42098  idomnnzpownz  42113  idomnnzgmulnz  42114  ringexp0nn  42115  aks6d1c5lem3  42118  aks6d1c5lem2  42119  deg1gprod  42121  deg1pow  42122  unitscyglem5  42180  domnexpgn0cl  42509  abvexp  42518  fidomncyc  42521  selvvvval  42571  evlselv  42573  mhphf  42583  mon1psubm  43187  deg1mhm  43188  amgm2d  44187  amgm3d  44188  amgm4d  44189  2zrngmmgm  48095  2zrngmsgrp  48096  2zrngnring  48101  cznrng  48104  cznnring  48105  mgpsumunsn  48205  invginvrid  48211  elmgpcntrd  48793  amgmlemALT  49033  amgmw2d  49034