Theorem resvplusg

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

	Ref	Expression
Hypotheses	resvbas.1	|- H = ( G |`v A )
	resvplusg.2	|- .+ = ( +g ` G )
Assertion	resvplusg	|- ( A e. V -> .+ = ( +g ` H ) )

Proof

Step	Hyp	Ref	Expression
1		resvbas.1	|- H = ( G |`v A )
2		resvplusg.2	|- .+ = ( +g ` G )
3		df-plusg	|- +g = Slot 2
4		2nn	|- 2 e. NN
5		2re	|- 2 e. RR
6		2lt5	|- 2 < 5
7	5 6	ltneii	|- 2 =/= 5
8	1 2 3 4 7	resvlem	|- ( A e. V -> .+ = ( +g ` H ) )