Theorem zlmnm

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

	Ref	Expression
Hypotheses	zlmlem2.1	$$⊢W=\mathrm{\mathbb{Z}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{\mathbb{Z}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)$$