Theorem mgpplusg 20096

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 6858	. . . 4 ⊢ · ∈ V
3		plusgid 17218	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17148	. . . 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 20095	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6847	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2790	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17130	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6836	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2784	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6836	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2784	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6848	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2798	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 182	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1542   ∈ wcel 2114  Vcvv 3442  ∅c0 4287  ⟨cop 4588  ‘cfv 6502  (class class class)co 7370   sSet csts 17104  ndxcnx 17134  +_gcplusg 17191  ._rcmulr 17192  mulGrpcmgp 20092

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 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-cnex 11096  ax-1cn 11098  ax-addcl 11100

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6269  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-ov 7373  df-oprab 7374  df-mpo 7375  df-om 7821  df-2nd 7946  df-frecs 8235  df-wrecs 8266  df-recs 8315  df-rdg 8353  df-nn 12160  df-2 12222  df-sets 17105  df-slot 17123  df-ndx 17135  df-plusg 17204  df-mgp 20093

This theorem is referenced by:  prdsmgp  20103  rngass  20111  rngcl  20116  isrngd  20125  rngpropd  20126  dfur2  20136  srgcl  20145  srgass  20146  srgideu  20147  srgidmlem  20153  issrgid  20156  srg1zr  20167  srgpcomp  20170  srgpcompp  20171  srgbinomlem4  20181  srgbinomlem  20182  csrgbinom  20184  ringcl  20202  crngcom  20203  iscrng2  20204  ringass  20205  ringideu  20206  ringidmlem  20220  isringid  20223  ringidss  20229  isringrng  20239  ringpropd  20240  crngpropd  20241  isringd  20243  iscrngd  20244  ring1  20262  gsummgp0  20270  pwspjmhmmgpd  20280  xpsring1d  20286  oppr1  20303  unitgrp  20336  unitlinv  20346  unitrinv  20347  rdivmuldivd  20366  rngidpropd  20368  invrpropd  20371  isrnghmmul  20395  dfrhm2  20427  rhmmul  20438  isrhm2d  20439  rhmunitinv  20461  rhmimasubrnglem  20515  rhmimasubrng  20516  cntzsubrng  20517  subrgugrp  20541  issubrg3  20550  cntzsubr  20556  rhmpropd  20559  isdomn3  20665  isdrng2  20693  drngmclOLD  20701  drngid2  20702  isdrngd  20715  isdrngdOLD  20717  cntzsdrg  20752  primefld  20755  rlmscaf  21176  rnglidlmmgm  21217  rnglidlmsgrp  21218  rng2idl1cntr  21277  xrsmcmn  21363  cnfldexp  21376  cnmsubglem  21402  expmhm  21408  nn0srg  21409  rge0srg  21410  expghm  21447  frobrhm  21547  psgnghm  21552  psgnco  21555  evpmodpmf1o  21568  sraassab  21840  sraassaOLD  21842  assamulgscmlem2  21873  psrcrng  21944  mplcoe3  22010  mplcoe5lem  22011  mplcoe5  22012  mplcoe2  22013  mplbas2  22014  evlslem1  22054  mpfind  22087  mhppwdeg  22110  psdpw  22130  coe1tm  22232  ply1coe  22259  ringvcl  22361  mamuvs2  22367  mat1mhm  22445  scmatmhm  22495  mdetdiaglem  22559  mdetrlin  22563  mdetrsca  22564  mdetralt  22569  mdetunilem7  22579  mdetuni0  22582  m2detleib  22592  invrvald  22637  mat2pmatmhm  22694  pm2mpmhm  22781  chfacfpmmulgsum2  22826  cpmadugsumlemB  22835  cnmpt1mulr  24143  cnmpt2mulr  24144  reefgim  26433  efabl  26532  efsubm  26533  amgm  26974  wilthlem2  27052  wilthlem3  27053  dchrelbas3  27222  dchrzrhmul  27230  dchrmulcl  27233  dchrn0  27234  dchrinvcl  27237  dchrptlem2  27249  dchrsum2  27252  sum2dchr  27258  lgseisenlem3  27361  lgseisenlem4  27362  zsoring  28422  urpropd  33331  ringm1expp1  33334  ringinvval  33335  dvrcan5  33336  isunit3  33341  elrgspnlem2  33343  elrgspnsubrunlem1  33347  elrgspnsubrunlem2  33348  0ringcring  33352  erler  33365  rlocaddval  33368  rlocmulval  33369  rloccring  33370  domnprodn0  33375  domnprodeq0  33376  rrgsubm  33384  unitprodclb  33488  elringlsm  33492  lsmsnpridl  33497  cringm4  33545  ssdifidlprm  33557  mxidlprm  33569  rprmdvdspow  33632  rprmdvdsprod  33633  1arithidomlem1  33634  1arithidom  33636  1arithufdlem2  33644  1arithufdlem3  33645  1arithufdlem4  33646  dfufd2lem  33648  zringfrac  33653  deg1prod  33682  psrmonprod  33735  mplmonprod  33737  vietalem  33762  srapwov  33772  assarrginv  33820  evls1fldgencl  33854  iistmd  34086  xrge0iifmhm  34123  xrge0pluscn  34124  pl1cn  34139  zrhcntr  34163  aks6d1c1p4  42510  evl1gprodd  42516  idomnnzpownz  42531  idomnnzgmulnz  42532  ringexp0nn  42533  aks6d1c5lem3  42536  aks6d1c5lem2  42537  deg1gprod  42539  deg1pow  42540  unitscyglem5  42598  domnexpgn0cl  42922  abvexp  42931  fidomncyc  42934  selvvvval  42972  evlselv  42974  mhphf  42984  mon1psubm  43585  deg1mhm  43586  amgm2d  44583  amgm3d  44584  amgm4d  44585  2zrngmmgm  48641  2zrngmsgrp  48642  2zrngnring  48647  cznrng  48650  cznnring  48651  mgpsumunsn  48750  invginvrid  48756  elmgpcntrd  49393  amgmlemALT  50191  amgmw2d  50192