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	|- ( ( V e. Fin /\ N e. NN0 ) -> ( # ` { w e. Word V | ( # ` w ) = N } ) = ( ( # ` V ) ^ N ) )

Proof

Step	Hyp	Ref	Expression
1		wrdnval	|- ( ( V e. Fin /\ N e. NN0 ) -> { w e. Word V | ( # ` w ) = N } = ( V ^m ( 0 ..^ N ) ) )
2	1	fveq2d	|- ( ( V e. Fin /\ N e. NN0 ) -> ( # ` { w e. Word V | ( # ` w ) = N } ) = ( # ` ( V ^m ( 0 ..^ N ) ) ) )
3		fzofi	|- ( 0 ..^ N ) e. Fin
4		hashmap	|- ( ( V e. Fin /\ ( 0 ..^ N ) e. Fin ) -> ( # ` ( V ^m ( 0 ..^ N ) ) ) = ( ( # ` V ) ^ ( # ` ( 0 ..^ N ) ) ) )
5	3 4	mpan2	|- ( V e. Fin -> ( # ` ( V ^m ( 0 ..^ N ) ) ) = ( ( # ` V ) ^ ( # ` ( 0 ..^ N ) ) ) )
6		hashfzo0	|- ( N e. NN0 -> ( # ` ( 0 ..^ N ) ) = N )
7	6	oveq2d	|- ( N e. NN0 -> ( ( # ` V ) ^ ( # ` ( 0 ..^ N ) ) ) = ( ( # ` V ) ^ N ) )
8	5 7	sylan9eq	|- ( ( V e. Fin /\ N e. NN0 ) -> ( # ` ( V ^m ( 0 ..^ N ) ) ) = ( ( # ` V ) ^ N ) )
9	2 8	eqtrd	|- ( ( V e. Fin /\ N e. NN0 ) -> ( # ` { w e. Word V | ( # ` w ) = N } ) = ( ( # ` V ) ^ N ) )