Metamath Proof Explorer


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 ) )