Theorem mgpplusg 20226

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 6895	. . . 4 ⊢ · ∈ V
3		plusgid 17343	. . . . 5 ⊢ +g = Slot (+g‘ndx)
4	3	setsid 17273	. . . 4 ⊢ ((𝑅 ∈ V ∧ · ∈ V) → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
5	2, 4	mpan2 703	. . 3 ⊢ (𝑅 ∈ V → · = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩)))
6		mgpval.1	. . . . 5 ⊢ 𝑀 = (mulGrp‘𝑅)
7	6, 1	mgpval 20225	. . . 4 ⊢ 𝑀 = (𝑅 sSet ⟨(+g‘ndx), · ⟩)
8	7	fveq2i 6884	. . 3 ⊢ (+g‘𝑀) = (+g‘(𝑅 sSet ⟨(+g‘ndx), · ⟩))
9	5, 8	eqtr4di 2815	. 2 ⊢ (𝑅 ∈ V → · = (+g‘𝑀))
10	3	str0 17255	. . 3 ⊢ ∅ = (+g‘∅)
11		fvprc 6873	. . . 4 ⊢ (¬ 𝑅 ∈ V → (.r‘𝑅) = ∅)
12	1, 11	eqtrid 2809	. . 3 ⊢ (¬ 𝑅 ∈ V → · = ∅)
13		fvprc 6873	. . . . 5 ⊢ (¬ 𝑅 ∈ V → (mulGrp‘𝑅) = ∅)
14	6, 13	eqtrid 2809	. . . 4 ⊢ (¬ 𝑅 ∈ V → 𝑀 = ∅)
15	14	fveq2d 6885	. . 3 ⊢ (¬ 𝑅 ∈ V → (+g‘𝑀) = (+g‘∅))
16	10, 12, 15	3eqtr4a 2823	. 2 ⊢ (¬ 𝑅 ∈ V → · = (+g‘𝑀))
17	9, 16	pm2.61i 184	1 ⊢ · = (+g‘𝑀)

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1569   ∈ wcel 2142  Vcvv 3454  ∅c0 4285  ⟨cop 4594  ‘cfv 6536  (class class class)co 7412   sSet csts 17229  ndxcnx 17259  +_gcplusg 17316  ._rcmulr 17317  mulGrpcmgp 20222

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-cnex 11162  ax-1cn 11164  ax-addcl 11166

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7861  df-2nd 7985  df-frecs 8276  df-wrecs 8307  df-recs 8356  df-rdg 8395  df-nn 12240  df-2 12309  df-sets 17230  df-slot 17248  df-ndx 17260  df-plusg 17329  df-mgp 20223

