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 ∈ Fin ∧ N ∈ ℕ 0 → w ∈ Word V | w = N = V N

Proof

Step Hyp Ref Expression
1 wrdnval ⊢ V ∈ Fin ∧ N ∈ ℕ 0 → w ∈ Word V | w = N = V 0 ..^ N
2 1 fveq2d ⊢ V ∈ Fin ∧ N ∈ ℕ 0 → w ∈ Word V | w = N = V 0 ..^ N
3 fzofi ⊢ 0 ..^ N ∈ Fin
4 hashmap ⊢ V ∈ Fin ∧ 0 ..^ N ∈ Fin → V 0 ..^ N = V 0 ..^ N
5 3 4 mpan2 ⊢ V ∈ Fin → V 0 ..^ N = V 0 ..^ N
6 hashfzo0 ⊢ N ∈ ℕ 0 → 0 ..^ N = N
7 6 oveq2d ⊢ N ∈ ℕ 0 → V 0 ..^ N = V N
8 5 7 sylan9eq ⊢ V ∈ Fin ∧ N ∈ ℕ 0 → V 0 ..^ N = V N
9 2 8 eqtrd ⊢ V ∈ Fin ∧ N ∈ ℕ 0 → w ∈ Word V | w = N = V N