Theorem ressmulr 17268

Description: ._r is unaffected by restriction. (Contributed by Stefan O'Rear, 27-Nov-2014.)

Hypotheses

Ref	Expression
ressmulr.1	⊢ 𝑆 = (𝑅 ↾s 𝐴)
ressmulr.2	⊢ · = (.r‘𝑅)

Assertion

Ref	Expression
ressmulr	⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝑆))

Proof of Theorem ressmulr

Step	Hyp	Ref	Expression
1		ressmulr.1	. 2 ⊢ 𝑆 = (𝑅 ↾s 𝐴)
2		ressmulr.2	. 2 ⊢ · = (.r‘𝑅)
3		mulridx 17256	. 2 ⊢ .r = Slot (.r‘ndx)
4		basendxnmulrndx 17257	. . 3 ⊢ (Base‘ndx) ≠ (.r‘ndx)
5	4	necomi 2989	. 2 ⊢ (.r‘ndx) ≠ (Base‘ndx)
6	1, 2, 3, 5	resseqnbas 17210	1 ⊢ (𝐴 ∈ 𝑉 → · = (.r‘𝑆))

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ‘cfv 6492  (class class class)co 7363  ndxcnx 17161  Basecbs 17177   ↾_s cress 17198  ._rcmulr 17219

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 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-cnex 11092  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112  ax-pre-mulgt0 11113

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 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  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 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-om 7814  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-sub 11377  df-neg 11378  df-nn 12173  df-2 12242  df-3 12243  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17178  df-ress 17199  df-mulr 17232

This theorem is referenced by:  mgpress  20129  rdivmuldivd  20391  subrngmcl  20536  issubrng2  20537  subrngpropd  20547  subrg1  20561  subrgdvds  20565  subrguss  20566  subrginv  20567  subrgdv  20568  subrgunit  20569  subrgugrp  20570  issubrg2  20571  subrgpropd  20587  primefld  20784  abvres  20810  suborng  20855  sralmod  21184  rnglidlmmgm  21245  rnglidlmsgrp  21246  rnglidlrng  21247  rngqiprngimfolem  21290  rngqiprnglinlem1  21291  rngqiprngimf1lem  21294  rngqiprngimf1  21300  rngqiprnglin  21302  rng2idl1cntr  21305  rngqiprngfulem5  21315  nn0srg  21419  rge0srg  21420  zringmulr  21439  pzriprnglem6  21468  remulr  21593  issubassa3  21848  resspsrmul  21957  resspsrvsca  21958  mplmulr  21989  ressmplmul  22012  ply1mulr  22217  ressply1mul  22222  evls1muld  22365  dmatcrng  22492  scmatcrng  22511  scmatsrng1  22513  scmatmhm  22524  clmmul  25067  isclmp  25089  cphsubrglem  25169  ipcau2  25226  qabvexp  27614  ostthlem2  27616  padicabv  27618  ostth2lem2  27622  ostth3  27626  ress1r  33321  subrdom  33373  xrge0slmod  33438  idlinsubrg  33521  zringfrac  33644  ressply1evls1  33655  resssra  33778  drgextlsp  33785  fedgmullem1  33820  fedgmullem2  33821  extdg1id  33857  fldextrspunlsplem  33864  2sqr3minply  33971  xrge0iifmhm  34130  qqhrhm  34180  imacrhmcl  43011  cnfldsrngmul  48661  zlidlring  48732  uzlidlring  48733  aacllem  50298