Metamath Proof Explorer


Theorem resvmulr

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

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 mulridx โŠข .r = Slot ( .r โ€˜ ndx )
4 scandxnmulrndx โŠข ( Scalar โ€˜ ndx ) โ‰  ( .r โ€˜ ndx )
5 4 necomi โŠข ( .r โ€˜ ndx ) โ‰  ( Scalar โ€˜ ndx )
6 1 2 3 5 resvlem โŠข ( ๐ด โˆˆ ๐‘‰ โ†’ ยท = ( .r โ€˜ ๐ป ) )