# Metamath Proof Explorer

## Theorem zlmnm

Description: Norm of a ZZ -module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017)

Ref Expression
Hypotheses zlmlem2.1 ${⊢}{W}=\mathrm{ℤMod}\left({G}\right)$
zlmnm.1 ${⊢}{N}=\mathrm{norm}\left({G}\right)$
Assertion zlmnm ${⊢}{G}\in {V}\to {N}=\mathrm{norm}\left({W}\right)$

### Proof

Step Hyp Ref Expression
1 zlmlem2.1 ${⊢}{W}=\mathrm{ℤMod}\left({G}\right)$
2 zlmnm.1 ${⊢}{N}=\mathrm{norm}\left({G}\right)$
3 eqid ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
4 1 3 zlmbas ${⊢}{\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{W}}$
5 4 a1i ${⊢}{G}\in {V}\to {\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{W}}$
6 eqid ${⊢}{+}_{{G}}={+}_{{G}}$
7 1 6 zlmplusg ${⊢}{+}_{{G}}={+}_{{W}}$
8 7 a1i ${⊢}{G}\in {V}\to {+}_{{G}}={+}_{{W}}$
9 eqid ${⊢}\mathrm{dist}\left({G}\right)=\mathrm{dist}\left({G}\right)$
10 1 9 zlmds ${⊢}{G}\in {V}\to \mathrm{dist}\left({G}\right)=\mathrm{dist}\left({W}\right)$
11 5 8 10 nmpropd ${⊢}{G}\in {V}\to \mathrm{norm}\left({G}\right)=\mathrm{norm}\left({W}\right)$
12 2 11 syl5eq ${⊢}{G}\in {V}\to {N}=\mathrm{norm}\left({W}\right)$