Theorem mgpplusg 18937

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 6559	. . . 4 ⊢ · ∈ V
3		plusgid 16429	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 16371	. . . 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 18936	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6548	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	syl6eqr 2851	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 16368	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6538	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	syl5eq 2845	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6538	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	syl5eq 2845	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6549	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2859	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 183	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1525   ∈ wcel 2083  Vcvv 3440  ∅c0 4217  ⟨cop 4484  ‘cfv 6232  (class class class)co 7023  ndxcnx 16313   sSet csts 16314  +_gcplusg 16398  ._rcmulr 16399  mulGrpcmgp 18933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-cnex 10446  ax-1cn 10448  ax-addcl 10450

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-nn 11493  df-2 11554  df-ndx 16319  df-slot 16320  df-sets 16323  df-plusg 16411  df-mgp 18934

This theorem is referenced by:  dfur2  18948  srgcl  18956  srgass  18957  srgideu  18958  srgidmlem  18964  issrgid  18967  srg1zr  18973  srgpcomp  18976  srgpcompp  18977  srgbinomlem4  18987  srgbinomlem  18988  csrgbinom  18990  ringcl  19005  crngcom  19006  iscrng2  19007  ringass  19008  ringideu  19009  ringidmlem  19014  isringid  19017  ringidss  19021  ringpropd  19026  crngpropd  19027  isringd  19029  iscrngd  19030  ring1  19046  gsummgp0  19052  prdsmgp  19054  oppr1  19078  unitgrp  19111  unitlinv  19121  unitrinv  19122  rngidpropd  19139  invrpropd  19142  dfrhm2  19163  rhmmul  19173  isrhm2d  19174  isdrng2  19206  drngmcl  19209  drngid2  19212  isdrngd  19221  subrgugrp  19248  issubrg3  19257  cntzsubr  19262  rhmpropd  19265  cntzsdrg  19275  primefld  19278  rlmscaf  19674  sraassa  19791  assamulgscmlem2  19821  psrcrng  19885  mplcoe3  19938  mplcoe5lem  19939  mplcoe5  19940  mplcoe2  19941  mplbas2  19942  evlslem1  19986  mpfind  20007  coe1tm  20128  ply1coe  20151  xrsmcmn  20254  cnfldexp  20264  cnmsubglem  20294  expmhm  20300  nn0srg  20301  rge0srg  20302  expghm  20329  psgnghm  20410  psgnco  20413  evpmodpmf1o  20426  ringvcl  20695  mamuvs2  20703  mat1mhm  20781  scmatmhm  20831  mdetdiaglem  20895  mdetrlin  20899  mdetrsca  20900  mdetralt  20905  mdetunilem7  20915  mdetuni0  20918  m2detleib  20928  invrvald  20973  mat2pmatmhm  21029  pm2mpmhm  21116  chfacfpmmulgsum2  21161  cpmadugsumlemB  21170  cnmpt1mulr  22477  cnmpt2mulr  22478  reefgim  24725  efabl  24819  efsubm  24820  amgm  25254  wilthlem2  25332  wilthlem3  25333  dchrelbas3  25500  dchrzrhmul  25508  dchrmulcl  25511  dchrn0  25512  dchrinvcl  25515  dchrptlem2  25527  dchrsum2  25530  sum2dchr  25536  lgseisenlem3  25639  lgseisenlem4  25640  rdivmuldivd  30512  ringinvval  30513  dvrcan5  30514  rhmunitinv  30545  iistmd  30758  xrge0iifmhm  30795  xrge0pluscn  30796  pl1cn  30811  isdomn3  39310  mon1psubm  39312  deg1mhm  39313  amgm2d  40058  amgm3d  40059  amgm4d  40060  isringrng  43652  rngcl  43654  isrnghmmul  43664  lidlmmgm  43696  lidlmsgrp  43697  2zrngmmgm  43717  2zrngmsgrp  43718  2zrngnring  43723  cznrng  43726  cznnring  43727  mgpsumunsn  43909  invginvrid  43917  amgmlemALT  44406  amgmw2d  44407