Metamath Proof Explorer


Theorem resvplusg

Description: +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018) (Revised by AV, 31-Oct-2024)

Ref Expression
Hypotheses resvbas.1
|- H = ( G |`v A )
resvplusg.2
|- .+ = ( +g ` G )
Assertion resvplusg
|- ( A e. V -> .+ = ( +g ` H ) )

Proof

Step Hyp Ref Expression
1 resvbas.1
 |-  H = ( G |`v A )
2 resvplusg.2
 |-  .+ = ( +g ` G )
3 plusgid
 |-  +g = Slot ( +g ` ndx )
4 scandxnplusgndx
 |-  ( Scalar ` ndx ) =/= ( +g ` ndx )
5 4 necomi
 |-  ( +g ` ndx ) =/= ( Scalar ` ndx )
6 1 2 3 5 resvlem
 |-  ( A e. V -> .+ = ( +g ` H ) )