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 ⊢ φ → I ∈ J
wrdpmtrlast.3 ⊢ φ → W ∈ Word S
wrdpmtrlast.4 ⊢ U = W ∘ s prefix W − 1
Assertion wrdpmtrlast ⊢ φ → ∃ s s : J ⟶ 1-1 onto J ∧ W ∘ s = U ++ ⟨“ W ⁡ I ”⟩

Proof

Step Hyp Ref Expression
1 wrdpmtrlast.1 ⊢ J = 0 ..^ W
2 wrdpmtrlast.2 ⊢ φ → I ∈ J
3 wrdpmtrlast.3 ⊢ φ → W ∈ Word S
4 wrdpmtrlast.4 ⊢ U = W ∘ s prefix W − 1
5 1 2 fzo0pmtrlast ⊢ φ → ∃ s s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I
6 simplr ⊢ φ ∧ 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 ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → s : 0 ..^ W ⟶ J
11 iswrdi ⊢ s : 0 ..^ W ⟶ J → s ∈ Word J
12 10 11 syl ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → s ∈ Word J
13 eqidd ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W = W
14 3 ad2antrr ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W ∈ Word S
15 13 14 wrdfd ⊢ φ ∧ 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 ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W : J ⟶ S
18 lenco ⊢ s ∈ Word J ∧ W : J ⟶ S → W ∘ s = s
19 12 17 18 syl2anc ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W ∘ s = s
20 10 ffund ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → Fun ⁡ s
21 hashfundm ⊢ s ∈ Word J ∧ Fun ⁡ s → s = dom ⁡ s
22 12 20 21 syl2anc ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → s = dom ⁡ s
23 10 fdmd ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → dom ⁡ s = 0 ..^ W
24 23 fveq2d ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → dom ⁡ s = 0 ..^ W
25 2 1 eleqtrdi ⊢ φ → I ∈ 0 ..^ W
26 25 ad2antrr ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → I ∈ 0 ..^ W
27 elfzo0 ⊢ I ∈ 0 ..^ W ↔ I ∈ ℕ 0 ∧ W ∈ ℕ ∧ I < W
28 27 simp2bi ⊢ I ∈ 0 ..^ W → W ∈ ℕ
29 26 28 syl ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W ∈ ℕ
30 29 nnnn0d ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W ∈ ℕ 0
31 hashfzo0 ⊢ W ∈ ℕ 0 → 0 ..^ W = W
32 30 31 syl ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → 0 ..^ W = W
33 22 24 32 3eqtrd ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → s = W
34 19 33 eqtr2d ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W = W ∘ s
35 34 oveq1d ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W − 1 = W ∘ s − 1
36 35 oveq2d ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W ∘ s prefix W − 1 = W ∘ s prefix W ∘ s − 1
37 4 36 eqtrid ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → U = W ∘ s prefix W ∘ s − 1
38 26 ne0d ⊢ φ ∧ 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 ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → s ≠ ∅
43 lswco ⊢ s ∈ Word J ∧ s ≠ ∅ ∧ W : J ⟶ S → lastS ⁡ W ∘ s = W ⁡ lastS ⁡ s
44 12 42 17 43 syl3anc ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → lastS ⁡ W ∘ s = W ⁡ lastS ⁡ s
45 lsw ⊢ s ∈ Word J → lastS ⁡ s = s ⁡ s − 1
46 12 45 syl ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → lastS ⁡ s = s ⁡ s − 1
47 33 oveq1d ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → s − 1 = W − 1
48 47 fveq2d ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → s ⁡ s − 1 = s ⁡ W − 1
49 simpr ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → s ⁡ W − 1 = I
50 46 48 49 3eqtrd ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → lastS ⁡ s = I
51 50 fveq2d ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W ⁡ lastS ⁡ s = W ⁡ I
52 44 51 eqtr2d ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W ⁡ I = lastS ⁡ W ∘ s
53 52 s1eqd ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → ⟨“ W ⁡ I ”⟩ = ⟨“ lastS ⁡ W ∘ s ”⟩
54 37 53 oveq12d ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → U ++ ⟨“ W ⁡ I ”⟩ = W ∘ s prefix W ∘ s − 1 ++ ⟨“ lastS ⁡ W ∘ s ”⟩
55 1 6 14 wrdpmcl ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W ∘ s ∈ Word S
56 fzo0end ⊢ W ∈ ℕ → W − 1 ∈ 0 ..^ W
57 29 56 syl ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W − 1 ∈ 0 ..^ W
58 57 1 eleqtrrdi ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W − 1 ∈ J
59 17 fdmd ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → dom ⁡ W = J
60 58 59 eleqtrrd ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W − 1 ∈ 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 ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → ran ⁡ s = J
64 58 63 eleqtrrd ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W − 1 ∈ ran ⁡ s
65 60 64 elind ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W − 1 ∈ dom ⁡ W ∩ ran ⁡ s
66 65 ne0d ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → dom ⁡ W ∩ ran ⁡ s ≠ ∅
67 coeq0 ⊢ W ∘ s = ∅ ↔ dom ⁡ W ∩ ran ⁡ s = ∅
68 67 necon3bii ⊢ W ∘ s ≠ ∅ ↔ dom ⁡ W ∩ ran ⁡ s ≠ ∅
69 66 68 sylibr ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W ∘ s ≠ ∅
70 pfxlswccat ⊢ W ∘ s ∈ Word S ∧ W ∘ s ≠ ∅ → W ∘ s prefix W ∘ s − 1 ++ ⟨“ lastS ⁡ W ∘ s ”⟩ = W ∘ s
71 55 69 70 syl2anc ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W ∘ s prefix W ∘ s − 1 ++ ⟨“ lastS ⁡ W ∘ s ”⟩ = W ∘ s
72 54 71 eqtr2d ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → W ∘ s = U ++ ⟨“ W ⁡ I ”⟩
73 6 72 jca ⊢ φ ∧ s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → s : J ⟶ 1-1 onto J ∧ W ∘ s = U ++ ⟨“ W ⁡ I ”⟩
74 73 expl ⊢ φ → s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → s : J ⟶ 1-1 onto J ∧ W ∘ s = U ++ ⟨“ W ⁡ I ”⟩
75 74 eximdv ⊢ φ → ∃ s s : J ⟶ 1-1 onto J ∧ s ⁡ W − 1 = I → ∃ s s : J ⟶ 1-1 onto J ∧ W ∘ s = U ++ ⟨“ W ⁡ I ”⟩
76 5 75 mpd ⊢ φ → ∃ s s : J ⟶ 1-1 onto J ∧ W ∘ s = U ++ ⟨“ W ⁡ I ”⟩