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 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ A ≠ ∅ → A ++ B ⁡ A − 1 = lastS ⁡ A

Proof

Step Hyp Ref Expression
1 lennncl ⊢ A ∈ Word V ∧ A ≠ ∅ → A ∈ ℕ
2 1 3adant2 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ A ≠ ∅ → A ∈ ℕ
3 fzo0end ⊢ A ∈ ℕ → A − 1 ∈ 0 ..^ A
4 2 3 syl ⊢ A ∈ Word V ∧ B ∈ Word V ∧ A ≠ ∅ → A − 1 ∈ 0 ..^ A
5 ccatval1 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ A − 1 ∈ 0 ..^ A → A ++ B ⁡ A − 1 = A ⁡ A − 1
6 4 5 syld3an3 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ A ≠ ∅ → A ++ B ⁡ A − 1 = A ⁡ A − 1
7 lsw ⊢ A ∈ Word V → lastS ⁡ A = A ⁡ A − 1
8 7 3ad2ant1 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ A ≠ ∅ → lastS ⁡ A = A ⁡ A − 1
9 6 8 eqtr4d ⊢ A ∈ Word V ∧ B ∈ Word V ∧ A ≠ ∅ → A ++ B ⁡ A − 1 = lastS ⁡ A