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 
|- ( ph -> W e. Word S )
ccatws1f1olast.4 
|- ( ph -> X e. S )
ccatws1f1olast.5 
|- ( ph -> T : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) )
Assertion ccatws1f1olast 
|- ( ph -> ( ( W ++ <" X "> ) o. ( T ++ <" N "> ) ) = ( ( W o. T ) ++ <" X "> ) )

Proof

Step Hyp Ref Expression
1 ccatws1f1olast.1 
 |-  N = ( # ` W )
2 ccatws1f1olast.3 
 |-  ( ph -> W e. Word S )
3 ccatws1f1olast.4 
 |-  ( ph -> X e. S )
4 ccatws1f1olast.5 
 |-  ( ph -> T : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) )
5 lencl 
 |-  ( W e. Word S -> ( # ` W ) e. NN0 )
6 2 5 syl 
 |-  ( ph -> ( # ` W ) e. NN0 )
7 1 6 eqeltrid 
 |-  ( ph -> N e. NN0 )
8 fzossfzop1 
 |-  ( N e. NN0 -> ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) )
9 7 8 syl 
 |-  ( ph -> ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) )
10 sswrd 
 |-  ( ( 0 ..^ N ) C_ ( 0 ..^ ( N + 1 ) ) -> Word ( 0 ..^ N ) C_ Word ( 0 ..^ ( N + 1 ) ) )
11 9 10 syl 
 |-  ( ph -> Word ( 0 ..^ N ) C_ Word ( 0 ..^ ( N + 1 ) ) )
12 f1of 
 |-  ( T : ( 0 ..^ N ) -1-1-onto-> ( 0 ..^ N ) -> T : ( 0 ..^ N ) --> ( 0 ..^ N ) )
13 4 12 syl 
 |-  ( ph -> T : ( 0 ..^ N ) --> ( 0 ..^ N ) )
14 iswrdi 
 |-  ( T : ( 0 ..^ N ) --> ( 0 ..^ N ) -> T e. Word ( 0 ..^ N ) )
15 13 14 syl 
 |-  ( ph -> T e. Word ( 0 ..^ N ) )
16 11 15 sseldd 
 |-  ( ph -> T e. Word ( 0 ..^ ( N + 1 ) ) )
17 fzonn0p1 
 |-  ( N e. NN0 -> N e. ( 0 ..^ ( N + 1 ) ) )
18 7 17 syl 
 |-  ( ph -> N e. ( 0 ..^ ( N + 1 ) ) )
19 18 s1cld 
 |-  ( ph -> <" N "> e. Word ( 0 ..^ ( N + 1 ) ) )
20 1 oveq1i 
 |-  ( N + 1 ) = ( ( # ` W ) + 1 )
21 ccatws1len 
 |-  ( W e. Word S -> ( # ` ( W ++ <" X "> ) ) = ( ( # ` W ) + 1 ) )
22 2 21 syl 
 |-  ( ph -> ( # ` ( W ++ <" X "> ) ) = ( ( # ` W ) + 1 ) )
23 20 22 eqtr4id 
 |-  ( ph -> ( N + 1 ) = ( # ` ( W ++ <" X "> ) ) )
24 ccatws1cl 
 |-  ( ( W e. Word S /\ X e. S ) -> ( W ++ <" X "> ) e. Word S )
25 2 3 24 syl2anc 
 |-  ( ph -> ( W ++ <" X "> ) e. Word S )
26 23 25 wrdfd 
 |-  ( ph -> ( W ++ <" X "> ) : ( 0 ..^ ( N + 1 ) ) --> S )
27 ccatco 
 |-  ( ( T e. Word ( 0 ..^ ( N + 1 ) ) /\ <" N "> e. Word ( 0 ..^ ( N + 1 ) ) /\ ( W ++ <" X "> ) : ( 0 ..^ ( N + 1 ) ) --> S ) -> ( ( W ++ <" X "> ) o. ( T ++ <" N "> ) ) = ( ( ( W ++ <" X "> ) o. T ) ++ ( ( W ++ <" X "> ) o. <" N "> ) ) )
28 16 19 26 27 syl3anc 
 |-  ( ph -> ( ( W ++ <" X "> ) o. ( T ++ <" N "> ) ) = ( ( ( W ++ <" X "> ) o. T ) ++ ( ( W ++ <" X "> ) o. <" N "> ) ) )
29 13 frnd 
 |-  ( ph -> ran T C_ ( 0 ..^ N ) )
30 cores 
 |-  ( ran T C_ ( 0 ..^ N ) -> ( ( ( W ++ <" X "> ) |` ( 0 ..^ N ) ) o. T ) = ( ( W ++ <" X "> ) o. T ) )
31 29 30 syl 
 |-  ( ph -> ( ( ( W ++ <" X "> ) |` ( 0 ..^ N ) ) o. T ) = ( ( W ++ <" X "> ) o. T ) )
32 1 a1i 
 |-  ( ph -> N = ( # ` W ) )
33 32 oveq2d 
 |-  ( ph -> ( ( W ++ <" X "> ) prefix N ) = ( ( W ++ <" X "> ) prefix ( # ` W ) ) )
34 fzossfz 
 |-  ( 0 ..^ ( N + 1 ) ) C_ ( 0 ... ( N + 1 ) )
35 20 a1i 
 |-  ( ph -> ( N + 1 ) = ( ( # ` W ) + 1 ) )
36 35 oveq2d 
 |-  ( ph -> ( 0 ... ( N + 1 ) ) = ( 0 ... ( ( # ` W ) + 1 ) ) )
37 34 36 sseqtrid 
 |-  ( ph -> ( 0 ..^ ( N + 1 ) ) C_ ( 0 ... ( ( # ` W ) + 1 ) ) )
38 37 18 sseldd 
 |-  ( ph -> N e. ( 0 ... ( ( # ` W ) + 1 ) ) )
39 22 oveq2d 
 |-  ( ph -> ( 0 ... ( # ` ( W ++ <" X "> ) ) ) = ( 0 ... ( ( # ` W ) + 1 ) ) )
40 38 39 eleqtrrd 
 |-  ( ph -> N e. ( 0 ... ( # ` ( W ++ <" X "> ) ) ) )
41 pfxres 
 |-  ( ( ( W ++ <" X "> ) e. Word S /\ N e. ( 0 ... ( # ` ( W ++ <" X "> ) ) ) ) -> ( ( W ++ <" X "> ) prefix N ) = ( ( W ++ <" X "> ) |` ( 0 ..^ N ) ) )
42 25 40 41 syl2anc 
 |-  ( ph -> ( ( W ++ <" X "> ) prefix N ) = ( ( W ++ <" X "> ) |` ( 0 ..^ N ) ) )
43 3 s1cld 
 |-  ( ph -> <" X "> e. Word S )
44 pfxccat1 
 |-  ( ( W e. Word S /\ <" X "> e. Word S ) -> ( ( W ++ <" X "> ) prefix ( # ` W ) ) = W )
45 2 43 44 syl2anc 
 |-  ( ph -> ( ( W ++ <" X "> ) prefix ( # ` W ) ) = W )
46 33 42 45 3eqtr3d 
 |-  ( ph -> ( ( W ++ <" X "> ) |` ( 0 ..^ N ) ) = W )
47 46 coeq1d 
 |-  ( ph -> ( ( ( W ++ <" X "> ) |` ( 0 ..^ N ) ) o. T ) = ( W o. T ) )
48 31 47 eqtr3d 
 |-  ( ph -> ( ( W ++ <" X "> ) o. T ) = ( W o. T ) )
49 s1co 
 |-  ( ( N e. ( 0 ..^ ( N + 1 ) ) /\ ( W ++ <" X "> ) : ( 0 ..^ ( N + 1 ) ) --> S ) -> ( ( W ++ <" X "> ) o. <" N "> ) = <" ( ( W ++ <" X "> ) ` N ) "> )
50 18 26 49 syl2anc 
 |-  ( ph -> ( ( W ++ <" X "> ) o. <" N "> ) = <" ( ( W ++ <" X "> ) ` N ) "> )
51 ccats1val2 
 |-  ( ( W e. Word S /\ X e. S /\ N = ( # ` W ) ) -> ( ( W ++ <" X "> ) ` N ) = X )
52 2 3 32 51 syl3anc 
 |-  ( ph -> ( ( W ++ <" X "> ) ` N ) = X )
53 52 s1eqd 
 |-  ( ph -> <" ( ( W ++ <" X "> ) ` N ) "> = <" X "> )
54 50 53 eqtrd 
 |-  ( ph -> ( ( W ++ <" X "> ) o. <" N "> ) = <" X "> )
55 48 54 oveq12d 
 |-  ( ph -> ( ( ( W ++ <" X "> ) o. T ) ++ ( ( W ++ <" X "> ) o. <" N "> ) ) = ( ( W o. T ) ++ <" X "> ) )
56 28 55 eqtrd 
 |-  ( ph -> ( ( W ++ <" X "> ) o. ( T ++ <" N "> ) ) = ( ( W o. T ) ++ <" X "> ) )