Theorem hashwrdn

Description: If there is only a finite number of symbols, the number of words of a fixed length over these sysmbols is the number of these symbols raised to the power of the length. (Contributed by Alexander van der Vekens, 25-Mar-2018)

	Ref	Expression
Assertion	hashwrdn	$$⊢\left(V\in \mathrm{Fin}\wedge N\in {\mathbb{N}}_0\right)\to \left|\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\right|={\left|V\right|}^N$$

Proof

Step	Hyp	Ref	Expression
1		wrdnval	$$⊢\left(V\in \mathrm{Fin}\wedge N\in {\mathbb{N}}_0\right)\to \left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}=V^{\left(0..^N\right)}$$
2	1	fveq2d	$$⊢\left(V\in \mathrm{Fin}\wedge N\in {\mathbb{N}}_0\right)\to \left|\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\right|=\left|V^{\left(0..^N\right)}\right|$$
3		fzofi	$$⊢\left(0..^N\right)\in \mathrm{Fin}$$
4		hashmap	$$⊢\left(V\in \mathrm{Fin}\wedge \left(0..^N\right)\in \mathrm{Fin}\right)\to \left|V^{\left(0..^N\right)}\right|={\left|V\right|}^{\left|\left(0..^N\right)\right|}$$
5	3 4	mpan2	$$⊢V\in \mathrm{Fin}\to \left|V^{\left(0..^N\right)}\right|={\left|V\right|}^{\left|\left(0..^N\right)\right|}$$
6		hashfzo0	$$⊢N\in {\mathbb{N}}_0\to \left|\left(0..^N\right)\right|=N$$
7	6	oveq2d	$$⊢N\in {\mathbb{N}}_0\to {\left|V\right|}^{\left|\left(0..^N\right)\right|}={\left|V\right|}^N$$
8	5 7	sylan9eq	$$⊢\left(V\in \mathrm{Fin}\wedge N\in {\mathbb{N}}_0\right)\to \left|V^{\left(0..^N\right)}\right|={\left|V\right|}^N$$
9	2 8	eqtrd	$$⊢\left(V\in \mathrm{Fin}\wedge N\in {\mathbb{N}}_0\right)\to \left|\left\{w\in \mathrm{Word}V|\left|w\right|=N\right\}\right|={\left|V\right|}^N$$