Theorem mgpplusg 20104

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 6890	. . . 4 ⊢ · ∈ V
3		plusgid 17298	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17226	. . . 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 20103	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6879	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2788	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17208	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6868	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2782	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6868	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2782	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6880	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2796	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 182	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2108  Vcvv 3459  ∅c0 4308  ⟨cop 4607  ‘cfv 6531  (class class class)co 7405   sSet csts 17182  ndxcnx 17212  +_gcplusg 17271  ._rcmulr 17272  mulGrpcmgp 20100

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 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-cnex 11185  ax-1cn 11187  ax-addcl 11189

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7862  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-nn 12241  df-2 12303  df-sets 17183  df-slot 17201  df-ndx 17213  df-plusg 17284  df-mgp 20101

This theorem is referenced by:  prdsmgp  20111  rngass  20119  rngcl  20124  isrngd  20133  rngpropd  20134  dfur2  20144  srgcl  20153  srgass  20154  srgideu  20155  srgidmlem  20161  issrgid  20164  srg1zr  20175  srgpcomp  20178  srgpcompp  20179  srgbinomlem4  20189  srgbinomlem  20190  csrgbinom  20192  ringcl  20210  crngcom  20211  iscrng2  20212  ringass  20213  ringideu  20214  ringidmlem  20228  isringid  20231  ringidss  20237  isringrng  20247  ringpropd  20248  crngpropd  20249  isringd  20251  iscrngd  20252  ring1  20270  gsummgp0  20278  pwspjmhmmgpd  20288  xpsring1d  20293  oppr1  20310  unitgrp  20343  unitlinv  20353  unitrinv  20354  rdivmuldivd  20373  rngidpropd  20375  invrpropd  20378  isrnghmmul  20402  dfrhm2  20434  rhmmul  20446  isrhm2d  20447  rhmunitinv  20471  rhmimasubrnglem  20525  rhmimasubrng  20526  cntzsubrng  20527  subrgugrp  20551  issubrg3  20560  cntzsubr  20566  rhmpropd  20569  isdomn3  20675  isdrng2  20703  drngmclOLD  20711  drngid2  20712  isdrngd  20725  isdrngdOLD  20727  cntzsdrg  20762  primefld  20765  rlmscaf  21165  rnglidlmmgm  21206  rnglidlmsgrp  21207  rng2idl1cntr  21266  xrsmcmn  21354  cnfldexp  21367  cnmsubglem  21398  expmhm  21404  nn0srg  21405  rge0srg  21406  expghm  21436  frobrhm  21536  psgnghm  21540  psgnco  21543  evpmodpmf1o  21556  sraassab  21828  sraassaOLD  21830  assamulgscmlem2  21860  psrcrng  21932  mplcoe3  21996  mplcoe5lem  21997  mplcoe5  21998  mplcoe2  21999  mplbas2  22000  evlslem1  22040  mpfind  22065  mhppwdeg  22088  psdpw  22108  coe1tm  22210  ply1coe  22236  ringvcl  22338  mamuvs2  22344  mat1mhm  22422  scmatmhm  22472  mdetdiaglem  22536  mdetrlin  22540  mdetrsca  22541  mdetralt  22546  mdetunilem7  22556  mdetuni0  22559  m2detleib  22569  invrvald  22614  mat2pmatmhm  22671  pm2mpmhm  22758  chfacfpmmulgsum2  22803  cpmadugsumlemB  22812  cnmpt1mulr  24120  cnmpt2mulr  24121  reefgim  26412  efabl  26511  efsubm  26512  amgm  26953  wilthlem2  27031  wilthlem3  27032  dchrelbas3  27201  dchrzrhmul  27209  dchrmulcl  27212  dchrn0  27213  dchrinvcl  27216  dchrptlem2  27228  dchrsum2  27231  sum2dchr  27237  lgseisenlem3  27340  lgseisenlem4  27341  urpropd  33227  ringinvval  33230  dvrcan5  33231  isunit3  33236  elrgspnlem2  33238  elrgspnsubrunlem1  33242  elrgspnsubrunlem2  33243  0ringcring  33247  erler  33260  rlocaddval  33263  rlocmulval  33264  rloccring  33265  domnprodn0  33270  rrgsubm  33278  unitprodclb  33404  elringlsm  33408  lsmsnpridl  33413  cringm4  33461  ssdifidlprm  33473  mxidlprm  33485  rprmdvdspow  33548  rprmdvdsprod  33549  1arithidomlem1  33550  1arithidom  33552  1arithufdlem2  33560  1arithufdlem3  33561  1arithufdlem4  33562  dfufd2lem  33564  zringfrac  33569  assarrginv  33676  evls1fldgencl  33711  iistmd  33933  xrge0iifmhm  33970  xrge0pluscn  33971  pl1cn  33986  zrhcntr  34010  aks6d1c1p4  42124  evl1gprodd  42130  idomnnzpownz  42145  idomnnzgmulnz  42146  ringexp0nn  42147  aks6d1c5lem3  42150  aks6d1c5lem2  42151  deg1gprod  42153  deg1pow  42154  unitscyglem5  42212  domnexpgn0cl  42546  abvexp  42555  fidomncyc  42558  selvvvval  42608  evlselv  42610  mhphf  42620  mon1psubm  43223  deg1mhm  43224  amgm2d  44222  amgm3d  44223  amgm4d  44224  2zrngmmgm  48227  2zrngmsgrp  48228  2zrngnring  48233  cznrng  48236  cznnring  48237  mgpsumunsn  48336  invginvrid  48342  elmgpcntrd  48979  amgmlemALT  49667  amgmw2d  49668