Metamath Proof Explorer
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 |
|
|
|
zlmplusg.2 |
|
|
Assertion |
zlmplusg |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
zlmbas.w |
|
2 |
|
zlmplusg.2 |
|
3 |
|
plusgid |
|
4 |
|
scandxnplusgndx |
|
5 |
4
|
necomi |
|
6 |
|
vscandxnplusgndx |
|
7 |
6
|
necomi |
|
8 |
1 3 5 7
|
zlmlem |
|
9 |
2 8
|
eqtri |
|