This theorem is used by:  prdsmgp  20233  elmgplsm  20234  rngass  20243  rngcl  20248  isrngd  20257  rngpropd  20258  rng1zrlem  20265  dfur2  20272  srgcl  20281  srgass  20282  srgideu  20283  srgidmlem  20289  issrgid  20292  srgpcomp  20306  srgpcompp  20307  srgbinomlem4  20317  srgbinomlem  20318  csrgbinom  20320  ringcl  20338  crngcom  20339  iscrng2  20340  ringass  20341  ringideu  20342  ringidmlem  20358  isringid  20361  ringidss  20367  isringrng  20377  ringpropd  20378  crngpropd  20379  isringd  20381  iscrngd  20382  ring1  20400  gsummgp0  20406  pwspjmhmmgpd  20416  xpsring1d  20422  oppr1  20439  unitgrp  20472  unitlinv  20482  unitrinv  20483  rdivmuldivd  20502  rngidpropd  20504  invrpropd  20507  isrnghmmul  20531  dfrhm2  20563  rhmmul  20579  isrhm2d  20580  rhmunitinv  20619  rhmimasubrnglem  20675  rhmimasubrng  20676  cntzsubrng  20677  subrgugrp  20701  issubrg3  20710  cntzsubr  20716  rhmpropd  20719  isdomn3  20824  isdrng2  20854  isdrng3lem1  20862  isdrng3lem2  20863  drngid2  20867  isdrngd  20879  isdrngdOLD  20881  cntzsdrg  20916  primefld  20919  rlmscaf  21339  rnglidlmmgm  21390  rnglidlmsgrp  21391  rng2idl1cntr  21456  cringm4  21482  ssdifidlprm  21497  prmidlsubm  21498  xrsmcmn  21556  cnfldexp  21566  cnmsubglem  21591  expmhm  21597  nn0srg  21598  rge0srg  21599  expghm  21636  frobrhm  21736  psgnghm  21741  psgnco  21744  evpmodpmf1o  21757  sraassab  22029  assamulgscmlem2  22061  psrcrng  22132  mplcoe3  22200  mplcoe5lem  22201  mplcoe5  22202  mplcoe2  22203  mplbas2  22204  evlslem1  22244  mpfind  22277  selvvvval  22304  mhppwdeg  22324  psdpw  22344  coe1tm  22445  ply1coe  22469  ringvcl  22568  mamuvs2  22574  mat1mhm  22652  scmatmhm  22702  mdetdiaglem  22766  mdetrlin  22770  mdetrsca  22771  mdetralt  22776  mdetunilem7  22786  mdetuni0  22789  m2detleib  22799  invrvald  22844  mat2pmatmhm  22901  pm2mpmhm  22988  chfacfpmmulgsum2  23033  cpmadugsumlemB  23042  cnmpt1mulr  24350  cnmpt2mulr  24351  reefgim  26624  efabl  26726  efsubm  26727  amgm  27166  wilthlem2  27244  wilthlem3  27245  dchrelbas3  27413  dchrzrhmul  27421  dchrmulcl  27424  dchrn0  27425  dchrinvcl  27428  dchrptlem2  27440  dchrsum2  27443  sum2dchr  27449  lgseisenlem3  27552  lgseisenlem4  27553  zsoring  28613  urpropd  33559  ringm1expp1  33562  ringinvval  33563  dvrcan5  33564  isunit3  33569  elrgspnlem2  33572  elrgspnsubrunlem1  33576  elrgspnsubrunlem2  33577  0ringcring  33581  erler  33594  rlocaddval  33598  rlocmulval  33599  rloccring  33600  rlocisunit  33605  domnprodn0  33607  domnprodeq0  33608  rrgsubm  33613  unitprodclb  33711  lsmsnpridl  33718  mxidlprm  33762  rprmdvdspow  33832  rprmdvdsprod  33833  1arithidomlem1  33834  1arithidom  33836  1arithufdlem2  33844  1arithufdlem3  33845  1arithufdlem4  33846  dfufd2lem  33848  zringfrac  33853  deg1prod  33882  psrmonprod  33951  mplmonprod  33953  vietalem  33978  srapwov  33988  assarrginv  34035  evls1fldgencl  34069  iistmd  34301  xrge0iifmhm  34338  xrge0pluscn  34339  pl1cn  34354  zrhcntr  34378  aks6d1c1p4  42906  evl1gprodd  42912  idomnnzpownz  42927  idomnnzgmulnz  42928  ringexp0nn  42929  aks6d1c5lem3  42932  aks6d1c5lem2  42933  deg1gprod  42935  deg1pow  42936  unitscyglem5  42994  domnexpgn0cl  43319  abvexp  43328  fidomncyc  43331  evlselv  43349  mhphf  43357  mon1psubm  43954  deg1mhm  43955  amgm2d  44952  amgm3d  44953  amgm4d  44954  2zrngmmgm  49045  2zrngmsgrp  49046  2zrngnring  49051  cznrng  49054  cznnring  49055  mgpsumunsn  49169  invginvrid  49175  elmgpcntrd  49811  amgmlemALT  50678  amgmw2d  50679