Theorem resvplusg

Description: +g 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{\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		plusgid	$$⊢{+}_{𝑔}=\mathrm{Slot}{+}_{\mathrm{ndx}}$$
4		scandxnplusgndx	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}$$
5	4	necomi	$$⊢{+}_{\mathrm{ndx}}\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$$
6	1 2 3 5	resvlem	$$⊢A\in V\to \underset{\dot{}}{+}={+}_H$$