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 ) ) ‘ 𝐼 ) = ( 𝑊 ‘ 𝐼 ) )