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

Metamath Proof Explorer

Theorem pfxtrcfv

Description: A symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018) (Revised by AV, 3-May-2020)

Ref Expression
Assertion pfxtrcfv ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 wrdfin ⊢ ( 𝑊 ∈ Word 𝑉 → 𝑊 ∈ Fin )
2 1elfz0hash ⊢ ( ( 𝑊 ∈ Fin ∧ 𝑊 ≠ ∅ ) → 1 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
3 1 2 sylan ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → 1 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
4 lennncl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ )
5 elfz1end ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ ( ♯ ‘ 𝑊 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
6 4 5 sylib ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ♯ ‘ 𝑊 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) )
7 3 6 jca ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 1 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) )
8 7 3adant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( 1 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) )
9 fz0fzdiffz0 ⊢ ( ( 1 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ ( ♯ ‘ 𝑊 ) ∈ ( 1 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
10 8 9 syl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
11 pfxfv ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )
12 10 11 syld3an2 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝐼 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )