Metamath Proof Explorer


Theorem resvmulr

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

Ref Expression
Hypotheses resvbas.1 H = G 𝑣 A
resvmulr.2 · ˙ = G
Assertion resvmulr A V · ˙ = H

Proof

Step Hyp Ref Expression
1 resvbas.1 H = G 𝑣 A
2 resvmulr.2 · ˙ = G
3 df-mulr 𝑟 = Slot 3
4 3nn 3
5 3re 3
6 3lt5 3 < 5
7 5 6 ltneii 3 5
8 1 2 3 4 7 resvlem A V · ˙ = H