Theorem mgpplusg 20110

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 6900	. . . 4 ⊢ · ∈ V
3		plusgid 17301	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17227	. . . 4 ⊢ ((𝑅 ∈ V ∧ · ∈ V) → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
5	2, 4	mpan2 691	. . 3 ⊢ (𝑅 ∈ V → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
6		mgpval.1	. . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅)
7	6, 1	mgpval 20109	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6889	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2787	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17209	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6878	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2781	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6878	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2781	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6890	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2795	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 182	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2107  Vcvv 3463  ∅c0 4313  ⟨cop 4612  ‘cfv 6541  (class class class)co 7413   sSet csts 17183  ndxcnx 17213  +_gcplusg 17274  ._rcmulr 17275  mulGrpcmgp 20106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-cnex 11193  ax-1cn 11195  ax-addcl 11197

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-tr 5240  df-id 5558  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-pred 6301  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7870  df-2nd 7997  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-nn 12249  df-2 12311  df-sets 17184  df-slot 17202  df-ndx 17214  df-plusg 17287  df-mgp 20107

This theorem is referenced by:  prdsmgp  20117  rngass  20125  rngcl  20130  isrngd  20139  rngpropd  20140  dfur2  20150  srgcl  20159  srgass  20160  srgideu  20161  srgidmlem  20167  issrgid  20170  srg1zr  20181  srgpcomp  20184  srgpcompp  20185  srgbinomlem4  20195  srgbinomlem  20196  csrgbinom  20198  ringcl  20216  crngcom  20217  iscrng2  20218  ringass  20219  ringideu  20220  ringidmlem  20234  isringid  20237  ringidss  20243  isringrng  20253  ringpropd  20254  crngpropd  20255  isringd  20257  iscrngd  20258  ring1  20276  gsummgp0  20284  pwspjmhmmgpd  20294  xpsring1d  20299  oppr1  20319  unitgrp  20352  unitlinv  20362  unitrinv  20363  rdivmuldivd  20382  rngidpropd  20384  invrpropd  20387  isrnghmmul  20411  dfrhm2  20443  rhmmul  20455  isrhm2d  20456  rhmunitinv  20480  rhmimasubrnglem  20534  rhmimasubrng  20535  cntzsubrng  20536  subrgugrp  20560  issubrg3  20569  cntzsubr  20575  rhmpropd  20578  isdomn3  20684  isdrng2  20712  drngmclOLD  20720  drngid2  20721  isdrngd  20734  isdrngdOLD  20736  cntzsdrg  20772  primefld  20775  rlmscaf  21177  rnglidlmmgm  21218  rnglidlmsgrp  21219  rng2idl1cntr  21278  xrsmcmn  21367  cnfldexp  21380  cnmsubglem  21411  expmhm  21417  nn0srg  21418  rge0srg  21419  expghm  21449  frobrhm  21549  psgnghm  21553  psgnco  21556  evpmodpmf1o  21569  sraassab  21843  sraassaOLD  21845  assamulgscmlem2  21875  psrcrng  21947  mplcoe3  22011  mplcoe5lem  22012  mplcoe5  22013  mplcoe2  22014  mplbas2  22015  evlslem1  22055  mpfind  22080  mhppwdeg  22103  psdpw  22123  coe1tm  22225  ply1coe  22251  ringvcl  22353  mamuvs2  22359  mat1mhm  22439  scmatmhm  22489  mdetdiaglem  22553  mdetrlin  22557  mdetrsca  22558  mdetralt  22563  mdetunilem7  22573  mdetuni0  22576  m2detleib  22586  invrvald  22631  mat2pmatmhm  22688  pm2mpmhm  22775  chfacfpmmulgsum2  22820  cpmadugsumlemB  22829  cnmpt1mulr  24137  cnmpt2mulr  24138  reefgim  26431  efabl  26529  efsubm  26530  amgm  26971  wilthlem2  27049  wilthlem3  27050  dchrelbas3  27219  dchrzrhmul  27227  dchrmulcl  27230  dchrn0  27231  dchrinvcl  27234  dchrptlem2  27246  dchrsum2  27249  sum2dchr  27255  lgseisenlem3  27358  lgseisenlem4  27359  urpropd  33180  ringinvval  33183  dvrcan5  33184  isunit3  33189  elrgspnlem2  33191  elrgspnsubrunlem1  33195  elrgspnsubrunlem2  33196  0ringcring  33200  erler  33213  rlocaddval  33216  rlocmulval  33217  rloccring  33218  domnprodn0  33223  rrgsubm  33231  unitprodclb  33357  elringlsm  33361  lsmsnpridl  33366  cringm4  33414  ssdifidlprm  33426  mxidlprm  33438  rprmdvdspow  33501  rprmdvdsprod  33502  1arithidomlem1  33503  1arithidom  33505  1arithufdlem2  33513  1arithufdlem3  33514  1arithufdlem4  33515  dfufd2lem  33517  zringfrac  33522  assarrginv  33627  evls1fldgencl  33662  iistmd  33876  xrge0iifmhm  33913  xrge0pluscn  33914  pl1cn  33929  zrhcntr  33955  aks6d1c1p4  42087  evl1gprodd  42093  idomnnzpownz  42108  idomnnzgmulnz  42109  ringexp0nn  42110  aks6d1c5lem3  42113  aks6d1c5lem2  42114  deg1gprod  42116  deg1pow  42117  unitscyglem5  42175  domnexpgn0cl  42512  abvexp  42521  fidomncyc  42524  selvvvval  42574  evlselv  42576  mhphf  42586  mon1psubm  43189  deg1mhm  43190  amgm2d  44188  amgm3d  44189  amgm4d  44190  2zrngmmgm  48141  2zrngmsgrp  48142  2zrngnring  48147  cznrng  48150  cznnring  48151  mgpsumunsn  48250  invginvrid  48256  elmgpcntrd  48886  amgmlemALT  49417  amgmw2d  49418