Metamath Proof Explorer


Theorem resvvsca

Description: .s is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018)

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 df-vsca
 |-  .s = Slot 6
4 6nn
 |-  6 e. NN
5 5re
 |-  5 e. RR
6 5lt6
 |-  5 < 6
7 5 6 gtneii
 |-  6 =/= 5
8 1 2 3 4 7 resvlem
 |-  ( A e. V -> .x. = ( .s ` H ) )