Theorem mgpplusg 20062

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 6836	. . . 4 ⊢ · ∈ V
3		plusgid 17188	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17118	. . . 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 20061	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6825	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2784	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17100	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6814	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2778	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6814	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2778	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6826	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2792	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 182	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2111  Vcvv 3436  ∅c0 4280  ⟨cop 4579  ‘cfv 6481  (class class class)co 7346   sSet csts 17074  ndxcnx 17104  +_gcplusg 17161  ._rcmulr 17162  mulGrpcmgp 20058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-cnex 11062  ax-1cn 11064  ax-addcl 11066

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-nn 12126  df-2 12188  df-sets 17075  df-slot 17093  df-ndx 17105  df-plusg 17174  df-mgp 20059

This theorem is referenced by:  prdsmgp  20069  rngass  20077  rngcl  20082  isrngd  20091  rngpropd  20092  dfur2  20102  srgcl  20111  srgass  20112  srgideu  20113  srgidmlem  20119  issrgid  20122  srg1zr  20133  srgpcomp  20136  srgpcompp  20137  srgbinomlem4  20147  srgbinomlem  20148  csrgbinom  20150  ringcl  20168  crngcom  20169  iscrng2  20170  ringass  20171  ringideu  20172  ringidmlem  20186  isringid  20189  ringidss  20195  isringrng  20205  ringpropd  20206  crngpropd  20207  isringd  20209  iscrngd  20210  ring1  20228  gsummgp0  20236  pwspjmhmmgpd  20246  xpsring1d  20251  oppr1  20268  unitgrp  20301  unitlinv  20311  unitrinv  20312  rdivmuldivd  20331  rngidpropd  20333  invrpropd  20336  isrnghmmul  20360  dfrhm2  20392  rhmmul  20403  isrhm2d  20404  rhmunitinv  20426  rhmimasubrnglem  20480  rhmimasubrng  20481  cntzsubrng  20482  subrgugrp  20506  issubrg3  20515  cntzsubr  20521  rhmpropd  20524  isdomn3  20630  isdrng2  20658  drngmclOLD  20666  drngid2  20667  isdrngd  20680  isdrngdOLD  20682  cntzsdrg  20717  primefld  20720  rlmscaf  21141  rnglidlmmgm  21182  rnglidlmsgrp  21183  rng2idl1cntr  21242  xrsmcmn  21328  cnfldexp  21341  cnmsubglem  21367  expmhm  21373  nn0srg  21374  rge0srg  21375  expghm  21412  frobrhm  21512  psgnghm  21517  psgnco  21520  evpmodpmf1o  21533  sraassab  21805  sraassaOLD  21807  assamulgscmlem2  21837  psrcrng  21909  mplcoe3  21973  mplcoe5lem  21974  mplcoe5  21975  mplcoe2  21976  mplbas2  21977  evlslem1  22017  mpfind  22042  mhppwdeg  22065  psdpw  22085  coe1tm  22187  ply1coe  22213  ringvcl  22315  mamuvs2  22321  mat1mhm  22399  scmatmhm  22449  mdetdiaglem  22513  mdetrlin  22517  mdetrsca  22518  mdetralt  22523  mdetunilem7  22533  mdetuni0  22536  m2detleib  22546  invrvald  22591  mat2pmatmhm  22648  pm2mpmhm  22735  chfacfpmmulgsum2  22780  cpmadugsumlemB  22789  cnmpt1mulr  24097  cnmpt2mulr  24098  reefgim  26387  efabl  26486  efsubm  26487  amgm  26928  wilthlem2  27006  wilthlem3  27007  dchrelbas3  27176  dchrzrhmul  27184  dchrmulcl  27187  dchrn0  27188  dchrinvcl  27191  dchrptlem2  27203  dchrsum2  27206  sum2dchr  27212  lgseisenlem3  27315  lgseisenlem4  27316  zsoring  28332  urpropd  33199  ringinvval  33202  dvrcan5  33203  isunit3  33208  elrgspnlem2  33210  elrgspnsubrunlem1  33214  elrgspnsubrunlem2  33215  0ringcring  33219  erler  33232  rlocaddval  33235  rlocmulval  33236  rloccring  33237  domnprodn0  33242  rrgsubm  33250  unitprodclb  33354  elringlsm  33358  lsmsnpridl  33363  cringm4  33411  ssdifidlprm  33423  mxidlprm  33435  rprmdvdspow  33498  rprmdvdsprod  33499  1arithidomlem1  33500  1arithidom  33502  1arithufdlem2  33510  1arithufdlem3  33511  1arithufdlem4  33512  dfufd2lem  33514  zringfrac  33519  srapwov  33601  assarrginv  33649  evls1fldgencl  33683  iistmd  33915  xrge0iifmhm  33952  xrge0pluscn  33953  pl1cn  33968  zrhcntr  33992  aks6d1c1p4  42203  evl1gprodd  42209  idomnnzpownz  42224  idomnnzgmulnz  42225  ringexp0nn  42226  aks6d1c5lem3  42229  aks6d1c5lem2  42230  deg1gprod  42232  deg1pow  42233  unitscyglem5  42291  domnexpgn0cl  42615  abvexp  42624  fidomncyc  42627  selvvvval  42677  evlselv  42679  mhphf  42689  mon1psubm  43291  deg1mhm  43292  amgm2d  44290  amgm3d  44291  amgm4d  44292  2zrngmmgm  48351  2zrngmsgrp  48352  2zrngnring  48357  cznrng  48360  cznnring  48361  mgpsumunsn  48460  invginvrid  48466  elmgpcntrd  49104  amgmlemALT  49903  amgmw2d  49904