Theorem mgpplusg 20032

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 6904	. . . 4 ⊢ · ∈ V
3		plusgid 17228	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17145	. . . 4 ⊢ ((𝑅 ∈ V ∧ · ∈ V) → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
5	2, 4	mpan2 687	. . 3 ⊢ (𝑅 ∈ V → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
6		mgpval.1	. . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅)
7	6, 1	mgpval 20031	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6893	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2788	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17126	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6882	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2782	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6882	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2782	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6894	. . 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 1539   ∈ wcel 2104  Vcvv 3472  ∅c0 4321  ⟨cop 4633  ‘cfv 6542  (class class class)co 7411   sSet csts 17100  ndxcnx 17130  +_gcplusg 17201  ._rcmulr 17202  mulGrpcmgp 20028

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-1cn 11170  ax-addcl 11172

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-nn 12217  df-2 12279  df-sets 17101  df-slot 17119  df-ndx 17131  df-plusg 17214  df-mgp 20029

This theorem is referenced by:  prdsmgp  20045  rngass  20053  rngcl  20058  isrngd  20067  rngpropd  20068  dfur2  20078  srgcl  20087  srgass  20088  srgideu  20089  srgidmlem  20095  issrgid  20098  srg1zr  20109  srgpcomp  20112  srgpcompp  20113  srgbinomlem4  20123  srgbinomlem  20124  csrgbinom  20126  ringcl  20144  crngcom  20145  iscrng2  20146  ringass  20147  ringideu  20148  ringidmlem  20156  isringid  20159  ringidss  20165  isringrng  20175  ringpropd  20176  crngpropd  20177  isringd  20179  iscrngd  20180  ring1  20198  gsummgp0  20206  pwspjmhmmgpd  20216  xpsring1d  20221  oppr1  20241  unitgrp  20274  unitlinv  20284  unitrinv  20285  rdivmuldivd  20304  rngidpropd  20306  invrpropd  20309  isrnghmmul  20333  dfrhm2  20365  rhmmul  20377  isrhm2d  20378  rhmunitinv  20402  rhmimasubrnglem  20453  rhmimasubrng  20454  cntzsubrng  20455  subrgugrp  20481  issubrg3  20490  cntzsubr  20496  rhmpropd  20499  isdrng2  20514  drngmcl  20517  drngid2  20521  isdrngd  20533  isdrngdOLD  20535  cntzsdrg  20561  primefld  20564  rlmscaf  20976  rnglidlmmgm  21034  rnglidlmsgrp  21035  rng2idl1cntr  21064  xrsmcmn  21168  cnfldexp  21178  cnmsubglem  21208  expmhm  21214  nn0srg  21215  rge0srg  21216  expghm  21246  psgnghm  21352  psgnco  21355  evpmodpmf1o  21368  sraassab  21641  sraassaOLD  21643  assamulgscmlem2  21673  psrcrng  21752  mplcoe3  21812  mplcoe5lem  21813  mplcoe5  21814  mplcoe2  21815  mplbas2  21816  evlslem1  21864  mpfind  21889  mhppwdeg  21912  coe1tm  22015  ply1coe  22040  ringvcl  22120  mamuvs2  22126  mat1mhm  22206  scmatmhm  22256  mdetdiaglem  22320  mdetrlin  22324  mdetrsca  22325  mdetralt  22330  mdetunilem7  22340  mdetuni0  22343  m2detleib  22353  invrvald  22398  mat2pmatmhm  22455  pm2mpmhm  22542  chfacfpmmulgsum2  22587  cpmadugsumlemB  22596  cnmpt1mulr  23906  cnmpt2mulr  23907  reefgim  26198  efabl  26295  efsubm  26296  amgm  26731  wilthlem2  26809  wilthlem3  26810  dchrelbas3  26977  dchrzrhmul  26985  dchrmulcl  26988  dchrn0  26989  dchrinvcl  26992  dchrptlem2  27004  dchrsum2  27007  sum2dchr  27013  lgseisenlem3  27116  lgseisenlem4  27117  urpropd  32648  frobrhm  32652  ringinvval  32654  dvrcan5  32655  elringlsm  32777  lsmsnpridl  32782  cringm4  32839  mxidlprm  32860  evls1fldgencl  33033  iistmd  33180  xrge0iifmhm  33217  xrge0pluscn  33218  pl1cn  33233  selvvvval  41459  evlselv  41461  mhphf  41471  isdomn3  42248  mon1psubm  42250  deg1mhm  42251  amgm2d  43252  amgm3d  43253  amgm4d  43254  2zrngmmgm  46932  2zrngmsgrp  46933  2zrngnring  46938  cznrng  46941  cznnring  46942  mgpsumunsn  47125  invginvrid  47131  amgmlemALT  47937  amgmw2d  47938