Metamath Proof Explorer


Theorem resvbas

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

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 df-base Base = Slot 1
4 1nn 1 ∈ ℕ
5 1re 1 ∈ ℝ
6 1lt5 1 < 5
7 5 6 ltneii 1 ≠ 5
8 1 2 3 4 7 resvlem ( 𝐴𝑉𝐵 = ( Base ‘ 𝐻 ) )