Theorem mgpplusg 20072

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 6906	. . . 4 ⊢ · ∈ V
3		plusgid 17254	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17171	. . . 4 ⊢ ((𝑅 ∈ V ∧ · ∈ V) → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
5	2, 4	mpan2 690	. . 3 ⊢ (𝑅 ∈ V → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
6		mgpval.1	. . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅)
7	6, 1	mgpval 20071	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6895	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2786	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17152	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6884	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2780	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6884	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2780	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6896	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2794	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 182	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1534   ∈ wcel 2099  Vcvv 3470  ∅c0 4319  ⟨cop 4631  ‘cfv 6543  (class class class)co 7415   sSet csts 17126  ndxcnx 17156  +_gcplusg 17227  ._rcmulr 17228  mulGrpcmgp 20068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5294  ax-nul 5301  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-cnex 11189  ax-1cn 11191  ax-addcl 11193

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-ral 3058  df-rex 3067  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-iun 4994  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7418  df-oprab 7419  df-mpo 7420  df-om 7866  df-2nd 7989  df-frecs 8281  df-wrecs 8312  df-recs 8386  df-rdg 8425  df-nn 12238  df-2 12300  df-sets 17127  df-slot 17145  df-ndx 17157  df-plusg 17240  df-mgp 20069

This theorem is referenced by:  prdsmgp  20085  rngass  20093  rngcl  20098  isrngd  20107  rngpropd  20108  dfur2  20118  srgcl  20127  srgass  20128  srgideu  20129  srgidmlem  20135  issrgid  20138  srg1zr  20149  srgpcomp  20152  srgpcompp  20153  srgbinomlem4  20163  srgbinomlem  20164  csrgbinom  20166  ringcl  20184  crngcom  20185  iscrng2  20186  ringass  20187  ringideu  20188  ringidmlem  20198  isringid  20201  ringidss  20207  isringrng  20217  ringpropd  20218  crngpropd  20219  isringd  20221  iscrngd  20222  ring1  20240  gsummgp0  20248  pwspjmhmmgpd  20258  xpsring1d  20263  oppr1  20283  unitgrp  20316  unitlinv  20326  unitrinv  20327  rdivmuldivd  20346  rngidpropd  20348  invrpropd  20351  isrnghmmul  20375  dfrhm2  20407  rhmmul  20419  isrhm2d  20420  rhmunitinv  20444  rhmimasubrnglem  20496  rhmimasubrng  20497  cntzsubrng  20498  subrgugrp  20524  issubrg3  20533  cntzsubr  20539  rhmpropd  20542  isdrng2  20632  drngmcl  20635  drngid2  20639  isdrngd  20651  isdrngdOLD  20653  cntzsdrg  20684  primefld  20687  rlmscaf  21094  rnglidlmmgm  21134  rnglidlmsgrp  21135  rng2idl1cntr  21189  isdomn3  21242  xrsmcmn  21313  cnfldexp  21326  cnmsubglem  21357  expmhm  21363  nn0srg  21364  rge0srg  21365  expghm  21395  psgnghm  21506  psgnco  21509  evpmodpmf1o  21522  sraassab  21795  sraassaOLD  21797  assamulgscmlem2  21827  psrcrng  21909  mplcoe3  21970  mplcoe5lem  21971  mplcoe5  21972  mplcoe2  21973  mplbas2  21974  evlslem1  22022  mpfind  22047  mhppwdeg  22068  coe1tm  22186  ply1coe  22211  ringvcl  22294  mamuvs2  22300  mat1mhm  22380  scmatmhm  22430  mdetdiaglem  22494  mdetrlin  22498  mdetrsca  22499  mdetralt  22504  mdetunilem7  22514  mdetuni0  22517  m2detleib  22527  invrvald  22572  mat2pmatmhm  22629  pm2mpmhm  22716  chfacfpmmulgsum2  22761  cpmadugsumlemB  22770  cnmpt1mulr  24080  cnmpt2mulr  24081  reefgim  26381  efabl  26478  efsubm  26479  amgm  26917  wilthlem2  26995  wilthlem3  26996  dchrelbas3  27165  dchrzrhmul  27173  dchrmulcl  27176  dchrn0  27177  dchrinvcl  27180  dchrptlem2  27192  dchrsum2  27195  sum2dchr  27201  lgseisenlem3  27304  lgseisenlem4  27305  urpropd  32934  frobrhm  32936  ringinvval  32938  dvrcan5  32939  rrgsubm  32948  erler  32974  rlocaddval  32977  rlocmulval  32978  rloccring  32979  zringfrac  32991  elringlsm  33097  lsmsnpridl  33102  cringm4  33157  mxidlprm  33178  evls1fldgencl  33349  iistmd  33498  xrge0iifmhm  33535  xrge0pluscn  33536  pl1cn  33551  aks6d1c1p4  41577  evl1gprodd  41583  idomnnzpownz  41598  idomnnzgmulnz  41599  ringexp0nn  41600  aks6d1c5lem3  41603  aks6d1c5lem2  41604  deg1gprod  41607  deg1pow  41608  selvvvval  41809  evlselv  41811  mhphf  41821  mon1psubm  42618  deg1mhm  42619  amgm2d  43619  amgm3d  43620  amgm4d  43621  2zrngmmgm  47305  2zrngmsgrp  47306  2zrngnring  47311  cznrng  47314  cznnring  47315  mgpsumunsn  47416  invginvrid  47422  amgmlemALT  48227  amgmw2d  48228