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

Metamath Proof Explorer

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