# 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 = ( Z/nZ ` N )`
znhash.1
`|- B = ( Base ` Y )`
Assertion znhash
`|- ( N e. NN -> ( # ` B ) = N )`

### Proof

Step Hyp Ref Expression
1 zntos.y
` |-  Y = ( Z/nZ ` N )`
2 znhash.1
` |-  B = ( Base ` Y )`
3 nnnn0
` |-  ( N e. NN -> N e. NN0 )`
4 eqid
` |-  ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) = ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) )`
5 eqid
` |-  if ( N = 0 , ZZ , ( 0 ..^ N ) ) = if ( N = 0 , ZZ , ( 0 ..^ N ) )`
6 1 2 4 5 znf1o
` |-  ( N e. NN0 -> ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) : if ( N = 0 , ZZ , ( 0 ..^ N ) ) -1-1-onto-> B )`
7 3 6 syl
` |-  ( N e. NN -> ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) : if ( N = 0 , ZZ , ( 0 ..^ N ) ) -1-1-onto-> B )`
8 nnne0
` |-  ( N e. NN -> N =/= 0 )`
9 ifnefalse
` |-  ( N =/= 0 -> if ( N = 0 , ZZ , ( 0 ..^ N ) ) = ( 0 ..^ N ) )`
10 f1oeq2
` |-  ( if ( N = 0 , ZZ , ( 0 ..^ N ) ) = ( 0 ..^ N ) -> ( ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) : if ( N = 0 , ZZ , ( 0 ..^ N ) ) -1-1-onto-> B <-> ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) : ( 0 ..^ N ) -1-1-onto-> B ) )`
11 8 9 10 3syl
` |-  ( N e. NN -> ( ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) : if ( N = 0 , ZZ , ( 0 ..^ N ) ) -1-1-onto-> B <-> ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) : ( 0 ..^ N ) -1-1-onto-> B ) )`
12 7 11 mpbid
` |-  ( N e. NN -> ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 0 ..^ N ) ) ) : ( 0 ..^ N ) -1-1-onto-> B )`
13 ovex
` |-  ( 0 ..^ N ) e. _V`
14 13 f1oen
` |-  ( ( ( ZRHom ` Y ) |` if ( N = 0 , ZZ , ( 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 e. NN -> ( # ` B ) = ( # ` ( 0 ..^ N ) ) )`
18 hashfzo0
` |-  ( N e. NN0 -> ( # ` ( 0 ..^ N ) ) = N )`
19 3 18 syl
` |-  ( N e. NN -> ( # ` ( 0 ..^ N ) ) = N )`
20 17 19 eqtrd
` |-  ( N e. NN -> ( # ` B ) = N )`