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∈WordV∧W≠∅→WsubstrW−1W=⟨“lastS⁡W”⟩

Proof

Step Hyp Ref Expression
1 hashneq0 ⊢W∈WordV→0<W↔W≠∅
2 lencl ⊢W∈WordV→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∈WordV→0<W→W−1∈0..^W
9 1 8 sylbird ⊢W∈WordV→W≠∅→W−1∈0..^W
10 9 imp ⊢W∈WordV∧W≠∅→W−1∈0..^W
11 swrds1 ⊢W∈WordV∧W−1∈0..^W→WsubstrW−1W-1+1=⟨“W⁡W−1”⟩
12 10 11 syldan ⊢W∈WordV∧W≠∅→WsubstrW−1W-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∈WordV→W=W-1+1
19 18 adantr ⊢W∈WordV∧W≠∅→W=W-1+1
20 19 opeq2d ⊢W∈WordV∧W≠∅→W−1W=W−1W-1+1
21 20 oveq2d ⊢W∈WordV∧W≠∅→WsubstrW−1W=WsubstrW−1W-1+1
22 lsw ⊢W∈WordV→lastS⁡W=W⁡W−1
23 22 adantr ⊢W∈WordV∧W≠∅→lastS⁡W=W⁡W−1
24 23 s1eqd ⊢W∈WordV∧W≠∅→⟨“lastS⁡W”⟩=⟨“W⁡W−1”⟩
25 12 21 24 3eqtr4d ⊢W∈WordV∧W≠∅→WsubstrW−1W=⟨“lastS⁡W”⟩