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 𝐻 = ( 𝐺v 𝐴 )
resvbas.2 𝐵 = ( Base ‘ 𝐺 )
Assertion resvbas ( 𝐴𝑉𝐵 = ( Base ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 resvbas.1 𝐻 = ( 𝐺v 𝐴 )
2 resvbas.2 𝐵 = ( Base ‘ 𝐺 )
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 ( 𝐴𝑉𝐵 = ( Base ‘ 𝐻 ) )