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 ⊢W∈WordV∧W≠∅∧I∈0..^W−1→WprefixW−1⁡I=W⁡I

Proof

Step Hyp Ref Expression
1 wrdfin ⊢W∈WordV→W∈Fin
2 1elfz0hash ⊢W∈Fin∧W≠∅→1∈0…W
3 1 2 sylan ⊢W∈WordV∧W≠∅→1∈0…W
4 lennncl ⊢W∈WordV∧W≠∅→W∈ℕ
5 elfz1end ⊢W∈ℕ↔W∈1…W
6 4 5 sylib ⊢W∈WordV∧W≠∅→W∈1…W
7 3 6 jca ⊢W∈WordV∧W≠∅→1∈0…W∧W∈1…W
8 7 3adant3 ⊢W∈WordV∧W≠∅∧I∈0..^W−1→1∈0…W∧W∈1…W
9 fz0fzdiffz0 ⊢1∈0…W∧W∈1…W→W−1∈0…W
10 8 9 syl ⊢W∈WordV∧W≠∅∧I∈0..^W−1→W−1∈0…W
11 pfxfv ⊢W∈WordV∧W−1∈0…W∧I∈0..^W−1→WprefixW−1⁡I=W⁡I
12 10 11 syld3an2 ⊢W∈WordV∧W≠∅∧I∈0..^W−1→WprefixW−1⁡I=W⁡I