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

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 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) → ( 𝑊 substr ⟨ ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) ⟩ ) = ⟨“ ( lastS ‘ 𝑊 ) ”⟩ )

Proof

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