Theorem lswccats1fst

Description: The last symbol of a nonempty word concatenated with its first symbol is the first symbol. (Contributed by AV, 28-Jun-2018) (Proof shortened by AV, 1-May-2020)

	Ref	Expression
Assertion	lswccats1fst	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( lastS ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		wrdsymb1	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
2		lswccats1	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ ( 𝑃 ‘ 0 ) ∈ 𝑉 ) → ( lastS ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( 𝑃 ‘ 0 ) )
3	1 2	syldan	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( lastS ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( 𝑃 ‘ 0 ) )
4		simpl	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → 𝑃 ∈ Word 𝑉 )
5	1	s1cld	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ∈ Word 𝑉 )
6		lencl	⊢ ( 𝑃 ∈ Word 𝑉 → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
7		elnnnn0c	⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) )
8	7	biimpri	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℕ )
9	6 8	sylan	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℕ )
10		lbfzo0	⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ↔ ( ♯ ‘ 𝑃 ) ∈ ℕ )
11	9 10	sylibr	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) )
12		ccatval1	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ∈ Word 𝑉 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( 𝑃 ‘ 0 ) )
13	4 5 11 12	syl3anc	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 0 ) = ( 𝑃 ‘ 0 ) )
14	3 13	eqtr4d	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( lastS ‘ ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ) = ( ( 𝑃 ++ ⟨“ ( 𝑃 ‘ 0 ) ”⟩ ) ‘ 0 ) )