Theorem ressplusg 17303

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ‘cfv 6530  (class class class)co 7403  ndxcnx 17210  Basecbs 17226   ↾_s cress 17249  +_gcplusg 17269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-om 7860  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-nn 12239  df-2 12301  df-sets 17181  df-slot 17199  df-ndx 17211  df-base 17227  df-ress 17250  df-plusg 17282

This theorem is referenced by:  issstrmgm  18629  gsumress  18658  issubmgm2  18679  resmgmhm  18687  resmgmhm2  18688  resmgmhm2b  18689  issubmnd  18737  ress0g  18738  submnd0  18739  resmhm  18796  resmhm2  18797  resmhm2b  18798  smndex1mgm  18883  smndex1sgrp  18884  smndex1mnd  18886  smndex1id  18887  ressmulgnn  19057  ressmulgnnd  19059  submmulg  19099  subg0  19113  subginv  19114  subgcl  19117  subgsub  19119  subgmulg  19121  issubg2  19122  nmznsg  19149  resghm  19213  subgga  19281  gasubg  19283  resscntz  19314  symgplusg  19362  sylow2blem2  19600  sylow3lem6  19611  subglsm  19652  pj1ghm  19682  subgabl  19815  subcmn  19816  submcmn2  19818  cntrcmnd  19821  cycsubmcmn  19868  ringidss  20235  opprsubg  20310  unitgrp  20341  unitlinv  20351  unitrinv  20352  invrpropd  20376  rhmunitinv  20469  issubrng2  20516  subrngpropd  20526  subrgugrp  20549  issubrg2  20550  subrgpropd  20566  isdrng2  20701  drngmclOLD  20709  drngid2  20710  isdrngd  20723  isdrngdOLD  20725  cntzsdrg  20760  abvres  20789  islss3  20914  sralmod  21143  rnglidlrng  21206  rngqiprngghmlem3  21248  xrs1mnd  21370  xrs10  21371  xrs1cmn  21372  xrge0subm  21373  cnmsubglem  21396  expmhm  21402  nn0srg  21403  rge0srg  21404  zringplusg  21413  expghm  21434  psgnghm  21538  psgnco  21541  evpmodpmf1o  21554  replusg  21568  phlssphl  21617  frlmplusgval  21722  resspsradd  21933  mplplusg  21965  ressmpladd  21985  mhpmulcl  22085  ply1plusg  22157  ressply1add  22163  evls1addd  22307  mdetralt  22544  invrvald  22612  submtmd  24040  imasdsf1olem  24310  xrge0gsumle  24771  clmadd  25023  isclmp  25046  ipcau2  25184  reefgim  26410  efabl  26509  efsubm  26510  dchrptlem2  27226  dchrsum2  27229  qabvle  27586  padicabv  27591  ostth2lem2  27595  ostth3  27599  ressplusf  32885  xrge0plusg  32954  submomnd  33024  ringinvval  33176  dvrcan5  33177  xrge0slmod  33309  idlinsubrg  33392  zringfrac  33515  drgextlsp  33579  fedgmullem2  33616  algextdeglem8  33704  2sqr3minply  33760  cos9thpiminply  33768  qqhghm  33965  qqhrhm  33966  esumpfinvallem  34051  lcdvadd  41562  primrootsunit1  42056  aks6d1c6isolem2  42134  mhphflem  42566  deg1mhm  43171  sge0tsms  46357  cnfldsrngadd  48085  amgmlemALT  49615