Theorem mgpplusg 20125

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 6854	. . . 4 ⊢ · ∈ V
3		plusgid 17247	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17177	. . . 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 20124	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6843	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2789	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17159	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6832	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2783	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6832	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2783	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6844	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2797	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 182	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1542   ∈ wcel 2114  Vcvv 3429  ∅c0 4273  ⟨cop 4573  ‘cfv 6498  (class class class)co 7367   sSet csts 17133  ndxcnx 17163  +_gcplusg 17220  ._rcmulr 17221  mulGrpcmgp 20121

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 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-1cn 11096  ax-addcl 11098

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-nn 12175  df-2 12244  df-sets 17134  df-slot 17152  df-ndx 17164  df-plusg 17233  df-mgp 20122

This theorem is referenced by:  prdsmgp  20132  rngass  20140  rngcl  20145  isrngd  20154  rngpropd  20155  dfur2  20165  srgcl  20174  srgass  20175  srgideu  20176  srgidmlem  20182  issrgid  20185  srg1zr  20196  srgpcomp  20199  srgpcompp  20200  srgbinomlem4  20210  srgbinomlem  20211  csrgbinom  20213  ringcl  20231  crngcom  20232  iscrng2  20233  ringass  20234  ringideu  20235  ringidmlem  20249  isringid  20252  ringidss  20258  isringrng  20268  ringpropd  20269  crngpropd  20270  isringd  20272  iscrngd  20273  ring1  20291  gsummgp0  20297  pwspjmhmmgpd  20307  xpsring1d  20313  oppr1  20330  unitgrp  20363  unitlinv  20373  unitrinv  20374  rdivmuldivd  20393  rngidpropd  20395  invrpropd  20398  isrnghmmul  20422  dfrhm2  20454  rhmmul  20465  isrhm2d  20466  rhmunitinv  20488  rhmimasubrnglem  20542  rhmimasubrng  20543  cntzsubrng  20544  subrgugrp  20568  issubrg3  20577  cntzsubr  20583  rhmpropd  20586  isdomn3  20692  isdrng2  20720  drngmclOLD  20728  drngid2  20729  isdrngd  20742  isdrngdOLD  20744  cntzsdrg  20779  primefld  20782  rlmscaf  21202  rnglidlmmgm  21243  rnglidlmsgrp  21244  rng2idl1cntr  21303  xrsmcmn  21375  cnfldexp  21385  cnmsubglem  21410  expmhm  21416  nn0srg  21417  rge0srg  21418  expghm  21455  frobrhm  21555  psgnghm  21560  psgnco  21563  evpmodpmf1o  21576  sraassab  21848  assamulgscmlem2  21880  psrcrng  21950  mplcoe3  22016  mplcoe5lem  22017  mplcoe5  22018  mplcoe2  22019  mplbas2  22020  evlslem1  22060  mpfind  22093  mhppwdeg  22116  psdpw  22136  coe1tm  22238  ply1coe  22263  ringvcl  22365  mamuvs2  22371  mat1mhm  22449  scmatmhm  22499  mdetdiaglem  22563  mdetrlin  22567  mdetrsca  22568  mdetralt  22573  mdetunilem7  22583  mdetuni0  22586  m2detleib  22596  invrvald  22641  mat2pmatmhm  22698  pm2mpmhm  22785  chfacfpmmulgsum2  22830  cpmadugsumlemB  22839  cnmpt1mulr  24147  cnmpt2mulr  24148  reefgim  26415  efabl  26514  efsubm  26515  amgm  26954  wilthlem2  27032  wilthlem3  27033  dchrelbas3  27201  dchrzrhmul  27209  dchrmulcl  27212  dchrn0  27213  dchrinvcl  27216  dchrptlem2  27228  dchrsum2  27231  sum2dchr  27237  lgseisenlem3  27340  lgseisenlem4  27341  zsoring  28401  urpropd  33292  ringm1expp1  33295  ringinvval  33296  dvrcan5  33297  isunit3  33302  elrgspnlem2  33304  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  0ringcring  33313  erler  33326  rlocaddval  33329  rlocmulval  33330  rloccring  33331  domnprodn0  33336  domnprodeq0  33337  rrgsubm  33345  unitprodclb  33449  elringlsm  33453  lsmsnpridl  33458  cringm4  33506  ssdifidlprm  33518  mxidlprm  33530  rprmdvdspow  33593  rprmdvdsprod  33594  1arithidomlem1  33595  1arithidom  33597  1arithufdlem2  33605  1arithufdlem3  33606  1arithufdlem4  33607  dfufd2lem  33609  zringfrac  33614  deg1prod  33643  psrmonprod  33696  mplmonprod  33698  vietalem  33723  srapwov  33733  assarrginv  33780  evls1fldgencl  33814  iistmd  34046  xrge0iifmhm  34083  xrge0pluscn  34084  pl1cn  34099  zrhcntr  34123  aks6d1c1p4  42550  evl1gprodd  42556  idomnnzpownz  42571  idomnnzgmulnz  42572  ringexp0nn  42573  aks6d1c5lem3  42576  aks6d1c5lem2  42577  deg1gprod  42579  deg1pow  42580  unitscyglem5  42638  domnexpgn0cl  42968  abvexp  42977  fidomncyc  42980  selvvvval  43018  evlselv  43020  mhphf  43030  mon1psubm  43627  deg1mhm  43628  amgm2d  44625  amgm3d  44626  amgm4d  44627  2zrngmmgm  48728  2zrngmsgrp  48729  2zrngnring  48734  cznrng  48737  cznnring  48738  mgpsumunsn  48837  invginvrid  48843  elmgpcntrd  49480  amgmlemALT  50278  amgmw2d  50279