Theorem resvplusg

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

	Ref	Expression
Hypotheses	resvbas.1	$$⊢H=G{\upharpoonright }_{𝑣}A$$
	resvplusg.2	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	resvplusg	$$⊢A\in V\to \underset{\dot{}}{+}={+}_H$$

Proof

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