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 𝑉 ∣ ( ♯ ‘ 𝑤 ) = 𝑁 } ) = ( ( ♯ ‘ 𝑉 ) ↑ 𝑁 ) )