This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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