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 ( ( 𝑉 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) = ( ( ♯ ‘ 𝑉 ) ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 wrdnval ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } = ( 𝑉 ↑m ( 0 ..^ 𝑁 ) ) )
2 1 fveq2d ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) = ( ♯ ‘ ( 𝑉 ↑m ( 0 ..^ 𝑁 ) ) ) )
3 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
4 hashmap ⊢ ( ( 𝑉 ∈ Fin ∧ ( 0 ..^ 𝑁 ) ∈ Fin ) → ( ♯ ‘ ( 𝑉 ↑m ( 0 ..^ 𝑁 ) ) ) = ( ( ♯ ‘ 𝑉 ) ↑ ( ♯ ‘ ( 0 ..^ 𝑁 ) ) ) )
5 3 4 mpan2 ⊢ ( 𝑉 ∈ Fin → ( ♯ ‘ ( 𝑉 ↑m ( 0 ..^ 𝑁 ) ) ) = ( ( ♯ ‘ 𝑉 ) ↑ ( ♯ ‘ ( 0 ..^ 𝑁 ) ) ) )
6 hashfzo0 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
7 6 oveq2d ⊢ ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ 𝑉 ) ↑ ( ♯ ‘ ( 0 ..^ 𝑁 ) ) ) = ( ( ♯ ‘ 𝑉 ) ↑ 𝑁 ) )
8 5 7 sylan9eq ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 𝑉 ↑m ( 0 ..^ 𝑁 ) ) ) = ( ( ♯ ‘ 𝑉 ) ↑ 𝑁 ) )
9 2 8 eqtrd ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ { 𝑤 ∈ Word 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) = ( ( ♯ ‘ 𝑉 ) ↑ 𝑁 ) )