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

Metamath Proof Explorer

Theorem pfxlen

Description: Length of a prefix. (Contributed by Stefan O'Rear, 24-Aug-2015) (Revised by AV, 2-May-2020)

Ref Expression
Assertion pfxlen ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 prefix 𝐿 ) ) = 𝐿 )

Proof

Step Hyp Ref Expression
1 pfxfn ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( 𝑆 prefix 𝐿 ) Fn ( 0 ..^ 𝐿 ) )
2 hashfn ⊢ ( ( 𝑆 prefix 𝐿 ) Fn ( 0 ..^ 𝐿 ) → ( ♯ ‘ ( 𝑆 prefix 𝐿 ) ) = ( ♯ ‘ ( 0 ..^ 𝐿 ) ) )
3 1 2 syl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 prefix 𝐿 ) ) = ( ♯ ‘ ( 0 ..^ 𝐿 ) ) )
4 elfznn0 ⊢ ( 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → 𝐿 ∈ ℕ0 )
5 4 adantl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → 𝐿 ∈ ℕ0 )
6 hashfzo0 ⊢ ( 𝐿 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝐿 ) ) = 𝐿 )
7 5 6 syl ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 0 ..^ 𝐿 ) ) = 𝐿 )
8 3 7 eqtrd ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 prefix 𝐿 ) ) = 𝐿 )