Metamath Proof Explorer


Theorem zlmmulr

Description: Ring operation of a ZZ -module (if present). (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 3-Nov-2024)

Ref Expression
Hypotheses zlmbas.w โŠข ๐‘Š = ( โ„คMod โ€˜ ๐บ )
zlmmulr.2 โŠข ยท = ( .r โ€˜ ๐บ )
Assertion zlmmulr ยท = ( .r โ€˜ ๐‘Š )

Proof

Step Hyp Ref Expression
1 zlmbas.w โŠข ๐‘Š = ( โ„คMod โ€˜ ๐บ )
2 zlmmulr.2 โŠข ยท = ( .r โ€˜ ๐บ )
3 mulrid โŠข .r = Slot ( .r โ€˜ ndx )
4 scandxnmulrndx โŠข ( Scalar โ€˜ ndx ) โ‰  ( .r โ€˜ ndx )
5 4 necomi โŠข ( .r โ€˜ ndx ) โ‰  ( Scalar โ€˜ ndx )
6 vscandxnmulrndx โŠข ( ยท๐‘  โ€˜ ndx ) โ‰  ( .r โ€˜ ndx )
7 6 necomi โŠข ( .r โ€˜ ndx ) โ‰  ( ยท๐‘  โ€˜ ndx )
8 1 3 5 7 zlmlem โŠข ( .r โ€˜ ๐บ ) = ( .r โ€˜ ๐‘Š )
9 2 8 eqtri โŠข ยท = ( .r โ€˜ ๐‘Š )