Theorem zlmnm

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

	Ref	Expression
Hypotheses	zlmlem2.1	|- W = ( ZMod ` G )
	zlmnm.1	|- N = ( norm ` G )
Assertion	zlmnm	|- ( G e. V -> N = ( norm ` W ) )

Proof

Step	Hyp	Ref	Expression
1		zlmlem2.1	|- W = ( ZMod ` G )
2		zlmnm.1	|- N = ( norm ` G )
3		eqid	|- ( Base ` G ) = ( Base ` G )
4	1 3	zlmbas	|- ( Base ` G ) = ( Base ` W )
5	4	a1i	|- ( G e. V -> ( Base ` G ) = ( Base ` W ) )
6		eqid	|- ( +g ` G ) = ( +g ` G )
7	1 6	zlmplusg	|- ( +g ` G ) = ( +g ` W )
8	7	a1i	|- ( G e. V -> ( +g ` G ) = ( +g ` W ) )
9		eqid	|- ( dist ` G ) = ( dist ` G )
10	1 9	zlmds	|- ( G e. V -> ( dist ` G ) = ( dist ` W ) )
11	5 8 10	nmpropd	|- ( G e. V -> ( norm ` G ) = ( norm ` W ) )
12	2 11	syl5eq	|- ( G e. V -> N = ( norm ` W ) )