Metamath Proof Explorer


Theorem resssca

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

Ref Expression
Hypotheses resssca.1 H=G𝑠A
resssca.2 F=ScalarG
Assertion resssca AVF=ScalarH

Proof

Step Hyp Ref Expression
1 resssca.1 H=G𝑠A
2 resssca.2 F=ScalarG
3 scaid Scalar=SlotScalarndx
4 scandxnbasendx ScalarndxBasendx
5 1 2 3 4 resseqnbas AVF=ScalarH