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 syl6eqr ⊢ 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 elfz4 ⊢ 0 ∈ ℤ ∧ W − 1 ∈ ℤ ∧ W - 1 - 1 ∈ ℤ ∧ 0 ≤ W - 1 - 1 ∧ W - 1 - 1 ≤ W − 1 → W - 1 - 1 ∈ 0 … W − 1
58 36 40 42 54 56 57 syl32anc ⊢ W ∈ Word V ∧ 2 ≤ N → W - 1 - 1 ∈ 0 … W − 1
59 35 58 eqeltrd ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 − 1 ∈ 0 … W − 1
60 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
61 2 32 59 60 syl3anc ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 prefix W prefix W − 1 − 1 = W prefix W prefix W − 1 − 1
62 34 10 syl6eqr ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 = N − 1
63 62 oveq1d ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 − 1 = N - 1 - 1
64 63 51 eqtrd ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 − 1 = N − 2
65 64 oveq2d ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W prefix W − 1 − 1 = W prefix N − 2
66 61 65 eqtrd ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 prefix W prefix W − 1 − 1 = W prefix N − 2
67 pfxtrcfvl ⊢ W ∈ Word V ∧ 2 ≤ W → lastS ⁡ W prefix W − 1 = W ⁡ W − 2
68 2 4 67 syl2anc ⊢ W ∈ Word V ∧ 2 ≤ N → lastS ⁡ W prefix W − 1 = W ⁡ W − 2
69 1 a1i ⊢ W ∈ Word V ∧ 2 ≤ N → N = W
70 69 fvoveq1d ⊢ W ∈ Word V ∧ 2 ≤ N → W ⁡ N − 2 = W ⁡ W − 2
71 68 70 eqtr4d ⊢ W ∈ Word V ∧ 2 ≤ N → lastS ⁡ W prefix W − 1 = W ⁡ N − 2
72 71 s1eqd ⊢ W ∈ Word V ∧ 2 ≤ N → ⟨“ lastS ⁡ W prefix W − 1 ”⟩ = ⟨“ W ⁡ N − 2 ”⟩
73 66 72 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 ”⟩
74 30 73 eqtr3d ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 = W prefix N − 2 ++ ⟨“ W ⁡ N − 2 ”⟩
75 74 oveq1d ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix W − 1 ++ ⟨“ W ⁡ N − 1 ”⟩ = W prefix N − 2 ++ ⟨“ W ⁡ N − 2 ”⟩ ++ ⟨“ W ⁡ N − 1 ”⟩
76 pfxcl ⊢ W ∈ Word V → W prefix N − 2 ∈ Word V
77 2 76 syl ⊢ W ∈ Word V ∧ 2 ≤ N → W prefix N − 2 ∈ Word V
78 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 ”⟩
79 77 78 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 ”⟩
80 16 75 79 3eqtrd ⊢ W ∈ Word V ∧ 2 ≤ N → W = W prefix N − 2 ++ ⟨“ W ⁡ N − 2 W ⁡ N − 1 ”⟩