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 ‘ 𝐴 ) )