Metamath Proof Explorer


Theorem resvmulr

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

Ref Expression
Hypotheses resvbas.1 𝐻 = ( 𝐺v 𝐴 )
resvmulr.2 · = ( .r𝐺 )
Assertion resvmulr ( 𝐴𝑉· = ( .r𝐻 ) )

Proof

Step Hyp Ref Expression
1 resvbas.1 𝐻 = ( 𝐺v 𝐴 )
2 resvmulr.2 · = ( .r𝐺 )
3 df-mulr .r = 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 ( 𝐴𝑉· = ( .r𝐻 ) )