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 ) ) 