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 โ ๐ป ) ) |
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 โ ๐ป ) ) |