Theorem ressplusg 17245

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6492  (class class class)co 7360  ndxcnx 17154  Basecbs 17170   ↾_s cress 17191  +_gcplusg 17211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-2 12235  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-ress 17192  df-plusg 17224

This theorem is referenced by:  issstrmgm  18612  gsumress  18641  issubmgm2  18662  resmgmhm  18670  resmgmhm2  18671  resmgmhm2b  18672  issubmnd  18720  ress0g  18721  submnd0  18722  resmhm  18779  resmhm2  18780  resmhm2b  18781  smndex1mgm  18869  smndex1sgrp  18870  smndex1mnd  18872  smndex1id  18873  ressmulgnn  19043  ressmulgnnd  19045  submmulg  19085  subg0  19099  subginv  19100  subgcl  19103  subgsub  19105  subgmulg  19107  issubg2  19108  nmznsg  19134  resghm  19198  subgga  19266  gasubg  19268  resscntz  19299  symgplusg  19349  sylow2blem2  19587  sylow3lem6  19598  subglsm  19639  pj1ghm  19669  subgabl  19802  subcmn  19803  submcmn2  19805  cntrcmnd  19808  cycsubmcmn  19855  submomnd  20098  ringidss  20249  opprsubg  20323  unitgrp  20354  unitlinv  20364  unitrinv  20365  invrpropd  20389  rhmunitinv  20479  issubrng2  20526  subrngpropd  20536  subrgugrp  20559  issubrg2  20560  subrgpropd  20576  isdrng2  20711  drngmclOLD  20719  drngid2  20720  isdrngd  20733  isdrngdOLD  20735  cntzsdrg  20770  abvres  20799  islss3  20945  sralmod  21174  rnglidlrng  21237  rngqiprngghmlem3  21279  cnmsubglem  21420  expmhm  21426  nn0srg  21427  rge0srg  21428  xrge0plusg  21429  xrs1mnd  21430  xrs10  21431  xrs1cmn  21432  xrge0subm  21433  zringplusg  21444  expghm  21465  psgnghm  21570  psgnco  21573  evpmodpmf1o  21586  replusg  21600  phlssphl  21649  frlmplusgval  21754  resspsradd  21963  mplplusg  21995  ressmpladd  22017  mhpmulcl  22125  ply1plusg  22197  ressply1add  22203  evls1addd  22346  mdetralt  22583  invrvald  22651  submtmd  24079  imasdsf1olem  24348  xrge0gsumle  24809  clmadd  25051  isclmp  25074  ipcau2  25211  reefgim  26428  efabl  26527  efsubm  26528  dchrptlem2  27242  dchrsum2  27245  qabvle  27602  padicabv  27607  ostth2lem2  27611  ostth3  27615  ressplusf  33038  ringinvval  33311  dvrcan5  33312  xrge0slmod  33423  idlinsubrg  33506  zringfrac  33629  drgextlsp  33753  fedgmullem2  33790  algextdeglem8  33884  2sqr3minply  33940  cos9thpiminply  33948  qqhghm  34148  qqhrhm  34149  esumpfinvallem  34234  lcdvadd  42057  primrootsunit1  42550  aks6d1c6isolem2  42628  mhphflem  43043  deg1mhm  43646  sge0tsms  46826  cnfldsrngadd  48650  amgmlemALT  50290