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

Proof

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