Theorem ressplusg 17311

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 17304	. 2 ⊢ +g = Slot (+g‘ndx)
4		basendxnplusgndx 17307	. . 3 ⊢ (Base‘ndx) ≠ (+g‘ndx)
5	4	necomi 3010	. 2 ⊢ (+g‘ndx) ≠ (Base‘ndx)
6	1, 2, 3, 5	resseqnbas 17269	1 ⊢ (𝐴 ∈ 𝑉 → + = (+g‘𝐻))

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  ‘cfv 6516  (class class class)co 7391  ndxcnx 17220  Basecbs 17236   ↾_s cress 17257  +_gcplusg 17277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-cnex 11123  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143  ax-pre-mulgt0 11144

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7348  df-ov 7394  df-oprab 7395  df-mpo 7396  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216  df-sub 11410  df-neg 11411  df-nn 12205  df-2 12274  df-sets 17191  df-slot 17209  df-ndx 17221  df-base 17237  df-ress 17258  df-plusg 17290

This theorem is referenced by:  issstrmgm  18678  gsumress  18707  issubmgm2  18728  resmgmhm  18736  resmgmhm2  18737  resmgmhm2b  18738  issubmnd  18786  ress0g  18787  submnd0  18788  resmhm  18845  resmhm2  18846  resmhm2b  18847  smndex1mgm  18935  smndex1sgrp  18936  smndex1mnd  18938  smndex1id  18939  ressmulgnn  19109  ressmulgnnd  19111  submmulg  19151  subg0  19165  subginv  19166  subgcl  19169  subgsub  19171  subgmulg  19173  issubg2  19174  nmznsg  19200  resghm  19263  subgga  19331  gasubg  19333  resscntz  19364  symgplusg  19414  sylow2blem2  19652  sylow3lem6  19663  subglsm  19704  pj1ghm  19734  subgabl  19867  subcmn  19868  submcmn2  19870  cntrcmnd  19873  cycsubmcmn  19920  submomnd  20163  ringidss  20314  opprsubg  20388  unitgrp  20419  unitlinv  20429  unitrinv  20430  invrpropd  20454  rhmunitinv  20548  issubrng2  20595  subrngpropd  20605  subrgugrp  20628  issubrg2  20629  subrgpropd  20645  isdrng2  20780  drngmclOLD  20788  drngid2  20789  isdrngd  20802  isdrngdOLD  20804  cntzsdrg  20839  abvres  20868  islss3  21014  sralmod  21242  rnglidlrng  21305  rngqiprngghmlem3  21347  cnmsubglem  21470  expmhm  21476  nn0srg  21477  rge0srg  21478  xrge0plusg  21479  xrs1mnd  21480  xrs10  21481  xrs1cmn  21482  xrge0subm  21483  zringplusg  21494  expghm  21515  psgnghm  21620  psgnco  21623  evpmodpmf1o  21636  replusg  21650  phlssphl  21699  frlmplusgval  21804  resspsradd  22014  mplplusg  22046  ressmpladd  22069  mhpmulcl  22202  ply1plusg  22273  ressply1add  22279  evls1addd  22422  mdetralt  22656  invrvald  22724  submtmd  24152  imasdsf1olem  24421  xrge0gsumle  24882  clmadd  25124  isclmp  25147  ipcau2  25284  reefgim  26501  efabl  26603  efsubm  26604  dchrptlem2  27317  dchrsum2  27320  qabvle  27677  padicabv  27682  ostth2lem2  27686  ostth3  27690  ressplusf  33102  ringinvval  33376  dvrcan5  33377  xrge0slmod  33495  idlinsubrg  33578  zringfrac  33711  drgextlsp  33852  fedgmullem2  33888  algextdeglem8  33982  2sqr3minply  34038  cos9thpiminply  34046  qqhghm  34246  qqhrhm  34247  esumpfinvallem  34332  lcdvadd  42182  primrootsunit1  42675  aks6d1c6isolem2  42753  mhphflem  43139  deg1mhm  43738  sge0tsms  46915  cnfldsrngadd  48745  amgmlemALT  50385