This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )