Theorem mgpplusg 20391

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 6919	. . . 4 ⊢ · ∈ V
3		plusgid 17481	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17411	. . . 4 ⊢ ((𝑅 ∈ V ∧ · ∈ V) → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
5	2, 4	mpan2 704	. . 3 ⊢ (𝑅 ∈ V → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
6		mgpval.1	. . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅)
7	6, 1	mgpval 20390	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6908	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2816	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17393	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6897	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2810	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6897	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2810	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6909	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2824	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 184	1 ⊢ · = (+g‘𝑀)

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2147  Vcvv 3454  ∅c0 4281  ⟨cop 4838  ‘cfv 6555  (class class class)co 7440   sSet csts 17367  ndxcnx 17397  +_gcplusg 17454  ._rcmulr 17455  mulGrpcmgp 20387

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-cnex 11280  ax-1cn 11282  ax-addcl 11284

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-ov 7443  df-oprab 7444  df-mpo 7445  df-om 7899  df-2nd 8023  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-nn 12360  df-2 12429  df-sets 17368  df-slot 17386  df-ndx 17398  df-plusg 17467  df-mgp 20388

This theorem is used by:  prdsmgp  20398  elmgplsm  20399  rngass  20408  rngcl  20413  isrngd  20422  rngpropd  20423  rng1zrlem  20430  dfur2  20437  srgcl  20446  srgass  20447  srgideu  20448  srgidmlem  20454  issrgid  20457  srgpcomp  20471  srgpcompp  20472  srgbinomlem4  20482  srgbinomlem  20483  csrgbinom  20485  ringcl  20504  crngcom  20505  iscrng2  20506  ringass  20507  ringideu  20508  ringidmlem  20524  isringid  20527  ringidss  20533  isringrng  20543  dfring3  20545  ringpropd  20546  crngpropd  20547  isringd  20549  iscrngd  20550  ring1  20568  gsummgp0  20574  pwspjmhmmgpd  20584  xpsring1d  20590  oppr1  20607  unitgrp  20640  unitlinv  20650  unitrinv  20651  rdivmuldivd  20670  rngidpropd  20672  invrpropd  20675  isrnghmmul  20699  dfrhm2  20731  rhmmul  20747  isrhm2d  20748  rhmunitinv  20788  rhmimasubrnglem  20844  rhmimasubrng  20845  cntzsubrng  20846  subrgugrp  20870  issubrg3  20879  cntzsubr  20885  rhmpropd  20888  isdomn3  20993  isdrng2  21024  isdrng3lem1  21032  isdrng3lem2  21033  drngid2  21037  isdrngd  21049  isdrngdOLD  21051  cntzsdrg  21086  primefld  21089  rlmscaf  21509  rnglidlmmgm  21560  rnglidlmsgrp  21561  rng2idl1cntr  21628  cringm4  21654  ssdifidlprm  21669  prmidlsubm  21670  xrsmcmn  21728  cnfldexp  21738  cnmsubglem  21763  expmhm  21769  nn0srg  21770  rge0srg  21771  expghm  21808  frobrhm  21908  psgnghm  21913  psgnco  21916  evpmodpmf1o  21929  sraassab  22203  assamulgscmlem2  22235  psrcrng  22306  mplcoe3  22374  mplcoe5lem  22375  mplcoe5  22376  mplcoe2  22377  mplbas2  22378  evlslem1  22418  mpfind  22451  selvvvval  22478  mhppwdeg  22498  psdpw  22518  coe1tm  22619  ply1coe  22643  ringvcl  22742  mamuvs2  22748  mat1mhm  22826  scmatmhm  22876  mdetdiaglem  22940  mdetrlin  22944  mdetrsca  22945  mdetralt  22950  mdetunilem7  22960  mdetuni0  22963  m2detleib  22973  invrvald  23018  mat2pmatmhm  23078  pm2mpmhm  23165  chfacfpmmulgsum2  23210  cpmadugsumlemB  23219  cnmpt1mulr  24528  cnmpt2mulr  24529  reefgim  26804  efabl  26905  efsubm  26906  amgm  27345  wilthlem2  27423  wilthlem3  27424  dchrelbas3  27592  dchrzrhmul  27600  dchrmulcl  27603  dchrn0  27604  dchrinvcl  27607  dchrptlem2  27619  dchrsum2  27622  sum2dchr  27628  lgseisenlem3  27731  lgseisenlem4  27732  zsoring  28822  urpropd  33858  ringm1expp1  33861  ringinvval  33862  dvrcan5  33863  isunit3  33868  elrgspnlem2  33871  elrgspnsubrunlem1  33875  elrgspnsubrunlem2  33876  0ringcring  33880  erler  33893  rlocaddval  33897  rlocmulval  33898  rloccring  33899  rlocisunit  33904  domnprodn0  33906  domnprodeq0  33907  rrgsubm  33912  unitprodclb  34011  lsmsnpridl  34018  mxidlprm  34062  rprmdvdspow  34132  rprmdvdsprod  34133  1arithidomlem1  34134  1arithidom  34136  1arithufdlem2  34144  1arithufdlem3  34145  1arithufdlem4  34146  dfufd2lem  34148  zringfrac  34153  deg1prod  34182  psrmonprod  34251  mplmonprod  34253  vietalem  34278  srapwov  34288  assarrginv  34335  evls1fldgencl  34369  iistmd  34601  xrge0iifmhm  34638  xrge0pluscn  34639  pl1cn  34654  zrhcntr  34678  aks6d1c1p4  43352  evl1gprodd  43358  idomnnzpownz  43373  idomnnzgmulnz  43374  ringexp0nn  43375  aks6d1c5lem3  43378  aks6d1c5lem2  43379  deg1gprod  43381  deg1pow  43382  unitscyglem5  43440  domnexpgn0cl  43775  abvexp  43787  fidomncyc  43790  evlselv  43808  mhphf  43816  mon1psubm  44391  deg1mhm  44392  amgm2d  45388  amgm3d  45389  amgm4d  45390  2zrngmmgm  49552  2zrngmsgrp  49553  2zrngnring  49558  cznrng  49561  cznnring  49562  mgpsumunsn  49676  invginvrid  49682  elmgpcntrd  50322  amgmlemALT  51266  amgmw2d  51267