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∈WordV∧2≤N→W=WprefixN−2++⟨“W⁡N−2W⁡N−1”⟩

Proof

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