Theorem resvmulrOLD

Description: Obsolete proof of resvmulr as of 31-Oct-2024. .s is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

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