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