Theorem mgpplusg 20311

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 6888	. . . 4 ⊢ · ∈ V
3		plusgid 17402	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17332	. . . 4 ⊢ ((𝑅 ∈ V ∧ · ∈ V) → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
5	2, 4	mpan2 704	. . 3 ⊢ (𝑅 ∈ V → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
6		mgpval.1	. . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅)
7	6, 1	mgpval 20310	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6877	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2813	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17314	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6866	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2807	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6866	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2807	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6878	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2821	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 184	1 ⊢ · = (+g‘𝑀)

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2145  Vcvv 3450  ∅c0 4279  ⟨cop 4590  ‘cfv 6528  (class class class)co 7409   sSet csts 17288  ndxcnx 17318  +_gcplusg 17375  ._rcmulr 17376  mulGrpcmgp 20307

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7735  ax-cnex 11213  ax-1cn 11215  ax-addcl 11217

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6294  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7862  df-2nd 7986  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-nn 12291  df-2 12360  df-sets 17289  df-slot 17307  df-ndx 17319  df-plusg 17388  df-mgp 20308

This theorem is used by:  prdsmgp  20318  elmgplsm  20319  rngass  20328  rngcl  20333  isrngd  20342  rngpropd  20343  rng1zrlem  20350  dfur2  20357  srgcl  20366  srgass  20367  srgideu  20368  srgidmlem  20374  issrgid  20377  srgpcomp  20391  srgpcompp  20392  srgbinomlem4  20402  srgbinomlem  20403  csrgbinom  20405  ringcl  20424  crngcom  20425  iscrng2  20426  ringass  20427  ringideu  20428  ringidmlem  20444  isringid  20447  ringidss  20453  isringrng  20463  dfring3  20465  ringpropd  20466  crngpropd  20467  isringd  20469  iscrngd  20470  ring1  20488  gsummgp0  20494  pwspjmhmmgpd  20504  xpsring1d  20510  oppr1  20527  unitgrp  20560  unitlinv  20570  unitrinv  20571  rdivmuldivd  20590  rngidpropd  20592  invrpropd  20595  isrnghmmul  20619  dfrhm2  20651  rhmmul  20667  isrhm2d  20668  rhmunitinv  20708  rhmimasubrnglem  20764  rhmimasubrng  20765  cntzsubrng  20766  subrgugrp  20790  issubrg3  20799  cntzsubr  20805  rhmpropd  20808  isdomn3  20913  isdrng2  20944  isdrng3lem1  20952  isdrng3lem2  20953  drngid2  20957  isdrngd  20969  isdrngdOLD  20971  cntzsdrg  21006  primefld  21009  rlmscaf  21429  rnglidlmmgm  21480  rnglidlmsgrp  21481  rng2idl1cntr  21548  cringm4  21574  ssdifidlprm  21589  prmidlsubm  21590  xrsmcmn  21648  cnfldexp  21658  cnmsubglem  21683  expmhm  21689  nn0srg  21690  rge0srg  21691  expghm  21728  frobrhm  21828  psgnghm  21833  psgnco  21836  evpmodpmf1o  21849  sraassab  22123  assamulgscmlem2  22155  psrcrng  22226  mplcoe3  22294  mplcoe5lem  22295  mplcoe5  22296  mplcoe2  22297  mplbas2  22298  evlslem1  22338  mpfind  22371  selvvvval  22398  mhppwdeg  22418  psdpw  22438  coe1tm  22539  ply1coe  22563  ringvcl  22662  mamuvs2  22668  mat1mhm  22746  scmatmhm  22796  mdetdiaglem  22860  mdetrlin  22864  mdetrsca  22865  mdetralt  22870  mdetunilem7  22880  mdetuni0  22883  m2detleib  22893  invrvald  22938  mat2pmatmhm  22998  pm2mpmhm  23085  chfacfpmmulgsum2  23130  cpmadugsumlemB  23139  cnmpt1mulr  24448  cnmpt2mulr  24449  reefgim  26726  efabl  26827  efsubm  26828  amgm  27267  wilthlem2  27345  wilthlem3  27346  dchrelbas3  27514  dchrzrhmul  27522  dchrmulcl  27525  dchrn0  27526  dchrinvcl  27529  dchrptlem2  27541  dchrsum2  27544  sum2dchr  27550  lgseisenlem3  27653  lgseisenlem4  27654  zsoring  28714  urpropd  33710  ringm1expp1  33713  ringinvval  33714  dvrcan5  33715  isunit3  33720  elrgspnlem2  33723  elrgspnsubrunlem1  33727  elrgspnsubrunlem2  33728  0ringcring  33732  erler  33745  rlocaddval  33749  rlocmulval  33750  rloccring  33751  rlocisunit  33756  domnprodn0  33758  domnprodeq0  33759  rrgsubm  33764  unitprodclb  33863  lsmsnpridl  33870  mxidlprm  33914  rprmdvdspow  33984  rprmdvdsprod  33985  1arithidomlem1  33986  1arithidom  33988  1arithufdlem2  33996  1arithufdlem3  33997  1arithufdlem4  33998  dfufd2lem  34000  zringfrac  34005  deg1prod  34034  psrmonprod  34103  mplmonprod  34105  vietalem  34130  srapwov  34140  assarrginv  34187  evls1fldgencl  34221  iistmd  34453  xrge0iifmhm  34490  xrge0pluscn  34491  pl1cn  34506  zrhcntr  34530  aks6d1c1p4  43075  evl1gprodd  43081  idomnnzpownz  43096  idomnnzgmulnz  43097  ringexp0nn  43098  aks6d1c5lem3  43101  aks6d1c5lem2  43102  deg1gprod  43104  deg1pow  43105  unitscyglem5  43163  domnexpgn0cl  43503  abvexp  43512  fidomncyc  43515  evlselv  43533  mhphf  43541  mon1psubm  44138  deg1mhm  44139  amgm2d  45136  amgm3d  45137  amgm4d  45138  2zrngmmgm  49265  2zrngmsgrp  49266  2zrngnring  49271  cznrng  49274  cznnring  49275  mgpsumunsn  49389  invginvrid  49395  elmgpcntrd  50029  amgmlemALT  50904  amgmw2d  50905