Theorem resvbas

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

	Ref	Expression
Hypotheses	resvbas.1	$$⊢H=G{\upharpoonright }_{𝑣}A$$
	resvbas.2	$$⊢B={\mathrm{Base}}_G$$
Assertion	resvbas	$$⊢A\in V\to B={\mathrm{Base}}_H$$

Proof

Step	Hyp	Ref	Expression
1		resvbas.1	$$⊢H=G{\upharpoonright }_{𝑣}A$$
2		resvbas.2	$$⊢B={\mathrm{Base}}_G$$
3		df-base	$$⊢\mathrm{Base}=\mathrm{Slot}1$$
4		1nn	$$⊢1\in \mathbb{N}$$
5		1re	$$⊢1\in ℝ$$
6		1lt5	$$⊢1<5$$
7	5 6	ltneii	$$⊢1\ne 5$$
8	1 2 3 4 7	resvlem	$$⊢A\in V\to B={\mathrm{Base}}_H$$