Step 
Hyp 
Ref 
Expression 
1 

zlmlem2.1 
⊢ 𝑊 = ( ℤMod ‘ 𝐺 ) 
2 

zlmnm.1 
⊢ 𝑁 = ( norm ‘ 𝐺 ) 
3 

eqid 
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) 
4 
1 3

zlmbas 
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝑊 ) 
5 
4

a1i 
⊢ ( 𝐺 ∈ 𝑉 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝑊 ) ) 
6 

eqid 
⊢ ( +_{g} ‘ 𝐺 ) = ( +_{g} ‘ 𝐺 ) 
7 
1 6

zlmplusg 
⊢ ( +_{g} ‘ 𝐺 ) = ( +_{g} ‘ 𝑊 ) 
8 
7

a1i 
⊢ ( 𝐺 ∈ 𝑉 → ( +_{g} ‘ 𝐺 ) = ( +_{g} ‘ 𝑊 ) ) 
9 

eqid 
⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 ) 
10 
1 9

zlmds 
⊢ ( 𝐺 ∈ 𝑉 → ( dist ‘ 𝐺 ) = ( dist ‘ 𝑊 ) ) 
11 
5 8 10

nmpropd 
⊢ ( 𝐺 ∈ 𝑉 → ( norm ‘ 𝐺 ) = ( norm ‘ 𝑊 ) ) 
12 
2 11

syl5eq 
⊢ ( 𝐺 ∈ 𝑉 → 𝑁 = ( norm ‘ 𝑊 ) ) 