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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ‘cfv 6485  (class class class)co 7356  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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  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 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  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  20483  issubrng2  20530  subrngpropd  20540  subrgugrp  20563  issubrg2  20564  subrgpropd  20580  isdrng2  20715  drngmclOLD  20723  drngid2  20724  isdrngd  20737  isdrngdOLD  20739  cntzsdrg  20774  abvres  20803  islss3  20949  sralmod  21177  rnglidlrng  21240  rngqiprngghmlem3  21282  cnmsubglem  21405  expmhm  21411  nn0srg  21412  rge0srg  21413  xrge0plusg  21414  xrs1mnd  21415  xrs10  21416  xrs1cmn  21417  xrge0subm  21418  zringplusg  21429  expghm  21450  psgnghm  21555  psgnco  21558  evpmodpmf1o  21571  replusg  21585  phlssphl  21634  frlmplusgval  21739  resspsradd  21949  mplplusg  21981  ressmpladd  22004  mhpmulcl  22137  ply1plusg  22208  ressply1add  22214  evls1addd  22357  mdetralt  22591  invrvald  22659  submtmd  24087  imasdsf1olem  24356  xrge0gsumle  24817  clmadd  25059  isclmp  25082  ipcau2  25219  reefgim  26433  efabl  26532  efsubm  26533  dchrptlem2  27246  dchrsum2  27249  qabvle  27606  padicabv  27611  ostth2lem2  27615  ostth3  27619  ressplusf  33042  ringinvval  33316  dvrcan5  33317  xrge0slmod  33431  idlinsubrg  33514  zringfrac  33637  drgextlsp  33778  fedgmullem2  33814  algextdeglem8  33908  2sqr3minply  33964  cos9thpiminply  33972  qqhghm  34172  qqhrhm  34173  esumpfinvallem  34258  lcdvadd  42089  primrootsunit1  42582  aks6d1c6isolem2  42660  mhphflem  43046  deg1mhm  43645  sge0tsms  46823  cnfldsrngadd  48653  amgmlemALT  50293