MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ressplusg Structured version   Unicode version

Theorem ressplusg 14721
Description:  +g is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)
Hypotheses
Ref Expression
ressplusg.1  |-  H  =  ( Gs  A )
ressplusg.2  |-  .+  =  ( +g  `  G )
Assertion
Ref Expression
ressplusg  |-  ( A  e.  V  ->  .+  =  ( +g  `  H ) )

Proof of Theorem ressplusg
StepHypRef Expression
1 ressplusg.1 . 2  |-  H  =  ( Gs  A )
2 ressplusg.2 . 2  |-  .+  =  ( +g  `  G )
3 df-plusg 14692 . 2  |-  +g  = Slot  2
4 2nn 10700 . 2  |-  2  e.  NN
5 1lt2 10709 . 2  |-  1  <  2
61, 2, 3, 4, 5resslem 14672 1  |-  ( A  e.  V  ->  .+  =  ( +g  `  H ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    e. wcel 1804   ` cfv 5578  (class class class)co 6281   2c2 10592   ↾s cress 14615   +g cplusg 14679
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-om 6686  df-recs 7044  df-rdg 7078  df-er 7313  df-en 7519  df-dom 7520  df-sdom 7521  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-nn 10544  df-2 10601  df-ndx 14617  df-slot 14618  df-base 14619  df-sets 14620  df-ress 14621  df-plusg 14692
This theorem is referenced by:  gsumress  15882  issubmnd  15927  ress0g  15928  submnd0  15929  resmhm  15969  resmhm2  15970  resmhm2b  15971  submmulg  16156  subg0  16186  subginv  16187  subgcl  16190  subgsub  16192  subgmulg  16194  issubg2  16195  nmznsg  16224  resghm  16262  subgga  16317  gasubg  16319  resscntz  16348  sylow2blem2  16620  sylow3lem6  16631  subglsm  16670  pj1ghm  16700  subgabl  16823  subcmn  16824  submcmn2  16826  ringidss  17204  opprsubg  17264  unitgrp  17295  unitlinv  17305  unitrinv  17306  invrpropd  17326  isdrng2  17385  drngmcl  17388  drngid2  17391  isdrngd  17400  subrgugrp  17427  issubrg2  17428  subrgpropd  17442  abvres  17467  islss3  17584  sralmod  17812  resspsradd  18050  mpladd  18083  ressmpladd  18098  mplplusg  18240  ply1plusg  18245  ressply1add  18250  xrs1mnd  18435  xrs10  18436  xrs1cmn  18437  xrge0subm  18438  cnmsubglem  18459  expmhm  18464  nn0srg  18465  rge0srg  18466  zringplusg  18474  zrngplusg  18480  zlpirlem3  18494  expghm  18507  expghmOLD  18508  mulgghm2OLD  18512  psgnghm  18594  psgnco  18597  evpmodpmf1o  18610  replusg  18624  frlmplusgval  18775  mdetralt  19088  invrvald  19156  submtmd  20581  imasdsf1olem  20854  xrge0gsumle  21316  clmadd  21552  ipcau2  21655  reefgim  22823  efabl  22915  efsubm  22916  dchrptlem2  23518  dchrsum2  23521  qabvle  23788  padicabv  23793  ostth2lem2  23797  ostth3  23801  ressplusf  27616  ressmulgnn  27649  xrge0plusg  27653  submomnd  27678  ringinvval  27760  dvrcan5  27761  rhmunitinv  27790  xrge0slmod  27812  qqhghm  27947  qqhrhm  27948  esumpfinvallem  28058  mzpmfpOLD  30656  cntzsdrg  31127  deg1mhm  31143  cnfldsrngadd  32412  issubmgm2  32432  resmgmhm  32440  resmgmhm2  32441  resmgmhm2b  32442  lidlrng  32560  lcdvadd  37199
  Copyright terms: Public domain W3C validator