Metamath Proof Explorer
Description: Base set of a ZZ module. (Contributed by Mario Carneiro, 2Oct2015)


Ref 
Expression 

Hypotheses 
zlmbas.w 
⊢ 𝑊 = ( ℤMod ‘ 𝐺 ) 


zlmbas.2 
⊢ 𝐵 = ( Base ‘ 𝐺 ) 

Assertion 
zlmbas 
⊢ 𝐵 = ( Base ‘ 𝑊 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

zlmbas.w 
⊢ 𝑊 = ( ℤMod ‘ 𝐺 ) 
2 

zlmbas.2 
⊢ 𝐵 = ( Base ‘ 𝐺 ) 
3 

dfbase 
⊢ Base = Slot 1 
4 

1nn 
⊢ 1 ∈ ℕ 
5 

1lt5 
⊢ 1 < 5 
6 
1 3 4 5

zlmlem 
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝑊 ) 
7 
2 6

eqtri 
⊢ 𝐵 = ( Base ‘ 𝑊 ) 