Metamath Proof Explorer

Theorem pfxlswccat

Description: Reconstruct a nonempty word from its prefix and last symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018) (Revised by AV, 9-May-2020)

Ref Expression
Assertion pfxlswccat ⊢ W ∈ Word V ∧ W ≠ ∅ → W prefix W − 1 ++ ⟨“ lastS ⁡ W ”⟩ = W

Proof

Step Hyp Ref Expression
1 swrdlsw ⊢ W ∈ Word V ∧ W ≠ ∅ → W substr W − 1 W = ⟨“ lastS ⁡ W ”⟩
2 1 eqcomd ⊢ W ∈ Word V ∧ W ≠ ∅ → ⟨“ lastS ⁡ W ”⟩ = W substr W − 1 W
3 2 oveq2d ⊢ W ∈ Word V ∧ W ≠ ∅ → W prefix W − 1 ++ ⟨“ lastS ⁡ W ”⟩ = W prefix W − 1 ++ W substr W − 1 W
4 wrdfin ⊢ W ∈ Word V → W ∈ Fin
5 1elfz0hash ⊢ W ∈ Fin ∧ W ≠ ∅ → 1 ∈ 0 … W
6 4 5 sylan ⊢ W ∈ Word V ∧ W ≠ ∅ → 1 ∈ 0 … W
7 fznn0sub2 ⊢ 1 ∈ 0 … W → W − 1 ∈ 0 … W
8 6 7 syl ⊢ W ∈ Word V ∧ W ≠ ∅ → W − 1 ∈ 0 … W
9 pfxcctswrd ⊢ W ∈ Word V ∧ W − 1 ∈ 0 … W → W prefix W − 1 ++ W substr W − 1 W = W
10 8 9 syldan ⊢ W ∈ Word V ∧ W ≠ ∅ → W prefix W − 1 ++ W substr W − 1 W = W
11 3 10 eqtrd ⊢ W ∈ Word V ∧ W ≠ ∅ → W prefix W − 1 ++ ⟨“ lastS ⁡ W ”⟩ = W