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

Metamath Proof Explorer

Theorem repswlen

Description: The length of a "repeated symbol word". (Contributed by AV, 4-Nov-2018)

Ref Expression
Assertion repswlen ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) = 𝑁 )

Proof

Step Hyp Ref Expression
1 repsf ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑆 repeatS 𝑁 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑉 )
2 ffn ⊢ ( ( 𝑆 repeatS 𝑁 ) : ( 0 ..^ 𝑁 ) ⟶ 𝑉 → ( 𝑆 repeatS 𝑁 ) Fn ( 0 ..^ 𝑁 ) )
3 hashfn ⊢ ( ( 𝑆 repeatS 𝑁 ) Fn ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
4 1 2 3 3syl ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
5 hashfzo0 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
6 5 adantl ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
7 4 6 eqtrd ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 𝑆 repeatS 𝑁 ) ) = 𝑁 )