This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑊 ∈ 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 ‘ 𝑊 ) ”⟩ ) = 𝑊 )