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 ‘ 𝐻 ) ) |
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 ‘ 𝐻 ) ) |