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 ∈ Word V ∧ W ≠ ∅ ∧ I ∈ 0 ..^ W − 1 → W prefix W − 1 ⁡ I = W ⁡ I

Proof

Step Hyp Ref Expression
1 wrdfin ⊢ W ∈ Word V → W ∈ Fin
2 1elfz0hash ⊢ W ∈ Fin ∧ W ≠ ∅ → 1 ∈ 0 … W
3 1 2 sylan ⊢ W ∈ Word V ∧ W ≠ ∅ → 1 ∈ 0 … W
4 lennncl ⊢ W ∈ Word V ∧ W ≠ ∅ → W ∈ ℕ
5 elfz1end ⊢ W ∈ ℕ ↔ W ∈ 1 … W
6 4 5 sylib ⊢ W ∈ Word V ∧ W ≠ ∅ → W ∈ 1 … W
7 3 6 jca ⊢ W ∈ Word V ∧ W ≠ ∅ → 1 ∈ 0 … W ∧ W ∈ 1 … W
8 7 3adant3 ⊢ W ∈ Word V ∧ 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 ∈ Word V ∧ W ≠ ∅ ∧ I ∈ 0 ..^ W − 1 → W − 1 ∈ 0 … W
11 pfxfv ⊢ W ∈ Word V ∧ W − 1 ∈ 0 … W ∧ I ∈ 0 ..^ W − 1 → W prefix W − 1 ⁡ I = W ⁡ I
12 10 11 syld3an2 ⊢ W ∈ Word V ∧ W ≠ ∅ ∧ I ∈ 0 ..^ W − 1 → W prefix W − 1 ⁡ I = W ⁡ I