Metamath Proof Explorer


Theorem zlmplusg

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

Ref Expression
Hypotheses zlmbas.w W = ℤMod G
zlmplusg.2 + ˙ = + G
Assertion zlmplusg + ˙ = + W

Proof

Step Hyp Ref Expression
1 zlmbas.w W = ℤMod G
2 zlmplusg.2 + ˙ = + G
3 plusgid + 𝑔 = Slot + ndx
4 scandxnplusgndx Scalar ndx + ndx
5 4 necomi + ndx Scalar ndx
6 vscandxnplusgndx ndx + ndx
7 6 necomi + ndx ndx
8 1 3 5 7 zlmlem + G = + W
9 2 8 eqtri + ˙ = + W