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 )