Metamath Proof Explorer

Theorem wrdpmtrlast

Description: Reorder a word, so that the symbol given at index I is at the end. (Contributed by Thierry Arnoux, 27-May-2025)

Ref Expression
Hypotheses wrdpmtrlast.1 
|- J = ( 0 ..^ ( # ` W ) )
wrdpmtrlast.2 
|- ( ph -> I e. J )
wrdpmtrlast.3 
|- ( ph -> W e. Word S )
wrdpmtrlast.4 
|- U = ( ( W o. s ) prefix ( ( # ` W ) - 1 ) )
Assertion wrdpmtrlast 
|- ( ph -> E. s ( s : J -1-1-onto-> J /\ ( W o. s ) = ( U ++ <" ( W ` I ) "> ) ) )

Proof

Step Hyp Ref Expression
1 wrdpmtrlast.1 
 |-  J = ( 0 ..^ ( # ` W ) )
2 wrdpmtrlast.2 
 |-  ( ph -> I e. J )
3 wrdpmtrlast.3 
 |-  ( ph -> W e. Word S )
4 wrdpmtrlast.4 
 |-  U = ( ( W o. s ) prefix ( ( # ` W ) - 1 ) )
5 1 2 fzo0pmtrlast 
 |-  ( ph -> E. s ( s : J -1-1-onto-> J /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) )
6 simplr 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> s : J -1-1-onto-> J )
7 f1of 
 |-  ( s : J -1-1-onto-> J -> s : J --> J )
8 1 feq2i 
 |-  ( s : J --> J <-> s : ( 0 ..^ ( # ` W ) ) --> J )
9 7 8 sylib 
 |-  ( s : J -1-1-onto-> J -> s : ( 0 ..^ ( # ` W ) ) --> J )
10 6 9 syl 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> s : ( 0 ..^ ( # ` W ) ) --> J )
11 iswrdi 
 |-  ( s : ( 0 ..^ ( # ` W ) ) --> J -> s e. Word J )
12 10 11 syl 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> s e. Word J )
13 eqidd 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( # ` W ) = ( # ` W ) )
14 3 ad2antrr 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> W e. Word S )
15 13 14 wrdfd 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> W : ( 0 ..^ ( # ` W ) ) --> S )
16 1 feq2i 
 |-  ( W : J --> S <-> W : ( 0 ..^ ( # ` W ) ) --> S )
17 15 16 sylibr 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> W : J --> S )
18 lenco 
 |-  ( ( s e. Word J /\ W : J --> S ) -> ( # ` ( W o. s ) ) = ( # ` s ) )
19 12 17 18 syl2anc 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( # ` ( W o. s ) ) = ( # ` s ) )
20 10 ffund 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> Fun s )
21 hashfundm 
 |-  ( ( s e. Word J /\ Fun s ) -> ( # ` s ) = ( # ` dom s ) )
22 12 20 21 syl2anc 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( # ` s ) = ( # ` dom s ) )
23 10 fdmd 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> dom s = ( 0 ..^ ( # ` W ) ) )
24 23 fveq2d 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( # ` dom s ) = ( # ` ( 0 ..^ ( # ` W ) ) ) )
25 2 1 eleqtrdi 
 |-  ( ph -> I e. ( 0 ..^ ( # ` W ) ) )
26 25 ad2antrr 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> I e. ( 0 ..^ ( # ` W ) ) )
27 elfzo0 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) <-> ( I e. NN0 /\ ( # ` W ) e. NN /\ I < ( # ` W ) ) )
28 27 simp2bi 
 |-  ( I e. ( 0 ..^ ( # ` W ) ) -> ( # ` W ) e. NN )
29 26 28 syl 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( # ` W ) e. NN )
30 29 nnnn0d 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( # ` W ) e. NN0 )
31 hashfzo0 
 |-  ( ( # ` W ) e. NN0 -> ( # ` ( 0 ..^ ( # ` W ) ) ) = ( # ` W ) )
32 30 31 syl 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( # ` ( 0 ..^ ( # ` W ) ) ) = ( # ` W ) )
33 22 24 32 3eqtrd 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( # ` s ) = ( # ` W ) )
34 19 33 eqtr2d 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( # ` W ) = ( # ` ( W o. s ) ) )
35 34 oveq1d 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( ( # ` W ) - 1 ) = ( ( # ` ( W o. s ) ) - 1 ) )
36 35 oveq2d 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( ( W o. s ) prefix ( ( # ` W ) - 1 ) ) = ( ( W o. s ) prefix ( ( # ` ( W o. s ) ) - 1 ) ) )
37 4 36 eqtrid 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> U = ( ( W o. s ) prefix ( ( # ` ( W o. s ) ) - 1 ) ) )
38 26 ne0d 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( 0 ..^ ( # ` W ) ) =/= (/) )
39 f0dom0 
 |-  ( s : ( 0 ..^ ( # ` W ) ) --> J -> ( ( 0 ..^ ( # ` W ) ) = (/) <-> s = (/) ) )
40 39 necon3bid 
 |-  ( s : ( 0 ..^ ( # ` W ) ) --> J -> ( ( 0 ..^ ( # ` W ) ) =/= (/) <-> s =/= (/) ) )
41 40 biimpa 
 |-  ( ( s : ( 0 ..^ ( # ` W ) ) --> J /\ ( 0 ..^ ( # ` W ) ) =/= (/) ) -> s =/= (/) )
42 10 38 41 syl2anc 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> s =/= (/) )
43 lswco 
 |-  ( ( s e. Word J /\ s =/= (/) /\ W : J --> S ) -> ( lastS ` ( W o. s ) ) = ( W ` ( lastS ` s ) ) )
44 12 42 17 43 syl3anc 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( lastS ` ( W o. s ) ) = ( W ` ( lastS ` s ) ) )
45 lsw 
 |-  ( s e. Word J -> ( lastS ` s ) = ( s ` ( ( # ` s ) - 1 ) ) )
46 12 45 syl 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( lastS ` s ) = ( s ` ( ( # ` s ) - 1 ) ) )
47 33 oveq1d 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( ( # ` s ) - 1 ) = ( ( # ` W ) - 1 ) )
48 47 fveq2d 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( s ` ( ( # ` s ) - 1 ) ) = ( s ` ( ( # ` W ) - 1 ) ) )
49 simpr 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( s ` ( ( # ` W ) - 1 ) ) = I )
50 46 48 49 3eqtrd 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( lastS ` s ) = I )
51 50 fveq2d 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( W ` ( lastS ` s ) ) = ( W ` I ) )
52 44 51 eqtr2d 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( W ` I ) = ( lastS ` ( W o. s ) ) )
53 52 s1eqd 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> <" ( W ` I ) "> = <" ( lastS ` ( W o. s ) ) "> )
54 37 53 oveq12d 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( U ++ <" ( W ` I ) "> ) = ( ( ( W o. s ) prefix ( ( # ` ( W o. s ) ) - 1 ) ) ++ <" ( lastS ` ( W o. s ) ) "> ) )
55 1 6 14 wrdpmcl 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( W o. s ) e. Word S )
56 fzo0end 
 |-  ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
57 29 56 syl 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
58 57 1 eleqtrrdi 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( ( # ` W ) - 1 ) e. J )
59 17 fdmd 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> dom W = J )
60 58 59 eleqtrrd 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( ( # ` W ) - 1 ) e. dom W )
61 dff1o5 
 |-  ( s : J -1-1-onto-> J <-> ( s : J -1-1-> J /\ ran s = J ) )
62 61 simprbi 
 |-  ( s : J -1-1-onto-> J -> ran s = J )
63 6 62 syl 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ran s = J )
64 58 63 eleqtrrd 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( ( # ` W ) - 1 ) e. ran s )
65 60 64 elind 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( ( # ` W ) - 1 ) e. ( dom W i^i ran s ) )
66 65 ne0d 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( dom W i^i ran s ) =/= (/) )
67 coeq0 
 |-  ( ( W o. s ) = (/) <-> ( dom W i^i ran s ) = (/) )
68 67 necon3bii 
 |-  ( ( W o. s ) =/= (/) <-> ( dom W i^i ran s ) =/= (/) )
69 66 68 sylibr 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( W o. s ) =/= (/) )
70 pfxlswccat 
 |-  ( ( ( W o. s ) e. Word S /\ ( W o. s ) =/= (/) ) -> ( ( ( W o. s ) prefix ( ( # ` ( W o. s ) ) - 1 ) ) ++ <" ( lastS ` ( W o. s ) ) "> ) = ( W o. s ) )
71 55 69 70 syl2anc 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( ( ( W o. s ) prefix ( ( # ` ( W o. s ) ) - 1 ) ) ++ <" ( lastS ` ( W o. s ) ) "> ) = ( W o. s ) )
72 54 71 eqtr2d 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( W o. s ) = ( U ++ <" ( W ` I ) "> ) )
73 6 72 jca 
 |-  ( ( ( ph /\ s : J -1-1-onto-> J ) /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( s : J -1-1-onto-> J /\ ( W o. s ) = ( U ++ <" ( W ` I ) "> ) ) )
74 73 expl 
 |-  ( ph -> ( ( s : J -1-1-onto-> J /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> ( s : J -1-1-onto-> J /\ ( W o. s ) = ( U ++ <" ( W ` I ) "> ) ) ) )
75 74 eximdv 
 |-  ( ph -> ( E. s ( s : J -1-1-onto-> J /\ ( s ` ( ( # ` W ) - 1 ) ) = I ) -> E. s ( s : J -1-1-onto-> J /\ ( W o. s ) = ( U ++ <" ( W ` I ) "> ) ) ) )
76 5 75 mpd 
 |-  ( ph -> E. s ( s : J -1-1-onto-> J /\ ( W o. s ) = ( U ++ <" ( W ` I ) "> ) ) )