Metamath Proof Explorer


Theorem resvvsca

Description: .s is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018) (Proof shortened by AV, 31-Oct-2024)

Ref Expression
Hypotheses resvbas.1
|- H = ( G |`v A )
resvvsca.2
|- .x. = ( .s ` G )
Assertion resvvsca
|- ( A e. V -> .x. = ( .s ` H ) )

Proof

Step Hyp Ref Expression
1 resvbas.1
 |-  H = ( G |`v A )
2 resvvsca.2
 |-  .x. = ( .s ` G )
3 vscaid
 |-  .s = Slot ( .s ` ndx )
4 vscandxnscandx
 |-  ( .s ` ndx ) =/= ( Scalar ` ndx )
5 1 2 3 4 resvlem
 |-  ( A e. V -> .x. = ( .s ` H ) )