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	⊢ 𝑁 = ( ♯ ‘ 𝑊 )
	ccatws1f1olast.3	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
	ccatws1f1olast.4	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	ccatws1f1olast.5	⊢ ( 𝜑 → 𝑇 : ( 0 ..^ 𝑁 ) –1-1-onto→ ( 0 ..^ 𝑁 ) )
Assertion	ccatws1f1olast	⊢ ( 𝜑 → ( ( 𝑊 ++ ⟨“ 𝑋 ”⟩ ) ∘ ( 𝑇 ++ ⟨“ 𝑁 ”⟩ ) ) = ( ( 𝑊 ∘ 𝑇 ) ++ ⟨“ 𝑋 ”⟩ ) )

Proof

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

Metamath Proof Explorer

Theorem ccatws1f1olast

Proof