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	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑊 ) ”⟩ ) = 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		swrdlsw	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ⟨“ ( lastS ‘ 𝑊 ) ”⟩ )
2	1	eqcomd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ⟨“ ( lastS ‘ 𝑊 ) ”⟩ = ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) )
3	2	oveq2d	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑊 ) ”⟩ ) = ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ++ ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) )
4		wrdfin	⊢ ( 𝑊 ∈ Word 𝑉 → 𝑊 ∈ Fin )
5		1elfz0hash	⊢ ( ( 𝑊 ∈ Fin ∧ 𝑊 ≠ ∅ ) → 1 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
6	4 5	sylan	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → 1 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
7		fznn0sub2	⊢ ( 1 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
8	6 7	syl	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
9		pfxcctswrd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ++ ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) = 𝑊 )
10	8 9	syldan	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ++ ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) ) = 𝑊 )
11	3 10	eqtrd	⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( ( 𝑊 prefix ( ( ♯ ‘ 𝑊 ) − 1 ) ) ++ ⟨“ ( lastS ‘ 𝑊 ) ”⟩ ) = 𝑊 )