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 e. 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 e. Word V /\ 2 <_ N ) -> W e. Word V )
3 simpr 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> 2 <_ N )
4 3 1 breqtrdi 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> 2 <_ ( # ` W ) )
5 wrdlenge2n0 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> W =/= (/) )
6 2 4 5 syl2anc 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> W =/= (/) )
7 pfxlswccat 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ++ <" ( lastS ` W ) "> ) = W )
8 2 6 7 syl2anc 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ++ <" ( lastS ` W ) "> ) = W )
9 lsw 
 |-  ( W e. 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 e. Word V -> ( lastS ` W ) = ( W ` ( N - 1 ) ) )
13 2 12 syl 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( lastS ` W ) = ( W ` ( N - 1 ) ) )
14 13 s1eqd 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> <" ( lastS ` W ) "> = <" ( W ` ( N - 1 ) ) "> )
15 14 oveq2d 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ++ <" ( lastS ` W ) "> ) = ( ( W prefix ( ( # ` W ) - 1 ) ) ++ <" ( W ` ( N - 1 ) ) "> ) )
16 8 15 eqtr3d 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> W = ( ( W prefix ( ( # ` W ) - 1 ) ) ++ <" ( W ` ( N - 1 ) ) "> ) )
17 pfxcl 
 |-  ( W e. Word V -> ( W prefix ( ( # ` W ) - 1 ) ) e. Word V )
18 2 17 syl 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( W prefix ( ( # ` W ) - 1 ) ) e. Word V )
19 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
20 2 19 syl 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( # ` W ) e. NN0 )
21 1 20 eqeltrid 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> N e. NN0 )
22 nn0ge2m1nn 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. NN )
23 21 3 22 syl2anc 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( N - 1 ) e. NN )
24 10 23 eqeltrrid 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( # ` W ) - 1 ) e. NN )
25 20 nn0red 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( # ` W ) e. RR )
26 25 lem1d 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( # ` W ) - 1 ) <_ ( # ` W ) )
27 pfxn0 
 |-  ( ( W e. Word V /\ ( ( # ` W ) - 1 ) e. NN /\ ( ( # ` W ) - 1 ) <_ ( # ` W ) ) -> ( W prefix ( ( # ` W ) - 1 ) ) =/= (/) )
28 2 24 26 27 syl3anc 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( W prefix ( ( # ` W ) - 1 ) ) =/= (/) )
29 pfxlswccat 
 |-  ( ( ( W prefix ( ( # ` W ) - 1 ) ) e. 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 e. 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 ) e. NN0 /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) )
32 20 4 31 syl2anc 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) )
33 pfxlen 
 |-  ( ( W e. Word V /\ ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( ( # ` W ) - 1 ) )
34 2 32 33 syl2anc 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( ( # ` W ) - 1 ) )
35 34 oveq1d 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) = ( ( ( # ` W ) - 1 ) - 1 ) )
36 0zd 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> 0 e. ZZ )
37 nn0ge2m1nn0 
 |-  ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. NN0 )
38 21 3 37 syl2anc 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( N - 1 ) e. NN0 )
39 10 38 eqeltrrid 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( # ` W ) - 1 ) e. NN0 )
40 39 nn0zd 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( # ` W ) - 1 ) e. ZZ )
41 1zzd 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> 1 e. ZZ )
42 40 41 zsubcld 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( ( # ` W ) - 1 ) - 1 ) e. ZZ )
43 2nn0 
 |-  2 e. NN0
44 43 a1i 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> 2 e. NN0 )
45 nn0sub 
 |-  ( ( 2 e. NN0 /\ N e. NN0 ) -> ( 2 <_ N <-> ( N - 2 ) e. NN0 ) )
46 45 biimpa 
 |-  ( ( ( 2 e. NN0 /\ N e. NN0 ) /\ 2 <_ N ) -> ( N - 2 ) e. NN0 )
47 44 21 3 46 syl21anc 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( N - 2 ) e. NN0 )
48 47 nn0ge0d 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> 0 <_ ( N - 2 ) )
49 21 nn0cnd 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> N e. CC )
50 sub1m1 
 |-  ( N e. CC -> ( ( N - 1 ) - 1 ) = ( N - 2 ) )
51 49 50 syl 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( N - 1 ) - 1 ) = ( N - 2 ) )
52 48 51 breqtrrd 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> 0 <_ ( ( N - 1 ) - 1 ) )
53 10 oveq1i 
 |-  ( ( N - 1 ) - 1 ) = ( ( ( # ` W ) - 1 ) - 1 )
54 52 53 breqtrdi 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> 0 <_ ( ( ( # ` W ) - 1 ) - 1 ) )
55 24 nnred 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( # ` W ) - 1 ) e. RR )
56 55 lem1d 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( ( # ` W ) - 1 ) - 1 ) <_ ( ( # ` W ) - 1 ) )
57 elfz4 
 |-  ( ( ( 0 e. ZZ /\ ( ( # ` W ) - 1 ) e. ZZ /\ ( ( ( # ` W ) - 1 ) - 1 ) e. ZZ ) /\ ( 0 <_ ( ( ( # ` W ) - 1 ) - 1 ) /\ ( ( ( # ` W ) - 1 ) - 1 ) <_ ( ( # ` W ) - 1 ) ) ) -> ( ( ( # ` W ) - 1 ) - 1 ) e. ( 0 ... ( ( # ` W ) - 1 ) ) )
58 36 40 42 54 56 57 syl32anc 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( ( # ` W ) - 1 ) - 1 ) e. ( 0 ... ( ( # ` W ) - 1 ) ) )
59 35 58 eqeltrd 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) e. ( 0 ... ( ( # ` W ) - 1 ) ) )
60 pfxpfx 
 |-  ( ( W e. Word V /\ ( ( # ` W ) - 1 ) e. ( 0 ... ( # ` W ) ) /\ ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) e. ( 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 e. Word V /\ 2 <_ N ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) prefix ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) = ( W prefix ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) )
62 34 10 eqtr4di 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( N - 1 ) )
63 62 oveq1d 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) = ( ( N - 1 ) - 1 ) )
64 63 51 eqtrd 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) = ( N - 2 ) )
65 64 oveq2d 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( W prefix ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) = ( W prefix ( N - 2 ) ) )
66 61 65 eqtrd 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) prefix ( ( # ` ( W prefix ( ( # ` W ) - 1 ) ) ) - 1 ) ) = ( W prefix ( N - 2 ) ) )
67 pfxtrcfvl 
 |-  ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( lastS ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( W ` ( ( # ` W ) - 2 ) ) )
68 2 4 67 syl2anc 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( lastS ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( W ` ( ( # ` W ) - 2 ) ) )
69 1 a1i 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> N = ( # ` W ) )
70 69 fvoveq1d 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( W ` ( N - 2 ) ) = ( W ` ( ( # ` W ) - 2 ) ) )
71 68 70 eqtr4d 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( lastS ` ( W prefix ( ( # ` W ) - 1 ) ) ) = ( W ` ( N - 2 ) ) )
72 71 s1eqd 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> <" ( lastS ` ( W prefix ( ( # ` W ) - 1 ) ) ) "> = <" ( W ` ( N - 2 ) ) "> )
73 66 72 oveq12d 
 |-  ( ( W e. 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 e. Word V /\ 2 <_ N ) -> ( W prefix ( ( # ` W ) - 1 ) ) = ( ( W prefix ( N - 2 ) ) ++ <" ( W ` ( N - 2 ) ) "> ) )
75 74 oveq1d 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ++ <" ( W ` ( N - 1 ) ) "> ) = ( ( ( W prefix ( N - 2 ) ) ++ <" ( W ` ( N - 2 ) ) "> ) ++ <" ( W ` ( N - 1 ) ) "> ) )
76 pfxcl 
 |-  ( W e. Word V -> ( W prefix ( N - 2 ) ) e. Word V )
77 2 76 syl 
 |-  ( ( W e. Word V /\ 2 <_ N ) -> ( W prefix ( N - 2 ) ) e. Word V )
78 ccatw2s1ccatws2 
 |-  ( ( W prefix ( N - 2 ) ) e. 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 e. 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 e. Word V /\ 2 <_ N ) -> W = ( ( W prefix ( N - 2 ) ) ++ <" ( W ` ( N - 2 ) ) ( W ` ( N - 1 ) ) "> ) )