Theorem resssca 17395

Description: Scalar is unaffected by restriction. (Contributed by Mario Carneiro, 7-Dec-2014.)

Hypotheses

Ref	Expression
resssca.1	⊢ 𝐻 = (𝐺 ↾s 𝐴)
resssca.2	⊢ 𝐹 = (Scalar‘𝐺)

Assertion

Ref	Expression
resssca	⊢ (𝐴 ∈ 𝑉 → 𝐹 = (Scalar‘𝐻))

Proof of Theorem resssca

Step	Hyp	Ref	Expression
1		resssca.1	. 2 ⊢ 𝐻 = (𝐺 ↾s 𝐴)
2		resssca.2	. 2 ⊢ 𝐹 = (Scalar‘𝐺)
3		scaid 17367	. 2 ⊢ Scalar = Slot (Scalar‘ndx)
4		scandxnbasendx 17368	. 2 ⊢ (Scalar‘ndx) ≠ (Base‘ndx)
5	1, 2, 3, 4	resseqnbas 17293	1 ⊢ (𝐴 ∈ 𝑉 → 𝐹 = (Scalar‘𝐻))

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2107  ‘cfv 6566  (class class class)co 7435   ↾_s cress 17280  Scalarcsca 17307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5303  ax-nul 5313  ax-pow 5372  ax-pr 5439  ax-un 7758  ax-cnex 11215  ax-resscn 11216  ax-1cn 11217  ax-icn 11218  ax-addcl 11219  ax-addrcl 11220  ax-mulcl 11221  ax-mulrcl 11222  ax-mulcom 11223  ax-addass 11224  ax-mulass 11225  ax-distr 11226  ax-i2m1 11227  ax-1ne0 11228  ax-1rid 11229  ax-rnegex 11230  ax-rrecex 11231  ax-cnre 11232  ax-pre-lttri 11233  ax-pre-lttrn 11234  ax-pre-ltadd 11235  ax-pre-mulgt0 11236

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1778  df-nf 1782  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3380  df-rab 3435  df-v 3481  df-sbc 3793  df-csb 3910  df-dif 3967  df-un 3969  df-in 3971  df-ss 3981  df-pss 3984  df-nul 4341  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4914  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5584  df-eprel 5590  df-po 5598  df-so 5599  df-fr 5642  df-we 5644  df-xp 5696  df-rel 5697  df-cnv 5698  df-co 5699  df-dm 5700  df-rn 5701  df-res 5702  df-ima 5703  df-pred 6326  df-ord 6392  df-on 6393  df-lim 6394  df-suc 6395  df-iota 6519  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7392  df-ov 7438  df-oprab 7439  df-mpo 7440  df-om 7892  df-2nd 8020  df-frecs 8311  df-wrecs 8342  df-recs 8416  df-rdg 8455  df-er 8750  df-en 8991  df-dom 8992  df-sdom 8993  df-pnf 11301  df-mnf 11302  df-xr 11303  df-ltxr 11304  df-le 11305  df-sub 11498  df-neg 11499  df-nn 12271  df-2 12333  df-3 12334  df-4 12335  df-5 12336  df-sets 17204  df-slot 17222  df-ndx 17234  df-base 17252  df-ress 17281  df-sca 17320

This theorem is referenced by:  islss3  20981  reslmhm  21075  reslmhm2  21076  reslmhm2b  21077  pj1lmhm  21123  lsslvec  21132  phlssphl  21701  frlmsca  21797  lsslindf  21874  issubassa3  21910  ressascl  21940  mplsca  22057  ply1sca  22276  scmatghm  22561  lssnlm  24744  lssnvc  24745  cphsscph  25307  lssbn  25408  cmslssbn  25428  csschl  25432  rrxsca  25452  xrge0slmod  33369  ply1degltdimlem  33663  fedgmullem2  33671  dimlssid  33673  algextdeglem8  33743  sitmcl  34346  repwsmet  37833  rrnequiv  37834  lcdsca  41594