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

Metamath Proof Explorer

Theorem ccatval1lsw

Description: The last symbol of the left (nonempty) half of a concatenated word. (Contributed by Alexander van der Vekens, 3-Oct-2018) (Proof shortened by AV, 1-May-2020)

Ref Expression
Assertion ccatval1lsw ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐴 ≠ ∅ ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) = ( lastS ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 lennncl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
2 1 3adant2 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐴 ≠ ∅ ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
3 fzo0end ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
4 2 3 syl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐴 ≠ ∅ ) → ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
5 ccatval1 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝐴 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) = ( 𝐴 ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
6 4 5 syld3an3 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐴 ≠ ∅ ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) = ( 𝐴 ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
7 lsw ⊢ ( 𝐴 ∈ Word 𝑉 → ( lastS ‘ 𝐴 ) = ( 𝐴 ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
8 7 3ad2ant1 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐴 ≠ ∅ ) → ( lastS ‘ 𝐴 ) = ( 𝐴 ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) )
9 6 8 eqtr4d ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐴 ≠ ∅ ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( ( ♯ ‘ 𝐴 ) − 1 ) ) = ( lastS ‘ 𝐴 ) )