Theorem mgpplusg 19639

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 6770	. . . 4 ⊢ · ∈ V
3		plusgid 16915	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 16837	. . . 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 19638	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6759	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2797	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 16818	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6748	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2790	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6748	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2790	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6760	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2805	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 182	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2108  Vcvv 3422  ∅c0 4253  ⟨cop 4564  ‘cfv 6418  (class class class)co 7255   sSet csts 16792  ndxcnx 16822  +_gcplusg 16888  ._rcmulr 16889  mulGrpcmgp 19635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-1cn 10860  ax-addcl 10862

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-nn 11904  df-2 11966  df-sets 16793  df-slot 16811  df-ndx 16823  df-plusg 16901  df-mgp 19636

This theorem is referenced by:  dfur2  19655  srgcl  19663  srgass  19664  srgideu  19665  srgidmlem  19671  issrgid  19674  srg1zr  19680  srgpcomp  19683  srgpcompp  19684  srgbinomlem4  19694  srgbinomlem  19695  csrgbinom  19697  ringcl  19715  crngcom  19716  iscrng2  19717  ringass  19718  ringideu  19719  ringidmlem  19724  isringid  19727  ringidss  19731  ringpropd  19736  crngpropd  19737  isringd  19739  iscrngd  19740  ring1  19756  gsummgp0  19762  prdsmgp  19764  oppr1  19791  unitgrp  19824  unitlinv  19834  unitrinv  19835  rngidpropd  19852  invrpropd  19855  dfrhm2  19876  rhmmul  19886  isrhm2d  19887  isdrng2  19916  drngmcl  19919  drngid2  19922  isdrngd  19931  subrgugrp  19958  issubrg3  19967  cntzsubr  19972  rhmpropd  19975  cntzsdrg  19985  primefld  19988  rlmscaf  20392  xrsmcmn  20533  cnfldexp  20543  cnmsubglem  20573  expmhm  20579  nn0srg  20580  rge0srg  20581  expghm  20609  psgnghm  20697  psgnco  20700  evpmodpmf1o  20713  sraassa  20984  assamulgscmlem2  21014  psrcrng  21092  mplcoe3  21149  mplcoe5lem  21150  mplcoe5  21151  mplcoe2  21152  mplbas2  21153  evlslem1  21202  mpfind  21227  mhppwdeg  21250  coe1tm  21354  ply1coe  21377  ringvcl  21457  mamuvs2  21463  mat1mhm  21541  scmatmhm  21591  mdetdiaglem  21655  mdetrlin  21659  mdetrsca  21660  mdetralt  21665  mdetunilem7  21675  mdetuni0  21678  m2detleib  21688  invrvald  21733  mat2pmatmhm  21790  pm2mpmhm  21877  chfacfpmmulgsum2  21922  cpmadugsumlemB  21931  cnmpt1mulr  23241  cnmpt2mulr  23242  reefgim  25514  efabl  25611  efsubm  25612  amgm  26045  wilthlem2  26123  wilthlem3  26124  dchrelbas3  26291  dchrzrhmul  26299  dchrmulcl  26302  dchrn0  26303  dchrinvcl  26306  dchrptlem2  26318  dchrsum2  26321  sum2dchr  26327  lgseisenlem3  26430  lgseisenlem4  26431  frobrhm  31387  rdivmuldivd  31390  ringinvval  31391  dvrcan5  31392  rhmunitinv  31423  elringlsm  31483  lsmsnpridl  31488  cringm4  31524  mxidlprm  31542  iistmd  31754  xrge0iifmhm  31791  xrge0pluscn  31792  pl1cn  31807  pwspjmhmmgpd  40192  mhphf  40208  isdomn3  40945  mon1psubm  40947  deg1mhm  40948  amgm2d  41698  amgm3d  41699  amgm4d  41700  isringrng  45327  rngcl  45329  isrnghmmul  45339  lidlmmgm  45371  lidlmsgrp  45372  2zrngmmgm  45392  2zrngmsgrp  45393  2zrngnring  45398  cznrng  45401  cznnring  45402  mgpsumunsn  45585  invginvrid  45591  amgmlemALT  46393  amgmw2d  46394