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∈WordV∧W≠∅→WprefixW−1++⟨“lastS⁡W”⟩=W

Proof

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