# 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 $⊢ Y = ℤ/Nℤ$
znhash.1 $⊢ B = Base Y$
Assertion znhash $⊢ N ∈ ℕ → B = N$

### Proof

Step Hyp Ref Expression
1 zntos.y $⊢ Y = ℤ/Nℤ$
2 znhash.1 $⊢ B = Base Y$
3 nnnn0 $⊢ N ∈ ℕ → N ∈ ℕ 0$
4 eqid $⊢ ℤRHom ⁡ Y ↾ if N = 0 ℤ 0 ..^ N = ℤRHom ⁡ Y ↾ if N = 0 ℤ 0 ..^ N$
5 eqid $⊢ if N = 0 ℤ 0 ..^ N = if N = 0 ℤ 0 ..^ N$
6 1 2 4 5 znf1o $⊢ N ∈ ℕ 0 → ℤRHom ⁡ Y ↾ if N = 0 ℤ 0 ..^ N : if N = 0 ℤ 0 ..^ N ⟶ 1-1 onto B$
7 3 6 syl $⊢ N ∈ ℕ → ℤRHom ⁡ Y ↾ if N = 0 ℤ 0 ..^ N : if N = 0 ℤ 0 ..^ N ⟶ 1-1 onto B$
8 nnne0 $⊢ N ∈ ℕ → N ≠ 0$
9 ifnefalse $⊢ N ≠ 0 → if N = 0 ℤ 0 ..^ N = 0 ..^ N$
10 f1oeq2 $⊢ if N = 0 ℤ 0 ..^ N = 0 ..^ N → ℤRHom ⁡ Y ↾ if N = 0 ℤ 0 ..^ N : if N = 0 ℤ 0 ..^ N ⟶ 1-1 onto B ↔ ℤRHom ⁡ Y ↾ if N = 0 ℤ 0 ..^ N : 0 ..^ N ⟶ 1-1 onto B$
11 8 9 10 3syl $⊢ N ∈ ℕ → ℤRHom ⁡ Y ↾ if N = 0 ℤ 0 ..^ N : if N = 0 ℤ 0 ..^ N ⟶ 1-1 onto B ↔ ℤRHom ⁡ Y ↾ if N = 0 ℤ 0 ..^ N : 0 ..^ N ⟶ 1-1 onto B$
12 7 11 mpbid $⊢ N ∈ ℕ → ℤRHom ⁡ Y ↾ if N = 0 ℤ 0 ..^ N : 0 ..^ N ⟶ 1-1 onto B$
13 ovex $⊢ 0 ..^ N ∈ V$
14 13 f1oen $⊢ ℤRHom ⁡ Y ↾ if N = 0 ℤ 0 ..^ N : 0 ..^ N ⟶ 1-1 onto B → 0 ..^ N ≈ B$
15 ensym $⊢ 0 ..^ N ≈ B → B ≈ 0 ..^ N$
16 hasheni $⊢ B ≈ 0 ..^ N → B = 0 ..^ N$
17 12 14 15 16 4syl $⊢ N ∈ ℕ → B = 0 ..^ N$
18 hashfzo0 $⊢ N ∈ ℕ 0 → 0 ..^ N = N$
19 3 18 syl $⊢ N ∈ ℕ → 0 ..^ N = N$
20 17 19 eqtrd $⊢ N ∈ ℕ → B = N$