Metamath Proof Explorer

Theorem pfxlsw2ccat

Description: Reconstruct a word from its prefix and its last two symbols. (Contributed by Thierry Arnoux, 26-Sep-2023)

Ref Expression
Hypothesis pfxlsw2ccat.n ⊢ N = W
Assertion pfxlsw2ccat ⊢ W ∈ Word V ∧ 2 ≤ N → W = W prefix N − 2 ++ ⟨“ W ⁡ N − 2 W ⁡ N − 1 ”⟩

Proof

Step Hyp Ref Expression
1 pfxlsw2ccat.n ⊢ N = W
2 simpl ⊢ W ∈ Word V ∧ 2 ≤ N → W ∈ Word V
3 simpr ⊢ W ∈ Word V ∧ 2 ≤ N → 2 ≤ N
4 3 1 breqtrdi ⊢ W ∈ Word V ∧ 2 ≤ N → 2 ≤ W
5 wrdlenge2n0 ⊢ W ∈ Word V ∧ 2 ≤ W → W ≠ ∅
6 2 4 5 syl2anc ⊢ W ∈ Word V ∧ 2 ≤ N → W ≠ ∅
7 pfxlswccat ⊢ W ∈ Word V ∧ W ≠ ∅ → W prefix W − 1 ++ ⟨“ lastS ⁡ W ”⟩ = W
8 2 6 7 syl2anc ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 ++ ⟨“ lastS ⁡ W ”⟩ = W
9 lsw ⊢ W ∈ Word V → lastS ⁡ W = W ⁡ W − 1
10 1 oveq1i ⊢ N − 1 = W − 1
11 10 fveq2i ⊢ W ⁡ N − 1 = W ⁡ W − 1
12 9 11 eqtr4di ⊢ W ∈ Word V → lastS ⁡ W = W ⁡ N − 1
13 2 12 syl ⊢ W ∈ Word V ∧ 2 ≤ N → lastS ⁡ W = W ⁡ N − 1
14 13 s1eqd ⊢ W ∈ Word V ∧ 2 ≤ N → ⟨“ lastS ⁡ W ”⟩ = ⟨“ W ⁡ N − 1 ”⟩
15 14 oveq2d ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 ++ ⟨“ lastS ⁡ W ”⟩ = W prefix W − 1 ++ ⟨“ W ⁡ N − 1 ”⟩
16 8 15 eqtr3d ⊢ W ∈ Word V ∧ 2 ≤ N → W = W prefix W − 1 ++ ⟨“ W ⁡ N − 1 ”⟩
17 pfxcl ⊢ W ∈ Word V → W prefix W − 1 ∈ Word V
18 2 17 syl ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 ∈ Word V
19 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
20 2 19 syl ⊢ W ∈ Word V ∧ 2 ≤ N → W ∈ ℕ 0
21 1 20 eqeltrid ⊢ W ∈ Word V ∧ 2 ≤ N → N ∈ ℕ 0
22 nn0ge2m1nn ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → N − 1 ∈ ℕ
23 21 3 22 syl2anc ⊢ W ∈ Word V ∧ 2 ≤ N → N − 1 ∈ ℕ
24 10 23 eqeltrrid ⊢ W ∈ Word V ∧ 2 ≤ N → W − 1 ∈ ℕ
25 20 nn0red ⊢ W ∈ Word V ∧ 2 ≤ N → W ∈ ℝ
26 25 lem1d ⊢ W ∈ Word V ∧ 2 ≤ N → W − 1 ≤ W
27 pfxn0 ⊢ W ∈ Word V ∧ W − 1 ∈ ℕ ∧ W − 1 ≤ W → W prefix W − 1 ≠ ∅
28 2 24 26 27 syl3anc ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 ≠ ∅
29 pfxlswccat ⊢ W prefix W − 1 ∈ Word V ∧ W prefix W − 1 ≠ ∅ → W prefix W − 1 prefix W prefix W − 1 − 1 ++ ⟨“ lastS ⁡ W prefix W − 1 ”⟩ = W prefix W − 1
30 18 28 29 syl2anc ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 prefix W prefix W − 1 − 1 ++ ⟨“ lastS ⁡ W prefix W − 1 ”⟩ = W prefix W − 1
31 ige2m1fz ⊢ W ∈ ℕ 0 ∧ 2 ≤ W → W − 1 ∈ 0 … W
32 20 4 31 syl2anc ⊢ W ∈ Word V ∧ 2 ≤ N → W − 1 ∈ 0 … W
33 pfxlen ⊢ W ∈ Word V ∧ W − 1 ∈ 0 … W → W prefix W − 1 = W − 1
34 2 32 33 syl2anc ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 = W − 1
35 34 oveq1d ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 − 1 = W - 1 - 1
36 0zd ⊢ W ∈ Word V ∧ 2 ≤ N → 0 ∈ ℤ
37 nn0ge2m1nn0 ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → N − 1 ∈ ℕ 0
38 21 3 37 syl2anc ⊢ W ∈ Word V ∧ 2 ≤ N → N − 1 ∈ ℕ 0
39 10 38 eqeltrrid ⊢ W ∈ Word V ∧ 2 ≤ N → W − 1 ∈ ℕ 0
40 39 nn0zd ⊢ W ∈ Word V ∧ 2 ≤ N → W − 1 ∈ ℤ
41 1zzd ⊢ W ∈ Word V ∧ 2 ≤ N → 1 ∈ ℤ
42 40 41 zsubcld ⊢ W ∈ Word V ∧ 2 ≤ N → W - 1 - 1 ∈ ℤ
43 2nn0 ⊢ 2 ∈ ℕ 0
44 43 a1i ⊢ W ∈ Word V ∧ 2 ≤ N → 2 ∈ ℕ 0
45 nn0sub ⊢ 2 ∈ ℕ 0 ∧ N ∈ ℕ 0 → 2 ≤ N ↔ N − 2 ∈ ℕ 0
46 45 biimpa ⊢ 2 ∈ ℕ 0 ∧ N ∈ ℕ 0 ∧ 2 ≤ N → N − 2 ∈ ℕ 0
47 44 21 3 46 syl21anc ⊢ W ∈ Word V ∧ 2 ≤ N → N − 2 ∈ ℕ 0
48 47 nn0ge0d ⊢ W ∈ Word V ∧ 2 ≤ N → 0 ≤ N − 2
49 21 nn0cnd ⊢ W ∈ Word V ∧ 2 ≤ N → N ∈ ℂ
50 sub1m1 ⊢ N ∈ ℂ → N - 1 - 1 = N − 2
51 49 50 syl ⊢ W ∈ Word V ∧ 2 ≤ N → N - 1 - 1 = N − 2
52 48 51 breqtrrd ⊢ W ∈ Word V ∧ 2 ≤ N → 0 ≤ N - 1 - 1
53 10 oveq1i ⊢ N - 1 - 1 = W - 1 - 1
54 52 53 breqtrdi ⊢ W ∈ Word V ∧ 2 ≤ N → 0 ≤ W - 1 - 1
55 24 nnred ⊢ W ∈ Word V ∧ 2 ≤ N → W − 1 ∈ ℝ
56 55 lem1d ⊢ W ∈ Word V ∧ 2 ≤ N → W - 1 - 1 ≤ W − 1
57 36 40 42 54 56 elfzd ⊢ W ∈ Word V ∧ 2 ≤ N → W - 1 - 1 ∈ 0 … W − 1
58 35 57 eqeltrd ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 − 1 ∈ 0 … W − 1
59 pfxpfx ⊢ W ∈ Word V ∧ W − 1 ∈ 0 … W ∧ W prefix W − 1 − 1 ∈ 0 … W − 1 → W prefix W − 1 prefix W prefix W − 1 − 1 = W prefix W prefix W − 1 − 1
60 2 32 58 59 syl3anc ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 prefix W prefix W − 1 − 1 = W prefix W prefix W − 1 − 1
61 34 10 eqtr4di ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 = N − 1
62 61 oveq1d ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 − 1 = N - 1 - 1
63 62 51 eqtrd ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 − 1 = N − 2
64 63 oveq2d ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W prefix W − 1 − 1 = W prefix N − 2
65 60 64 eqtrd ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 prefix W prefix W − 1 − 1 = W prefix N − 2
66 pfxtrcfvl ⊢ W ∈ Word V ∧ 2 ≤ W → lastS ⁡ W prefix W − 1 = W ⁡ W − 2
67 2 4 66 syl2anc ⊢ W ∈ Word V ∧ 2 ≤ N → lastS ⁡ W prefix W − 1 = W ⁡ W − 2
68 1 a1i ⊢ W ∈ Word V ∧ 2 ≤ N → N = W
69 68 fvoveq1d ⊢ W ∈ Word V ∧ 2 ≤ N → W ⁡ N − 2 = W ⁡ W − 2
70 67 69 eqtr4d ⊢ W ∈ Word V ∧ 2 ≤ N → lastS ⁡ W prefix W − 1 = W ⁡ N − 2
71 70 s1eqd ⊢ W ∈ Word V ∧ 2 ≤ N → ⟨“ lastS ⁡ W prefix W − 1 ”⟩ = ⟨“ W ⁡ N − 2 ”⟩
72 65 71 oveq12d ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 prefix W prefix W − 1 − 1 ++ ⟨“ lastS ⁡ W prefix W − 1 ”⟩ = W prefix N − 2 ++ ⟨“ W ⁡ N − 2 ”⟩
73 30 72 eqtr3d ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 = W prefix N − 2 ++ ⟨“ W ⁡ N − 2 ”⟩
74 73 oveq1d ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 ++ ⟨“ W ⁡ N − 1 ”⟩ = W prefix N − 2 ++ ⟨“ W ⁡ N − 2 ”⟩ ++ ⟨“ W ⁡ N − 1 ”⟩
75 pfxcl ⊢ W ∈ Word V → W prefix N − 2 ∈ Word V
76 2 75 syl ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix N − 2 ∈ Word V
77 ccatw2s1ccatws2 ⊢ W prefix N − 2 ∈ Word V → W prefix N − 2 ++ ⟨“ W ⁡ N − 2 ”⟩ ++ ⟨“ W ⁡ N − 1 ”⟩ = W prefix N − 2 ++ ⟨“ W ⁡ N − 2 W ⁡ N − 1 ”⟩
78 76 77 syl ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix N − 2 ++ ⟨“ W ⁡ N − 2 ”⟩ ++ ⟨“ W ⁡ N − 1 ”⟩ = W prefix N − 2 ++ ⟨“ W ⁡ N − 2 W ⁡ N − 1 ”⟩
79 16 74 78 3eqtrd ⊢ W ∈ Word V ∧ 2 ≤ N → W = W prefix N − 2 ++ ⟨“ W ⁡ N − 2 W ⁡ N − 1 ”⟩