Theorem resvvsca

Description: .s is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018) (Proof shortened by AV, 31-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		resvbas.1	$$⊢H=G{\upharpoonright }_{𝑣}A$$
2		resvvsca.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		vscaid	$$⊢{\cdot }_{𝑠}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$
4		vscandxnscandx	$$⊢{\cdot }_{\mathrm{ndx}}\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$$
5	1 2 3 4	resvlem	$$⊢A\in V\to \underset{\dot{}}{·}={\cdot }_H$$