Metamath Proof Explorer

Theorem swrdlsw

Description: Extract the last single symbol from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018)

Ref Expression
Assertion swrdlsw ⊢ W ∈ Word V ∧ W ≠ ∅ → W substr W − 1 W = ⟨“ lastS ⁡ W ”⟩

Proof

Step Hyp Ref Expression
1 hashneq0 ⊢ W ∈ Word V → 0 < W ↔ W ≠ ∅
2 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
3 nn0z ⊢ W ∈ ℕ 0 → W ∈ ℤ
4 elnnz ⊢ W ∈ ℕ ↔ W ∈ ℤ ∧ 0 < W
5 fzo0end ⊢ W ∈ ℕ → W − 1 ∈ 0 ..^ W
6 4 5 sylbir ⊢ W ∈ ℤ ∧ 0 < W → W − 1 ∈ 0 ..^ W
7 6 ex ⊢ W ∈ ℤ → 0 < W → W − 1 ∈ 0 ..^ W
8 2 3 7 3syl ⊢ W ∈ Word V → 0 < W → W − 1 ∈ 0 ..^ W
9 1 8 sylbird ⊢ W ∈ Word V → W ≠ ∅ → W − 1 ∈ 0 ..^ W
10 9 imp ⊢ W ∈ Word V ∧ W ≠ ∅ → W − 1 ∈ 0 ..^ W
11 swrds1 ⊢ W ∈ Word V ∧ W − 1 ∈ 0 ..^ W → W substr W − 1 W - 1 + 1 = ⟨“ W ⁡ W − 1 ”⟩
12 10 11 syldan ⊢ W ∈ Word V ∧ W ≠ ∅ → W substr W − 1 W - 1 + 1 = ⟨“ W ⁡ W − 1 ”⟩
13 nn0cn ⊢ W ∈ ℕ 0 → W ∈ ℂ
14 ax-1cn ⊢ 1 ∈ ℂ
15 13 14 jctir ⊢ W ∈ ℕ 0 → W ∈ ℂ ∧ 1 ∈ ℂ
16 npcan ⊢ W ∈ ℂ ∧ 1 ∈ ℂ → W - 1 + 1 = W
17 16 eqcomd ⊢ W ∈ ℂ ∧ 1 ∈ ℂ → W = W - 1 + 1
18 2 15 17 3syl ⊢ W ∈ Word V → W = W - 1 + 1
19 18 adantr ⊢ W ∈ Word V ∧ W ≠ ∅ → W = W - 1 + 1
20 19 opeq2d ⊢ W ∈ Word V ∧ W ≠ ∅ → W − 1 W = W − 1 W - 1 + 1
21 20 oveq2d ⊢ W ∈ Word V ∧ W ≠ ∅ → W substr W − 1 W = W substr W − 1 W - 1 + 1
22 lsw ⊢ W ∈ Word V → lastS ⁡ W = W ⁡ W − 1
23 22 adantr ⊢ W ∈ Word V ∧ W ≠ ∅ → lastS ⁡ W = W ⁡ W − 1
24 23 s1eqd ⊢ W ∈ Word V ∧ W ≠ ∅ → ⟨“ lastS ⁡ W ”⟩ = ⟨“ W ⁡ W − 1 ”⟩
25 12 21 24 3eqtr4d ⊢ W ∈ Word V ∧ W ≠ ∅ → W substr W − 1 W = ⟨“ lastS ⁡ W ”⟩