Theorem ressplusg 16926

Description: +_g is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)

Hypotheses

Ref	Expression
ressplusg.1	⊢ 𝐻 = (𝐺 ↾s 𝐴)
ressplusg.2	⊢ + = (+g‘𝐺)

Assertion

Ref	Expression
ressplusg	⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻))

Proof of Theorem ressplusg

Step	Hyp	Ref	Expression
1		ressplusg.1	. 2 ⊢ 𝐻 = (𝐺 ↾s 𝐴)
2		ressplusg.2	. 2 ⊢ + = (+g‘𝐺)
3		plusgid 16915	. 2 ⊢ +g = Slot (+g‘ndx)
4		basendxnplusgndx 16918	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
5	4	necomi 2997	. 2 ⊢ (+g‘ndx) ≠ (Base‘ndx)
6	1, 2, 3, 5	resseqnbas 16877	1 ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻))

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  ‘cfv 6418  (class class class)co 7255  ndxcnx 16822  Basecbs 16840   ↾_s cress 16867  +_gcplusg 16888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904  df-2 11966  df-sets 16793  df-slot 16811  df-ndx 16823  df-base 16841  df-ress 16868  df-plusg 16901

This theorem is referenced by:  issstrmgm  18252  gsumress  18281  issubmnd  18327  ress0g  18328  submnd0  18329  resmhm  18374  resmhm2  18375  resmhm2b  18376  smndex1mgm  18461  smndex1sgrp  18462  smndex1mnd  18464  smndex1id  18465  submmulg  18662  subg0  18676  subginv  18677  subgcl  18680  subgsub  18682  subgmulg  18684  issubg2  18685  nmznsg  18711  resghm  18765  subgga  18821  gasubg  18823  resscntz  18853  symgplusg  18905  sylow2blem2  19141  sylow3lem6  19152  subglsm  19194  pj1ghm  19224  subgabl  19352  subcmn  19353  submcmn2  19355  cntrcmnd  19358  cycsubmcmn  19404  ringidss  19731  opprsubg  19793  unitgrp  19824  unitlinv  19834  unitrinv  19835  invrpropd  19855  isdrng2  19916  drngmcl  19919  drngid2  19922  isdrngd  19931  subrgugrp  19958  issubrg2  19959  subrgpropd  19974  cntzsdrg  19985  abvres  20014  islss3  20136  sralmod  20370  xrs1mnd  20548  xrs10  20549  xrs1cmn  20550  xrge0subm  20551  cnmsubglem  20573  expmhm  20579  nn0srg  20580  rge0srg  20581  zringplusg  20589  expghm  20609  psgnghm  20697  psgnco  20700  evpmodpmf1o  20713  replusg  20727  phlssphl  20776  frlmplusgval  20881  resspsradd  21095  mpladd  21123  ressmpladd  21140  mhpmulcl  21249  mplplusg  21301  ply1plusg  21306  ressply1add  21311  mdetralt  21665  invrvald  21733  submtmd  23163  imasdsf1olem  23434  xrge0gsumle  23902  clmadd  24143  isclmp  24166  ipcau2  24303  reefgim  25514  efabl  25611  efsubm  25612  dchrptlem2  26318  dchrsum2  26321  qabvle  26678  padicabv  26683  ostth2lem2  26687  ostth3  26691  ressplusf  31137  ressmulgnn  31194  xrge0plusg  31198  submomnd  31238  ringinvval  31391  dvrcan5  31392  rhmunitinv  31423  xrge0slmod  31450  idlinsubrg  31510  drgextlsp  31583  fedgmullem2  31613  qqhghm  31838  qqhrhm  31839  esumpfinvallem  31942  lcdvadd  39538  mhphflem  40207  deg1mhm  40948  sge0tsms  43808  cnfldsrngadd  45212  issubmgm2  45232  resmgmhm  45240  resmgmhm2  45241  resmgmhm2b  45242  lidlrng  45373  amgmlemALT  46393