This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ↾ 𝑣 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 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 ∈ V → B = Base H