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 ⊢ 𝑁 = ( ♯ ‘ 𝑊 )
Assertion pfxlsw2ccat ( ( 𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁 ) → 𝑊 = ( ( 𝑊 prefix ( 𝑁 − 2 ) ) ++ ⟨“ ( 𝑊 ‘ ( 𝑁 − 2 ) ) ( 𝑊 ‘ ( 𝑁 − 1 ) ) ”⟩ ) )

Proof

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