Theorem mgpplusg 19312

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 6673	. . . 4 ⊢ · ∈ V
3		plusgid 16655	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 16597	. . . 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 19311	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6662	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2812	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 16594	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6651	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	syl5eq 2806	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6651	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	syl5eq 2806	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6663	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2820	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 185	1 ⊢ · = (+g‘𝑀)

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2112  Vcvv 3410  ∅c0 4226  ⟨cop 4529  ‘cfv 6336  (class class class)co 7151  ndxcnx 16539   sSet csts 16540  +_gcplusg 16624  ._rcmulr 16625  mulGrpcmgp 19308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10632  ax-1cn 10634  ax-addcl 10636

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7581  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-nn 11676  df-2 11738  df-ndx 16545  df-slot 16546  df-sets 16549  df-plusg 16637  df-mgp 19309

This theorem is referenced by:  dfur2  19323  srgcl  19331  srgass  19332  srgideu  19333  srgidmlem  19339  issrgid  19342  srg1zr  19348  srgpcomp  19351  srgpcompp  19352  srgbinomlem4  19362  srgbinomlem  19363  csrgbinom  19365  ringcl  19383  crngcom  19384  iscrng2  19385  ringass  19386  ringideu  19387  ringidmlem  19392  isringid  19395  ringidss  19399  ringpropd  19404  crngpropd  19405  isringd  19407  iscrngd  19408  ring1  19424  gsummgp0  19430  prdsmgp  19432  oppr1  19456  unitgrp  19489  unitlinv  19499  unitrinv  19500  rngidpropd  19517  invrpropd  19520  dfrhm2  19541  rhmmul  19551  isrhm2d  19552  isdrng2  19581  drngmcl  19584  drngid2  19587  isdrngd  19596  subrgugrp  19623  issubrg3  19632  cntzsubr  19637  rhmpropd  19640  cntzsdrg  19650  primefld  19653  rlmscaf  20050  xrsmcmn  20190  cnfldexp  20200  cnmsubglem  20230  expmhm  20236  nn0srg  20237  rge0srg  20238  expghm  20266  psgnghm  20346  psgnco  20349  evpmodpmf1o  20362  sraassa  20633  assamulgscmlem2  20664  psrcrng  20742  mplcoe3  20799  mplcoe5lem  20800  mplcoe5  20801  mplcoe2  20802  mplbas2  20803  evlslem1  20846  mpfind  20871  mhppwdeg  20894  coe1tm  20998  ply1coe  21021  ringvcl  21101  mamuvs2  21107  mat1mhm  21185  scmatmhm  21235  mdetdiaglem  21299  mdetrlin  21303  mdetrsca  21304  mdetralt  21309  mdetunilem7  21319  mdetuni0  21322  m2detleib  21332  invrvald  21377  mat2pmatmhm  21434  pm2mpmhm  21521  chfacfpmmulgsum2  21566  cpmadugsumlemB  21575  cnmpt1mulr  22883  cnmpt2mulr  22884  reefgim  25145  efabl  25242  efsubm  25243  amgm  25676  wilthlem2  25754  wilthlem3  25755  dchrelbas3  25922  dchrzrhmul  25930  dchrmulcl  25933  dchrn0  25934  dchrinvcl  25937  dchrptlem2  25949  dchrsum2  25952  sum2dchr  25958  lgseisenlem3  26061  lgseisenlem4  26062  frobrhm  31012  rdivmuldivd  31015  ringinvval  31016  dvrcan5  31017  rhmunitinv  31048  elringlsm  31103  lsmsnpridl  31108  cringm4  31144  mxidlprm  31162  iistmd  31374  xrge0iifmhm  31411  xrge0pluscn  31412  pl1cn  31427  pwspjmhmmgpd  39775  mhphf  39791  isdomn3  40522  mon1psubm  40524  deg1mhm  40525  amgm2d  41278  amgm3d  41279  amgm4d  41280  isringrng  44873  rngcl  44875  isrnghmmul  44885  lidlmmgm  44917  lidlmsgrp  44918  2zrngmmgm  44938  2zrngmsgrp  44939  2zrngnring  44944  cznrng  44947  cznnring  44948  mgpsumunsn  45131  invginvrid  45137  amgmlemALT  45723  amgmw2d  45724