Theorem mgpplusg 20220

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 6896	. . . 4 ⊢ · ∈ V
3		plusgid 17337	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17267	. . . 4 ⊢ ((𝑅 ∈ V ∧ · ∈ V) → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
5	2, 4	mpan2 703	. . 3 ⊢ (𝑅 ∈ V → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
6		mgpval.1	. . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅)
7	6, 1	mgpval 20219	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6885	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2822	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17249	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6874	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2816	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6874	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2816	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6886	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2830	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 184	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1567   ∈ wcel 2149  Vcvv 3461  ∅c0 4292  ⟨cop 4598  ‘cfv 6537  (class class class)co 7411   sSet csts 17223  ndxcnx 17253  +_gcplusg 17310  ._rcmulr 17311  mulGrpcmgp 20216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5259  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11156  ax-1cn 11158  ax-addcl 11160

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3376  df-rab 3423  df-v 3463  df-sbc 3752  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7863  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-nn 12234  df-2 12303  df-sets 17224  df-slot 17242  df-ndx 17254  df-plusg 17323  df-mgp 20217

This theorem is referenced by:  prdsmgp  20227  elmgplsm  20228  rngass  20237  rngcl  20242  isrngd  20251  rngpropd  20252  rng1zrlem  20259  dfur2  20266  srgcl  20275  srgass  20276  srgideu  20277  srgidmlem  20283  issrgid  20286  srgpcomp  20300  srgpcompp  20301  srgbinomlem4  20311  srgbinomlem  20312  csrgbinom  20314  ringcl  20332  crngcom  20333  iscrng2  20334  ringass  20335  ringideu  20336  ringidmlem  20351  isringid  20354  ringidss  20360  isringrng  20370  ringpropd  20371  crngpropd  20372  isringd  20374  iscrngd  20375  ring1  20393  gsummgp0  20399  pwspjmhmmgpd  20409  xpsring1d  20415  oppr1  20432  unitgrp  20465  unitlinv  20475  unitrinv  20476  rdivmuldivd  20495  rngidpropd  20497  invrpropd  20500  isrnghmmul  20524  dfrhm2  20556  rhmmul  20568  isrhm2d  20569  rhmunitinv  20594  rhmimasubrnglem  20650  rhmimasubrng  20651  cntzsubrng  20652  subrgugrp  20676  issubrg3  20685  cntzsubr  20691  rhmpropd  20694  isdomn3  20799  isdrng2  20827  drngid2  20835  isdrngd  20847  isdrngdOLD  20849  cntzsdrg  20883  primefld  20886  rlmscaf  21306  rnglidlmmgm  21353  rnglidlmsgrp  21354  rng2idl1cntr  21416  cringm4  21442  ssdifidlprm  21455  prmidlsubm  21456  xrsmcmn  21514  cnfldexp  21524  cnmsubglem  21549  expmhm  21555  nn0srg  21556  rge0srg  21557  expghm  21594  frobrhm  21694  psgnghm  21699  psgnco  21702  evpmodpmf1o  21715  sraassab  21987  assamulgscmlem2  22019  psrcrng  22090  mplcoe3  22158  mplcoe5lem  22159  mplcoe5  22160  mplcoe2  22161  mplbas2  22162  evlslem1  22202  mpfind  22235  selvvvval  22262  mhppwdeg  22282  psdpw  22302  coe1tm  22403  ply1coe  22427  ringvcl  22526  mamuvs2  22532  mat1mhm  22610  scmatmhm  22660  mdetdiaglem  22724  mdetrlin  22728  mdetrsca  22729  mdetralt  22734  mdetunilem7  22744  mdetuni0  22747  m2detleib  22757  invrvald  22802  mat2pmatmhm  22859  pm2mpmhm  22946  chfacfpmmulgsum2  22991  cpmadugsumlemB  23000  cnmpt1mulr  24308  cnmpt2mulr  24309  reefgim  26579  efabl  26681  efsubm  26682  amgm  27121  wilthlem2  27199  wilthlem3  27200  dchrelbas3  27368  dchrzrhmul  27376  dchrmulcl  27379  dchrn0  27380  dchrinvcl  27383  dchrptlem2  27395  dchrsum2  27398  sum2dchr  27404  lgseisenlem3  27507  lgseisenlem4  27508  zsoring  28568  urpropd  33491  ringm1expp1  33494  ringinvval  33495  dvrcan5  33496  isunit3  33501  elrgspnlem2  33504  elrgspnsubrunlem1  33508  elrgspnsubrunlem2  33509  0ringcring  33513  erler  33526  rlocaddval  33530  rlocmulval  33531  rloccring  33532  rlocisunit  33537  domnprodn0  33539  domnprodeq0  33540  rrgsubm  33545  unitprodclb  33646  lsmsnpridl  33653  mxidlprm  33698  rprmdvdspow  33768  rprmdvdsprod  33769  1arithidomlem1  33770  1arithidom  33772  1arithufdlem2  33780  1arithufdlem3  33781  1arithufdlem4  33782  dfufd2lem  33784  zringfrac  33789  deg1prod  33818  psrmonprod  33887  mplmonprod  33889  vietalem  33914  srapwov  33924  assarrginv  33971  evls1fldgencl  34005  iistmd  34237  xrge0iifmhm  34274  xrge0pluscn  34275  pl1cn  34290  zrhcntr  34314  aks6d1c1p4  42803  evl1gprodd  42809  idomnnzpownz  42824  idomnnzgmulnz  42825  ringexp0nn  42826  aks6d1c5lem3  42829  aks6d1c5lem2  42830  deg1gprod  42832  deg1pow  42833  unitscyglem5  42891  domnexpgn0cl  43218  abvexp  43227  fidomncyc  43230  evlselv  43248  mhphf  43256  mon1psubm  43853  deg1mhm  43854  amgm2d  44851  amgm3d  44852  amgm4d  44853  2zrngmmgm  48941  2zrngmsgrp  48942  2zrngnring  48947  cznrng  48950  cznnring  48951  mgpsumunsn  49061  invginvrid  49067  elmgpcntrd  49703  amgmlemALT  50512  amgmw2d  50513