Metamath Proof Explorer

Theorem znhash

Description: The Z/nZ structure has n elements. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypotheses zntos.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
znhash.1 ⊢ 𝐵 = ( Base ‘ 𝑌 )
Assertion znhash ( 𝑁 ∈ ℕ → ( ♯ ‘ 𝐵 ) = 𝑁 )

Proof

Step Hyp Ref Expression
1 zntos.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2 znhash.1 ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 nnnn0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
4 eqid ⊢ ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) = ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) )
5 eqid ⊢ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
6 1 2 4 5 znf1o ⊢ ( 𝑁 ∈ ℕ0 → ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ 𝐵 )
7 3 6 syl ⊢ ( 𝑁 ∈ ℕ → ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ 𝐵 )
8 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
9 ifnefalse ⊢ ( 𝑁 ≠ 0 → if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) )
10 f1oeq2 ⊢ ( if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) → ( ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ 𝐵 ↔ ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐵 ) )
11 8 9 10 3syl ⊢ ( 𝑁 ∈ ℕ → ( ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) –1-1-onto→ 𝐵 ↔ ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐵 ) )
12 7 11 mpbid ⊢ ( 𝑁 ∈ ℕ → ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐵 )
13 ovex ⊢ ( 0 ..^ 𝑁 ) ∈ V
14 13 f1oen ⊢ ( ( ( ℤRHom ‘ 𝑌 ) ↾ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ) : ( 0 ..^ 𝑁 ) –1-1-onto→ 𝐵 → ( 0 ..^ 𝑁 ) ≈ 𝐵 )
15 ensym ⊢ ( ( 0 ..^ 𝑁 ) ≈ 𝐵 → 𝐵 ≈ ( 0 ..^ 𝑁 ) )
16 hasheni ⊢ ( 𝐵 ≈ ( 0 ..^ 𝑁 ) → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
17 12 14 15 16 4syl ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ 𝐵 ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
18 hashfzo0 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
19 3 18 syl ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
20 17 19 eqtrd ⊢ ( 𝑁 ∈ ℕ → ( ♯ ‘ 𝐵 ) = 𝑁 )