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 | ⊢ 𝑊 = ( ℤMod ‘ 𝐺 ) | |
| zlmplusg.2 | ⊢ + = ( +g ‘ 𝐺 ) | ||
| Assertion | zlmplusg | ⊢ + = ( +g ‘ 𝑊 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zlmbas.w | ⊢ 𝑊 = ( ℤMod ‘ 𝐺 ) | |
| 2 | zlmplusg.2 | ⊢ + = ( +g ‘ 𝐺 ) | |
| 3 | plusgid | ⊢ +g = Slot ( +g ‘ ndx ) | |
| 4 | scandxnplusgndx | ⊢ ( Scalar ‘ ndx ) ≠ ( +g ‘ ndx ) | |
| 5 | 4 | necomi | ⊢ ( +g ‘ ndx ) ≠ ( Scalar ‘ ndx ) |
| 6 | vscandxnplusgndx | ⊢ ( ·𝑠 ‘ ndx ) ≠ ( +g ‘ ndx ) | |
| 7 | 6 | necomi | ⊢ ( +g ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) |
| 8 | 1 3 5 7 | zlmlem | ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝑊 ) |
| 9 | 2 8 | eqtri | ⊢ + = ( +g ‘ 𝑊 ) |