Theorem znhash

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

	Ref	Expression
Hypotheses	zntos.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
	znhash.1	$$⊢B={\mathrm{Base}}_Y$$
Assertion	znhash	$$⊢N\in \mathbb{N}\to \left|B\right|=N$$

Proof

Step	Hyp	Ref	Expression
1		zntos.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
2		znhash.1	$$⊢B={\mathrm{Base}}_Y$$
3		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
4		eqid	$$⊢{\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}={\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}$$
5		eqid	$$⊢if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)=if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)$$
6	1 2 4 5	znf1o	$$⊢N\in {\mathbb{N}}_0\to \left({\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right):if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)\underset{1-1\; onto}{⟶}B$$
7	3 6	syl	$$⊢N\in \mathbb{N}\to \left({\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right):if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)\underset{1-1\; onto}{⟶}B$$
8		nnne0	$$⊢N\in \mathbb{N}\to N\ne 0$$
9		ifnefalse	$$⊢N\ne 0\to if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)=\left(0..^N\right)$$
10		f1oeq2	$$⊢if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)=\left(0..^N\right)\to \left(\left({\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right):if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)\underset{1-1\; onto}{⟶}B\leftrightarrow \left({\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right):\left(0..^N\right)\underset{1-1\; onto}{⟶}B\right)$$
11	8 9 10	3syl	$$⊢N\in \mathbb{N}\to \left(\left({\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right):if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)\underset{1-1\; onto}{⟶}B\leftrightarrow \left({\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right):\left(0..^N\right)\underset{1-1\; onto}{⟶}B\right)$$
12	7 11	mpbid	$$⊢N\in \mathbb{N}\to \left({\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right):\left(0..^N\right)\underset{1-1\; onto}{⟶}B$$
13		ovex	$$⊢\left(0..^N\right)\in \mathrm{V}$$
14	13	f1oen	$$⊢\left({\mathrm{\mathbb{Z}RHom}\left(Y\right)\upharpoonright }_{if\left(N=0,\mathbb{Z},\left(0..^N\right)\right)}\right):\left(0..^N\right)\underset{1-1\; onto}{⟶}B\to \left(0..^N\right)\approx B$$
15		ensym	$$⊢\left(0..^N\right)\approx B\to B\approx \left(0..^N\right)$$
16		hasheni	$$⊢B\approx \left(0..^N\right)\to \left|B\right|=\left|\left(0..^N\right)\right|$$
17	12 14 15 16	4syl	$$⊢N\in \mathbb{N}\to \left|B\right|=\left|\left(0..^N\right)\right|$$
18		hashfzo0	$$⊢N\in {\mathbb{N}}_0\to \left|\left(0..^N\right)\right|=N$$
19	3 18	syl	$$⊢N\in \mathbb{N}\to \left|\left(0..^N\right)\right|=N$$
20	17 19	eqtrd	$$⊢N\in \mathbb{N}\to \left|B\right|=N$$