Metamath Proof Explorer


Theorem resvbas

Description: Base 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 )
resvbas.2
|- B = ( Base ` G )
Assertion resvbas
|- ( A e. V -> B = ( Base ` H ) )

Proof

Step Hyp Ref Expression
1 resvbas.1
 |-  H = ( G |`v A )
2 resvbas.2
 |-  B = ( Base ` G )
3 baseid
 |-  Base = Slot ( Base ` ndx )
4 scandxnbasendx
 |-  ( Scalar ` ndx ) =/= ( Base ` ndx )
5 4 necomi
 |-  ( Base ` ndx ) =/= ( Scalar ` ndx )
6 1 2 3 5 resvlem
 |-  ( A e. V -> B = ( Base ` H ) )