Metamath Proof Explorer


Theorem resvbas

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

Ref Expression
Hypotheses resvbas.1 H = G 𝑣 A
resvbas.2 B = Base G
Assertion resvbas A V B = Base H

Proof

Step Hyp Ref Expression
1 resvbas.1 H = G 𝑣 A
2 resvbas.2 B = Base G
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 A V B = Base H