Metamath Proof Explorer

Theorem ccatws1f1olast

Description: Two ways to reorder symbols in a word W according to permutation T , and add a last symbol X . (Contributed by Thierry Arnoux, 27-May-2025)

Ref Expression
Hypotheses ccatws1f1olast.1 ⊢ N = W
ccatws1f1olast.3 ⊢ φ → W ∈ Word S
ccatws1f1olast.4 ⊢ φ → X ∈ S
ccatws1f1olast.5 ⊢ φ → T : 0 ..^ N ⟶ 1-1 onto 0 ..^ N
Assertion ccatws1f1olast ⊢ φ → W ++ ⟨“ X ”⟩ ∘ T ++ ⟨“ N ”⟩ = W ∘ T ++ ⟨“ X ”⟩

Proof

Step Hyp Ref Expression
1 ccatws1f1olast.1 ⊢ N = W
2 ccatws1f1olast.3 ⊢ φ → W ∈ Word S
3 ccatws1f1olast.4 ⊢ φ → X ∈ S
4 ccatws1f1olast.5 ⊢ φ → T : 0 ..^ N ⟶ 1-1 onto 0 ..^ N
5 lencl ⊢ W ∈ Word S → W ∈ ℕ 0
6 2 5 syl ⊢ φ → W ∈ ℕ 0
7 1 6 eqeltrid ⊢ φ → N ∈ ℕ 0
8 fzossfzop1 ⊢ N ∈ ℕ 0 → 0 ..^ N ⊆ 0 ..^ N + 1
9 7 8 syl ⊢ φ → 0 ..^ N ⊆ 0 ..^ N + 1
10 sswrd ⊢ 0 ..^ N ⊆ 0 ..^ N + 1 → Word 0 ..^ N ⊆ Word 0 ..^ N + 1
11 9 10 syl ⊢ φ → Word 0 ..^ N ⊆ Word 0 ..^ N + 1
12 f1of ⊢ T : 0 ..^ N ⟶ 1-1 onto 0 ..^ N → T : 0 ..^ N ⟶ 0 ..^ N
13 4 12 syl ⊢ φ → T : 0 ..^ N ⟶ 0 ..^ N
14 iswrdi ⊢ T : 0 ..^ N ⟶ 0 ..^ N → T ∈ Word 0 ..^ N
15 13 14 syl ⊢ φ → T ∈ Word 0 ..^ N
16 11 15 sseldd ⊢ φ → T ∈ Word 0 ..^ N + 1
17 fzonn0p1 ⊢ N ∈ ℕ 0 → N ∈ 0 ..^ N + 1
18 7 17 syl ⊢ φ → N ∈ 0 ..^ N + 1
19 18 s1cld ⊢ φ → ⟨“ N ”⟩ ∈ Word 0 ..^ N + 1
20 1 oveq1i ⊢ N + 1 = W + 1
21 ccatws1len ⊢ W ∈ Word S → W ++ ⟨“ X ”⟩ = W + 1
22 2 21 syl ⊢ φ → W ++ ⟨“ X ”⟩ = W + 1
23 20 22 eqtr4id ⊢ φ → N + 1 = W ++ ⟨“ X ”⟩
24 ccatws1cl ⊢ W ∈ Word S ∧ X ∈ S → W ++ ⟨“ X ”⟩ ∈ Word S
25 2 3 24 syl2anc ⊢ φ → W ++ ⟨“ X ”⟩ ∈ Word S
26 23 25 wrdfd ⊢ φ → W ++ ⟨“ X ”⟩ : 0 ..^ N + 1 ⟶ S
27 ccatco ⊢ T ∈ Word 0 ..^ N + 1 ∧ ⟨“ N ”⟩ ∈ Word 0 ..^ N + 1 ∧ W ++ ⟨“ X ”⟩ : 0 ..^ N + 1 ⟶ S → W ++ ⟨“ X ”⟩ ∘ T ++ ⟨“ N ”⟩ = W ++ ⟨“ X ”⟩ ∘ T ++ W ++ ⟨“ X ”⟩ ∘ ⟨“ N ”⟩
28 16 19 26 27 syl3anc ⊢ φ → W ++ ⟨“ X ”⟩ ∘ T ++ ⟨“ N ”⟩ = W ++ ⟨“ X ”⟩ ∘ T ++ W ++ ⟨“ X ”⟩ ∘ ⟨“ N ”⟩
29 13 frnd ⊢ φ → ran ⁡ T ⊆ 0 ..^ N
30 cores ⊢ ran ⁡ T ⊆ 0 ..^ N → W ++ ⟨“ X ”⟩ ↾ 0 ..^ N ∘ T = W ++ ⟨“ X ”⟩ ∘ T
31 29 30 syl ⊢ φ → W ++ ⟨“ X ”⟩ ↾ 0 ..^ N ∘ T = W ++ ⟨“ X ”⟩ ∘ T
32 1 a1i ⊢ φ → N = W
33 32 oveq2d ⊢ φ → W ++ ⟨“ X ”⟩ prefix N = W ++ ⟨“ X ”⟩ prefix W
34 fzossfz ⊢ 0 ..^ N + 1 ⊆ 0 … N + 1
35 20 a1i ⊢ φ → N + 1 = W + 1
36 35 oveq2d ⊢ φ → 0 … N + 1 = 0 … W + 1
37 34 36 sseqtrid ⊢ φ → 0 ..^ N + 1 ⊆ 0 … W + 1
38 37 18 sseldd ⊢ φ → N ∈ 0 … W + 1
39 22 oveq2d ⊢ φ → 0 … W ++ ⟨“ X ”⟩ = 0 … W + 1
40 38 39 eleqtrrd ⊢ φ → N ∈ 0 … W ++ ⟨“ X ”⟩
41 pfxres ⊢ W ++ ⟨“ X ”⟩ ∈ Word S ∧ N ∈ 0 … W ++ ⟨“ X ”⟩ → W ++ ⟨“ X ”⟩ prefix N = W ++ ⟨“ X ”⟩ ↾ 0 ..^ N
42 25 40 41 syl2anc ⊢ φ → W ++ ⟨“ X ”⟩ prefix N = W ++ ⟨“ X ”⟩ ↾ 0 ..^ N
43 3 s1cld ⊢ φ → ⟨“ X ”⟩ ∈ Word S
44 pfxccat1 ⊢ W ∈ Word S ∧ ⟨“ X ”⟩ ∈ Word S → W ++ ⟨“ X ”⟩ prefix W = W
45 2 43 44 syl2anc ⊢ φ → W ++ ⟨“ X ”⟩ prefix W = W
46 33 42 45 3eqtr3d ⊢ φ → W ++ ⟨“ X ”⟩ ↾ 0 ..^ N = W
47 46 coeq1d ⊢ φ → W ++ ⟨“ X ”⟩ ↾ 0 ..^ N ∘ T = W ∘ T
48 31 47 eqtr3d ⊢ φ → W ++ ⟨“ X ”⟩ ∘ T = W ∘ T
49 s1co ⊢ N ∈ 0 ..^ N + 1 ∧ W ++ ⟨“ X ”⟩ : 0 ..^ N + 1 ⟶ S → W ++ ⟨“ X ”⟩ ∘ ⟨“ N ”⟩ = ⟨“ W ++ ⟨“ X ”⟩ ⁡ N ”⟩
50 18 26 49 syl2anc ⊢ φ → W ++ ⟨“ X ”⟩ ∘ ⟨“ N ”⟩ = ⟨“ W ++ ⟨“ X ”⟩ ⁡ N ”⟩
51 ccats1val2 ⊢ W ∈ Word S ∧ X ∈ S ∧ N = W → W ++ ⟨“ X ”⟩ ⁡ N = X
52 2 3 32 51 syl3anc ⊢ φ → W ++ ⟨“ X ”⟩ ⁡ N = X
53 52 s1eqd ⊢ φ → ⟨“ W ++ ⟨“ X ”⟩ ⁡ N ”⟩ = ⟨“ X ”⟩
54 50 53 eqtrd ⊢ φ → W ++ ⟨“ X ”⟩ ∘ ⟨“ N ”⟩ = ⟨“ X ”⟩
55 48 54 oveq12d ⊢ φ → W ++ ⟨“ X ”⟩ ∘ T ++ W ++ ⟨“ X ”⟩ ∘ ⟨“ N ”⟩ = W ∘ T ++ ⟨“ X ”⟩
56 28 55 eqtrd ⊢ φ → W ++ ⟨“ X ”⟩ ∘ T ++ ⟨“ N ”⟩ = W ∘ T ++ ⟨“ X ”⟩