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 ⊢ P ∈ Word V ∧ 1 ≤ P → lastS ⁡ P ++ ⟨“ P ⁡ 0 ”⟩ = P ++ ⟨“ P ⁡ 0 ”⟩ ⁡ 0

Proof

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