Metamath Proof Explorer

Theorem efgredleme

Description: Lemma for efgred . (Contributed by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 15-Oct-2022)

Ref Expression
Hypotheses efgval.w 
|- W = ( _I ` Word ( I X. 2o ) )
efgval.r 
|- .~ = ( ~FG ` I )
efgval2.m 
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
efgval2.t 
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
efgred.d 
|- D = ( W \ U_ x e. W ran ( T ` x ) )
efgred.s 
|- S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
efgredlem.1 
|- ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
efgredlem.2 
|- ( ph -> A e. dom S )
efgredlem.3 
|- ( ph -> B e. dom S )
efgredlem.4 
|- ( ph -> ( S ` A ) = ( S ` B ) )
efgredlem.5 
|- ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )
efgredlemb.k 
|- K = ( ( ( # ` A ) - 1 ) - 1 )
efgredlemb.l 
|- L = ( ( ( # ` B ) - 1 ) - 1 )
efgredlemb.p 
|- ( ph -> P e. ( 0 ... ( # ` ( A ` K ) ) ) )
efgredlemb.q 
|- ( ph -> Q e. ( 0 ... ( # ` ( B ` L ) ) ) )
efgredlemb.u 
|- ( ph -> U e. ( I X. 2o ) )
efgredlemb.v 
|- ( ph -> V e. ( I X. 2o ) )
efgredlemb.6 
|- ( ph -> ( S ` A ) = ( P ( T ` ( A ` K ) ) U ) )
efgredlemb.7 
|- ( ph -> ( S ` B ) = ( Q ( T ` ( B ` L ) ) V ) )
efgredlemb.8 
|- ( ph -> -. ( A ` K ) = ( B ` L ) )
efgredlemd.9 
|- ( ph -> P e. ( ZZ>= ` ( Q + 2 ) ) )
efgredlemd.c 
|- ( ph -> C e. dom S )
efgredlemd.sc 
|- ( ph -> ( S ` C ) = ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )
Assertion efgredleme 
|- ( ph -> ( ( A ` K ) e. ran ( T ` ( S ` C ) ) /\ ( B ` L ) e. ran ( T ` ( S ` C ) ) ) )

Proof

Step Hyp Ref Expression
1 efgval.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
2 efgval.r 
 |-  .~ = ( ~FG ` I )
3 efgval2.m 
 |-  M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
4 efgval2.t 
 |-  T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
5 efgred.d 
 |-  D = ( W \ U_ x e. W ran ( T ` x ) )
6 efgred.s 
 |-  S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
7 efgredlem.1 
 |-  ( ph -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
8 efgredlem.2 
 |-  ( ph -> A e. dom S )
9 efgredlem.3 
 |-  ( ph -> B e. dom S )
10 efgredlem.4 
 |-  ( ph -> ( S ` A ) = ( S ` B ) )
11 efgredlem.5 
 |-  ( ph -> -. ( A ` 0 ) = ( B ` 0 ) )
12 efgredlemb.k 
 |-  K = ( ( ( # ` A ) - 1 ) - 1 )
13 efgredlemb.l 
 |-  L = ( ( ( # ` B ) - 1 ) - 1 )
14 efgredlemb.p 
 |-  ( ph -> P e. ( 0 ... ( # ` ( A ` K ) ) ) )
15 efgredlemb.q 
 |-  ( ph -> Q e. ( 0 ... ( # ` ( B ` L ) ) ) )
16 efgredlemb.u 
 |-  ( ph -> U e. ( I X. 2o ) )
17 efgredlemb.v 
 |-  ( ph -> V e. ( I X. 2o ) )
18 efgredlemb.6 
 |-  ( ph -> ( S ` A ) = ( P ( T ` ( A ` K ) ) U ) )
19 efgredlemb.7 
 |-  ( ph -> ( S ` B ) = ( Q ( T ` ( B ` L ) ) V ) )
20 efgredlemb.8 
 |-  ( ph -> -. ( A ` K ) = ( B ` L ) )
21 efgredlemd.9 
 |-  ( ph -> P e. ( ZZ>= ` ( Q + 2 ) ) )
22 efgredlemd.c 
 |-  ( ph -> C e. dom S )
23 efgredlemd.sc 
 |-  ( ph -> ( S ` C ) = ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )
24 1 2 3 4 5 6 efgsf 
 |-  S : { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W
25 24 fdmi 
 |-  dom S = { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) }
26 25 feq2i 
 |-  ( S : dom S --> W <-> S : { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W )
27 24 26 mpbir 
 |-  S : dom S --> W
28 27 ffvelrni 
 |-  ( C e. dom S -> ( S ` C ) e. W )
29 22 28 syl 
 |-  ( ph -> ( S ` C ) e. W )
30 elfzuz 
 |-  ( Q e. ( 0 ... ( # ` ( B ` L ) ) ) -> Q e. ( ZZ>= ` 0 ) )
31 15 30 syl 
 |-  ( ph -> Q e. ( ZZ>= ` 0 ) )
32 23 fveq2d 
 |-  ( ph -> ( # ` ( S ` C ) ) = ( # ` ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) )
33 fviss 
 |-  ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
34 1 33 eqsstri 
 |-  W C_ Word ( I X. 2o )
35 1 2 3 4 5 6 7 8 9 10 11 12 13 efgredlemf 
 |-  ( ph -> ( ( A ` K ) e. W /\ ( B ` L ) e. W ) )
36 35 simprd 
 |-  ( ph -> ( B ` L ) e. W )
37 34 36 sseldi 
 |-  ( ph -> ( B ` L ) e. Word ( I X. 2o ) )
38 pfxcl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) )
39 37 38 syl 
 |-  ( ph -> ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) )
40 35 simpld 
 |-  ( ph -> ( A ` K ) e. W )
41 34 40 sseldi 
 |-  ( ph -> ( A ` K ) e. Word ( I X. 2o ) )
42 swrdcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) )
43 41 42 syl 
 |-  ( ph -> ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) )
44 ccatlen 
 |-  ( ( ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) /\ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) ) -> ( # ` ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) = ( ( # ` ( ( B ` L ) prefix Q ) ) + ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) )
45 39 43 44 syl2anc 
 |-  ( ph -> ( # ` ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) = ( ( # ` ( ( B ` L ) prefix Q ) ) + ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) )
46 pfxlen 
 |-  ( ( ( B ` L ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( # ` ( ( B ` L ) prefix Q ) ) = Q )
47 37 15 46 syl2anc 
 |-  ( ph -> ( # ` ( ( B ` L ) prefix Q ) ) = Q )
48 2nn0 
 |-  2 e. NN0
49 uzaddcl 
 |-  ( ( Q e. ( ZZ>= ` 0 ) /\ 2 e. NN0 ) -> ( Q + 2 ) e. ( ZZ>= ` 0 ) )
50 31 48 49 sylancl 
 |-  ( ph -> ( Q + 2 ) e. ( ZZ>= ` 0 ) )
51 elfzuz3 
 |-  ( P e. ( 0 ... ( # ` ( A ` K ) ) ) -> ( # ` ( A ` K ) ) e. ( ZZ>= ` P ) )
52 14 51 syl 
 |-  ( ph -> ( # ` ( A ` K ) ) e. ( ZZ>= ` P ) )
53 uztrn 
 |-  ( ( ( # ` ( A ` K ) ) e. ( ZZ>= ` P ) /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) -> ( # ` ( A ` K ) ) e. ( ZZ>= ` ( Q + 2 ) ) )
54 52 21 53 syl2anc 
 |-  ( ph -> ( # ` ( A ` K ) ) e. ( ZZ>= ` ( Q + 2 ) ) )
55 elfzuzb 
 |-  ( ( Q + 2 ) e. ( 0 ... ( # ` ( A ` K ) ) ) <-> ( ( Q + 2 ) e. ( ZZ>= ` 0 ) /\ ( # ` ( A ` K ) ) e. ( ZZ>= ` ( Q + 2 ) ) ) )
56 50 54 55 sylanbrc 
 |-  ( ph -> ( Q + 2 ) e. ( 0 ... ( # ` ( A ` K ) ) ) )
57 lencl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( # ` ( A ` K ) ) e. NN0 )
58 41 57 syl 
 |-  ( ph -> ( # ` ( A ` K ) ) e. NN0 )
59 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
60 58 59 eleqtrdi 
 |-  ( ph -> ( # ` ( A ` K ) ) e. ( ZZ>= ` 0 ) )
61 eluzfz2 
 |-  ( ( # ` ( A ` K ) ) e. ( ZZ>= ` 0 ) -> ( # ` ( A ` K ) ) e. ( 0 ... ( # ` ( A ` K ) ) ) )
62 60 61 syl 
 |-  ( ph -> ( # ` ( A ` K ) ) e. ( 0 ... ( # ` ( A ` K ) ) ) )
63 swrdlen 
 |-  ( ( ( A ` K ) e. Word ( I X. 2o ) /\ ( Q + 2 ) e. ( 0 ... ( # ` ( A ` K ) ) ) /\ ( # ` ( A ` K ) ) e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( # ` ( A ` K ) ) - ( Q + 2 ) ) )
64 41 56 62 63 syl3anc 
 |-  ( ph -> ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( # ` ( A ` K ) ) - ( Q + 2 ) ) )
65 47 64 oveq12d 
 |-  ( ph -> ( ( # ` ( ( B ` L ) prefix Q ) ) + ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) = ( Q + ( ( # ` ( A ` K ) ) - ( Q + 2 ) ) ) )
66 elfzelz 
 |-  ( Q e. ( 0 ... ( # ` ( B ` L ) ) ) -> Q e. ZZ )
67 15 66 syl 
 |-  ( ph -> Q e. ZZ )
68 67 zcnd 
 |-  ( ph -> Q e. CC )
69 58 nn0cnd 
 |-  ( ph -> ( # ` ( A ` K ) ) e. CC )
70 2z 
 |-  2 e. ZZ
71 zaddcl 
 |-  ( ( Q e. ZZ /\ 2 e. ZZ ) -> ( Q + 2 ) e. ZZ )
72 67 70 71 sylancl 
 |-  ( ph -> ( Q + 2 ) e. ZZ )
73 72 zcnd 
 |-  ( ph -> ( Q + 2 ) e. CC )
74 68 69 73 addsubassd 
 |-  ( ph -> ( ( Q + ( # ` ( A ` K ) ) ) - ( Q + 2 ) ) = ( Q + ( ( # ` ( A ` K ) ) - ( Q + 2 ) ) ) )
75 2cn 
 |-  2 e. CC
76 75 a1i 
 |-  ( ph -> 2 e. CC )
77 68 69 76 pnpcand 
 |-  ( ph -> ( ( Q + ( # ` ( A ` K ) ) ) - ( Q + 2 ) ) = ( ( # ` ( A ` K ) ) - 2 ) )
78 65 74 77 3eqtr2d 
 |-  ( ph -> ( ( # ` ( ( B ` L ) prefix Q ) ) + ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) = ( ( # ` ( A ` K ) ) - 2 ) )
79 32 45 78 3eqtrd 
 |-  ( ph -> ( # ` ( S ` C ) ) = ( ( # ` ( A ` K ) ) - 2 ) )
80 elfzelz 
 |-  ( P e. ( 0 ... ( # ` ( A ` K ) ) ) -> P e. ZZ )
81 14 80 syl 
 |-  ( ph -> P e. ZZ )
82 zsubcl 
 |-  ( ( P e. ZZ /\ 2 e. ZZ ) -> ( P - 2 ) e. ZZ )
83 81 70 82 sylancl 
 |-  ( ph -> ( P - 2 ) e. ZZ )
84 70 a1i 
 |-  ( ph -> 2 e. ZZ )
85 81 zcnd 
 |-  ( ph -> P e. CC )
86 npcan 
 |-  ( ( P e. CC /\ 2 e. CC ) -> ( ( P - 2 ) + 2 ) = P )
87 85 75 86 sylancl 
 |-  ( ph -> ( ( P - 2 ) + 2 ) = P )
88 87 fveq2d 
 |-  ( ph -> ( ZZ>= ` ( ( P - 2 ) + 2 ) ) = ( ZZ>= ` P ) )
89 52 88 eleqtrrd 
 |-  ( ph -> ( # ` ( A ` K ) ) e. ( ZZ>= ` ( ( P - 2 ) + 2 ) ) )
90 eluzsub 
 |-  ( ( ( P - 2 ) e. ZZ /\ 2 e. ZZ /\ ( # ` ( A ` K ) ) e. ( ZZ>= ` ( ( P - 2 ) + 2 ) ) ) -> ( ( # ` ( A ` K ) ) - 2 ) e. ( ZZ>= ` ( P - 2 ) ) )
91 83 84 89 90 syl3anc 
 |-  ( ph -> ( ( # ` ( A ` K ) ) - 2 ) e. ( ZZ>= ` ( P - 2 ) ) )
92 79 91 eqeltrd 
 |-  ( ph -> ( # ` ( S ` C ) ) e. ( ZZ>= ` ( P - 2 ) ) )
93 eluzsub 
 |-  ( ( Q e. ZZ /\ 2 e. ZZ /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) -> ( P - 2 ) e. ( ZZ>= ` Q ) )
94 67 84 21 93 syl3anc 
 |-  ( ph -> ( P - 2 ) e. ( ZZ>= ` Q ) )
95 uztrn 
 |-  ( ( ( # ` ( S ` C ) ) e. ( ZZ>= ` ( P - 2 ) ) /\ ( P - 2 ) e. ( ZZ>= ` Q ) ) -> ( # ` ( S ` C ) ) e. ( ZZ>= ` Q ) )
96 92 94 95 syl2anc 
 |-  ( ph -> ( # ` ( S ` C ) ) e. ( ZZ>= ` Q ) )
97 elfzuzb 
 |-  ( Q e. ( 0 ... ( # ` ( S ` C ) ) ) <-> ( Q e. ( ZZ>= ` 0 ) /\ ( # ` ( S ` C ) ) e. ( ZZ>= ` Q ) ) )
98 31 96 97 sylanbrc 
 |-  ( ph -> Q e. ( 0 ... ( # ` ( S ` C ) ) ) )
99 1 2 3 4 efgtval 
 |-  ( ( ( S ` C ) e. W /\ Q e. ( 0 ... ( # ` ( S ` C ) ) ) /\ V e. ( I X. 2o ) ) -> ( Q ( T ` ( S ` C ) ) V ) = ( ( S ` C ) splice <. Q , Q , <" V ( M ` V ) "> >. ) )
100 29 98 17 99 syl3anc 
 |-  ( ph -> ( Q ( T ` ( S ` C ) ) V ) = ( ( S ` C ) splice <. Q , Q , <" V ( M ` V ) "> >. ) )
101 pfxcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) prefix Q ) e. Word ( I X. 2o ) )
102 41 101 syl 
 |-  ( ph -> ( ( A ` K ) prefix Q ) e. Word ( I X. 2o ) )
103 wrd0 
 |-  (/) e. Word ( I X. 2o )
104 103 a1i 
 |-  ( ph -> (/) e. Word ( I X. 2o ) )
105 3 efgmf 
 |-  M : ( I X. 2o ) --> ( I X. 2o )
106 105 ffvelrni 
 |-  ( V e. ( I X. 2o ) -> ( M ` V ) e. ( I X. 2o ) )
107 17 106 syl 
 |-  ( ph -> ( M ` V ) e. ( I X. 2o ) )
108 17 107 s2cld 
 |-  ( ph -> <" V ( M ` V ) "> e. Word ( I X. 2o ) )
109 67 zred 
 |-  ( ph -> Q e. RR )
110 nn0addge1 
 |-  ( ( Q e. RR /\ 2 e. NN0 ) -> Q <_ ( Q + 2 ) )
111 109 48 110 sylancl 
 |-  ( ph -> Q <_ ( Q + 2 ) )
112 eluz2 
 |-  ( ( Q + 2 ) e. ( ZZ>= ` Q ) <-> ( Q e. ZZ /\ ( Q + 2 ) e. ZZ /\ Q <_ ( Q + 2 ) ) )
113 67 72 111 112 syl3anbrc 
 |-  ( ph -> ( Q + 2 ) e. ( ZZ>= ` Q ) )
114 uztrn 
 |-  ( ( P e. ( ZZ>= ` ( Q + 2 ) ) /\ ( Q + 2 ) e. ( ZZ>= ` Q ) ) -> P e. ( ZZ>= ` Q ) )
115 21 113 114 syl2anc 
 |-  ( ph -> P e. ( ZZ>= ` Q ) )
116 elfzuzb 
 |-  ( Q e. ( 0 ... P ) <-> ( Q e. ( ZZ>= ` 0 ) /\ P e. ( ZZ>= ` Q ) ) )
117 31 115 116 sylanbrc 
 |-  ( ph -> Q e. ( 0 ... P ) )
118 ccatpfx 
 |-  ( ( ( A ` K ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , P >. ) ) = ( ( A ` K ) prefix P ) )
119 41 117 14 118 syl3anc 
 |-  ( ph -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , P >. ) ) = ( ( A ` K ) prefix P ) )
120 119 oveq1d 
 |-  ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , P >. ) ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( A ` K ) prefix P ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) )
121 pfxcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) )
122 41 121 syl 
 |-  ( ph -> ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) )
123 105 ffvelrni 
 |-  ( U e. ( I X. 2o ) -> ( M ` U ) e. ( I X. 2o ) )
124 16 123 syl 
 |-  ( ph -> ( M ` U ) e. ( I X. 2o ) )
125 16 124 s2cld 
 |-  ( ph -> <" U ( M ` U ) "> e. Word ( I X. 2o ) )
126 swrdcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) )
127 41 126 syl 
 |-  ( ph -> ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) )
128 ccatass 
 |-  ( ( ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) /\ <" U ( M ` U ) "> e. Word ( I X. 2o ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) ) -> ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( A ` K ) prefix P ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) )
129 122 125 127 128 syl3anc 
 |-  ( ph -> ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( A ` K ) prefix P ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) )
130 1 2 3 4 efgtval 
 |-  ( ( ( A ` K ) e. W /\ P e. ( 0 ... ( # ` ( A ` K ) ) ) /\ U e. ( I X. 2o ) ) -> ( P ( T ` ( A ` K ) ) U ) = ( ( A ` K ) splice <. P , P , <" U ( M ` U ) "> >. ) )
131 40 14 16 130 syl3anc 
 |-  ( ph -> ( P ( T ` ( A ` K ) ) U ) = ( ( A ` K ) splice <. P , P , <" U ( M ` U ) "> >. ) )
132 splval 
 |-  ( ( ( A ` K ) e. W /\ ( P e. ( 0 ... ( # ` ( A ` K ) ) ) /\ P e. ( 0 ... ( # ` ( A ` K ) ) ) /\ <" U ( M ` U ) "> e. Word ( I X. 2o ) ) ) -> ( ( A ` K ) splice <. P , P , <" U ( M ` U ) "> >. ) = ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) )
133 40 14 14 125 132 syl13anc 
 |-  ( ph -> ( ( A ` K ) splice <. P , P , <" U ( M ` U ) "> >. ) = ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) )
134 18 131 133 3eqtrd 
 |-  ( ph -> ( S ` A ) = ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) )
135 1 2 3 4 efgtval 
 |-  ( ( ( B ` L ) e. W /\ Q e. ( 0 ... ( # ` ( B ` L ) ) ) /\ V e. ( I X. 2o ) ) -> ( Q ( T ` ( B ` L ) ) V ) = ( ( B ` L ) splice <. Q , Q , <" V ( M ` V ) "> >. ) )
136 36 15 17 135 syl3anc 
 |-  ( ph -> ( Q ( T ` ( B ` L ) ) V ) = ( ( B ` L ) splice <. Q , Q , <" V ( M ` V ) "> >. ) )
137 splval 
 |-  ( ( ( B ` L ) e. W /\ ( Q e. ( 0 ... ( # ` ( B ` L ) ) ) /\ Q e. ( 0 ... ( # ` ( B ` L ) ) ) /\ <" V ( M ` V ) "> e. Word ( I X. 2o ) ) ) -> ( ( B ` L ) splice <. Q , Q , <" V ( M ` V ) "> >. ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
138 36 15 15 108 137 syl13anc 
 |-  ( ph -> ( ( B ` L ) splice <. Q , Q , <" V ( M ` V ) "> >. ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
139 19 136 138 3eqtrd 
 |-  ( ph -> ( S ` B ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
140 10 134 139 3eqtr3d 
 |-  ( ph -> ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
141 120 129 140 3eqtr2d 
 |-  ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , P >. ) ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
142 swrdcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. Q , P >. ) e. Word ( I X. 2o ) )
143 41 142 syl 
 |-  ( ph -> ( ( A ` K ) substr <. Q , P >. ) e. Word ( I X. 2o ) )
144 ccatcl 
 |-  ( ( <" U ( M ` U ) "> e. Word ( I X. 2o ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) ) -> ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) )
145 125 127 144 syl2anc 
 |-  ( ph -> ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) )
146 ccatass 
 |-  ( ( ( ( A ` K ) prefix Q ) e. Word ( I X. 2o ) /\ ( ( A ` K ) substr <. Q , P >. ) e. Word ( I X. 2o ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) ) -> ( ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , P >. ) ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( A ` K ) prefix Q ) ++ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) )
147 102 143 145 146 syl3anc 
 |-  ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , P >. ) ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( A ` K ) prefix Q ) ++ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) )
148 swrdcl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
149 37 148 syl 
 |-  ( ph -> ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
150 ccatass 
 |-  ( ( ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) /\ <" V ( M ` V ) "> e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) -> ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) )
151 39 108 149 150 syl3anc 
 |-  ( ph -> ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) )
152 141 147 151 3eqtr3d 
 |-  ( ph -> ( ( ( A ` K ) prefix Q ) ++ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) = ( ( ( B ` L ) prefix Q ) ++ ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) )
153 ccatcl 
 |-  ( ( ( ( A ` K ) substr <. Q , P >. ) e. Word ( I X. 2o ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) ) -> ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) e. Word ( I X. 2o ) )
154 143 145 153 syl2anc 
 |-  ( ph -> ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) e. Word ( I X. 2o ) )
155 ccatcl 
 |-  ( ( <" V ( M ` V ) "> e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) -> ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) e. Word ( I X. 2o ) )
156 108 149 155 syl2anc 
 |-  ( ph -> ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) e. Word ( I X. 2o ) )
157 uztrn 
 |-  ( ( ( # ` ( A ` K ) ) e. ( ZZ>= ` P ) /\ P e. ( ZZ>= ` Q ) ) -> ( # ` ( A ` K ) ) e. ( ZZ>= ` Q ) )
158 52 115 157 syl2anc 
 |-  ( ph -> ( # ` ( A ` K ) ) e. ( ZZ>= ` Q ) )
159 elfzuzb 
 |-  ( Q e. ( 0 ... ( # ` ( A ` K ) ) ) <-> ( Q e. ( ZZ>= ` 0 ) /\ ( # ` ( A ` K ) ) e. ( ZZ>= ` Q ) ) )
160 31 158 159 sylanbrc 
 |-  ( ph -> Q e. ( 0 ... ( # ` ( A ` K ) ) ) )
161 pfxlen 
 |-  ( ( ( A ` K ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( # ` ( ( A ` K ) prefix Q ) ) = Q )
162 41 160 161 syl2anc 
 |-  ( ph -> ( # ` ( ( A ` K ) prefix Q ) ) = Q )
163 162 47 eqtr4d 
 |-  ( ph -> ( # ` ( ( A ` K ) prefix Q ) ) = ( # ` ( ( B ` L ) prefix Q ) ) )
164 ccatopth 
 |-  ( ( ( ( ( A ` K ) prefix Q ) e. Word ( I X. 2o ) /\ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) e. Word ( I X. 2o ) ) /\ ( ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) /\ ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) e. Word ( I X. 2o ) ) /\ ( # ` ( ( A ` K ) prefix Q ) ) = ( # ` ( ( B ` L ) prefix Q ) ) ) -> ( ( ( ( A ` K ) prefix Q ) ++ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) = ( ( ( B ` L ) prefix Q ) ++ ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) <-> ( ( ( A ` K ) prefix Q ) = ( ( B ` L ) prefix Q ) /\ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) ) )
165 102 154 39 156 163 164 syl221anc 
 |-  ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) = ( ( ( B ` L ) prefix Q ) ++ ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) <-> ( ( ( A ` K ) prefix Q ) = ( ( B ` L ) prefix Q ) /\ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) ) )
166 152 165 mpbid 
 |-  ( ph -> ( ( ( A ` K ) prefix Q ) = ( ( B ` L ) prefix Q ) /\ ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) )
167 166 simpld 
 |-  ( ph -> ( ( A ` K ) prefix Q ) = ( ( B ` L ) prefix Q ) )
168 167 oveq1d 
 |-  ( ph -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )
169 ccatrid 
 |-  ( ( ( A ` K ) prefix Q ) e. Word ( I X. 2o ) -> ( ( ( A ` K ) prefix Q ) ++ (/) ) = ( ( A ` K ) prefix Q ) )
170 102 169 syl 
 |-  ( ph -> ( ( ( A ` K ) prefix Q ) ++ (/) ) = ( ( A ` K ) prefix Q ) )
171 170 oveq1d 
 |-  ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ (/) ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )
172 168 171 23 3eqtr4rd 
 |-  ( ph -> ( S ` C ) = ( ( ( ( A ` K ) prefix Q ) ++ (/) ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )
173 162 eqcomd 
 |-  ( ph -> Q = ( # ` ( ( A ` K ) prefix Q ) ) )
174 hash0 
 |-  ( # ` (/) ) = 0
175 174 oveq2i 
 |-  ( Q + ( # ` (/) ) ) = ( Q + 0 )
176 68 addid1d 
 |-  ( ph -> ( Q + 0 ) = Q )
177 175 176 syl5req 
 |-  ( ph -> Q = ( Q + ( # ` (/) ) ) )
178 102 104 43 108 172 173 177 splval2 
 |-  ( ph -> ( ( S ` C ) splice <. Q , Q , <" V ( M ` V ) "> >. ) = ( ( ( ( A ` K ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )
179 elfzuzb 
 |-  ( Q e. ( 0 ... ( Q + 2 ) ) <-> ( Q e. ( ZZ>= ` 0 ) /\ ( Q + 2 ) e. ( ZZ>= ` Q ) ) )
180 31 113 179 sylanbrc 
 |-  ( ph -> Q e. ( 0 ... ( Q + 2 ) ) )
181 elfzuzb 
 |-  ( ( Q + 2 ) e. ( 0 ... P ) <-> ( ( Q + 2 ) e. ( ZZ>= ` 0 ) /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) )
182 50 21 181 sylanbrc 
 |-  ( ph -> ( Q + 2 ) e. ( 0 ... P ) )
183 ccatswrd 
 |-  ( ( ( A ` K ) e. Word ( I X. 2o ) /\ ( Q e. ( 0 ... ( Q + 2 ) ) /\ ( Q + 2 ) e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` ( A ` K ) ) ) ) ) -> ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) = ( ( A ` K ) substr <. Q , P >. ) )
184 41 180 182 14 183 syl13anc 
 |-  ( ph -> ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) = ( ( A ` K ) substr <. Q , P >. ) )
185 184 oveq1d 
 |-  ( ph -> ( ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) )
186 swrdcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) e. Word ( I X. 2o ) )
187 41 186 syl 
 |-  ( ph -> ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) e. Word ( I X. 2o ) )
188 swrdcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) e. Word ( I X. 2o ) )
189 41 188 syl 
 |-  ( ph -> ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) e. Word ( I X. 2o ) )
190 ccatass 
 |-  ( ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) e. Word ( I X. 2o ) /\ ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) e. Word ( I X. 2o ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) ) -> ( ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) )
191 187 189 145 190 syl3anc 
 |-  ( ph -> ( ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) )
192 166 simprd 
 |-  ( ph -> ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
193 185 191 192 3eqtr3d 
 |-  ( ph -> ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) = ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
194 ccatcl 
 |-  ( ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) e. Word ( I X. 2o ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) ) -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) e. Word ( I X. 2o ) )
195 189 145 194 syl2anc 
 |-  ( ph -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) e. Word ( I X. 2o ) )
196 swrdlen 
 |-  ( ( ( A ` K ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... ( Q + 2 ) ) /\ ( Q + 2 ) e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( # ` ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( ( Q + 2 ) - Q ) )
197 41 180 56 196 syl3anc 
 |-  ( ph -> ( # ` ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( ( Q + 2 ) - Q ) )
198 pncan2 
 |-  ( ( Q e. CC /\ 2 e. CC ) -> ( ( Q + 2 ) - Q ) = 2 )
199 68 75 198 sylancl 
 |-  ( ph -> ( ( Q + 2 ) - Q ) = 2 )
200 197 199 eqtrd 
 |-  ( ph -> ( # ` ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = 2 )
201 s2len 
 |-  ( # ` <" V ( M ` V ) "> ) = 2
202 200 201 eqtr4di 
 |-  ( ph -> ( # ` ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( # ` <" V ( M ` V ) "> ) )
203 ccatopth 
 |-  ( ( ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) e. Word ( I X. 2o ) /\ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) e. Word ( I X. 2o ) ) /\ ( <" V ( M ` V ) "> e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) /\ ( # ` ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( # ` <" V ( M ` V ) "> ) ) -> ( ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) = ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) <-> ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) = <" V ( M ` V ) "> /\ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) )
204 187 195 108 149 202 203 syl221anc 
 |-  ( ph -> ( ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) ) = ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) <-> ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) = <" V ( M ` V ) "> /\ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) )
205 193 204 mpbid 
 |-  ( ph -> ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) = <" V ( M ` V ) "> /\ ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
206 205 simpld 
 |-  ( ph -> ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) = <" V ( M ` V ) "> )
207 206 oveq2d 
 |-  ( ph -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( ( ( A ` K ) prefix Q ) ++ <" V ( M ` V ) "> ) )
208 ccatpfx 
 |-  ( ( ( A ` K ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... ( Q + 2 ) ) /\ ( Q + 2 ) e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( ( A ` K ) prefix ( Q + 2 ) ) )
209 41 180 56 208 syl3anc 
 |-  ( ph -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( ( A ` K ) prefix ( Q + 2 ) ) )
210 207 209 eqtr3d 
 |-  ( ph -> ( ( ( A ` K ) prefix Q ) ++ <" V ( M ` V ) "> ) = ( ( A ` K ) prefix ( Q + 2 ) ) )
211 210 oveq1d 
 |-  ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( ( A ` K ) prefix ( Q + 2 ) ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )
212 ccatpfx 
 |-  ( ( ( A ` K ) e. Word ( I X. 2o ) /\ ( Q + 2 ) e. ( 0 ... ( # ` ( A ` K ) ) ) /\ ( # ` ( A ` K ) ) e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( ( ( A ` K ) prefix ( Q + 2 ) ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( A ` K ) prefix ( # ` ( A ` K ) ) ) )
213 41 56 62 212 syl3anc 
 |-  ( ph -> ( ( ( A ` K ) prefix ( Q + 2 ) ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( A ` K ) prefix ( # ` ( A ` K ) ) ) )
214 pfxid 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) prefix ( # ` ( A ` K ) ) ) = ( A ` K ) )
215 41 214 syl 
 |-  ( ph -> ( ( A ` K ) prefix ( # ` ( A ` K ) ) ) = ( A ` K ) )
216 211 213 215 3eqtrd 
 |-  ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( A ` K ) )
217 100 178 216 3eqtrd 
 |-  ( ph -> ( Q ( T ` ( S ` C ) ) V ) = ( A ` K ) )
218 1 2 3 4 efgtf 
 |-  ( ( S ` C ) e. W -> ( ( T ` ( S ` C ) ) = ( a e. ( 0 ... ( # ` ( S ` C ) ) ) , i e. ( I X. 2o ) |-> ( ( S ` C ) splice <. a , a , <" i ( M ` i ) "> >. ) ) /\ ( T ` ( S ` C ) ) : ( ( 0 ... ( # ` ( S ` C ) ) ) X. ( I X. 2o ) ) --> W ) )
219 29 218 syl 
 |-  ( ph -> ( ( T ` ( S ` C ) ) = ( a e. ( 0 ... ( # ` ( S ` C ) ) ) , i e. ( I X. 2o ) |-> ( ( S ` C ) splice <. a , a , <" i ( M ` i ) "> >. ) ) /\ ( T ` ( S ` C ) ) : ( ( 0 ... ( # ` ( S ` C ) ) ) X. ( I X. 2o ) ) --> W ) )
220 219 simprd 
 |-  ( ph -> ( T ` ( S ` C ) ) : ( ( 0 ... ( # ` ( S ` C ) ) ) X. ( I X. 2o ) ) --> W )
221 220 ffnd 
 |-  ( ph -> ( T ` ( S ` C ) ) Fn ( ( 0 ... ( # ` ( S ` C ) ) ) X. ( I X. 2o ) ) )
222 fnovrn 
 |-  ( ( ( T ` ( S ` C ) ) Fn ( ( 0 ... ( # ` ( S ` C ) ) ) X. ( I X. 2o ) ) /\ Q e. ( 0 ... ( # ` ( S ` C ) ) ) /\ V e. ( I X. 2o ) ) -> ( Q ( T ` ( S ` C ) ) V ) e. ran ( T ` ( S ` C ) ) )
223 221 98 17 222 syl3anc 
 |-  ( ph -> ( Q ( T ` ( S ` C ) ) V ) e. ran ( T ` ( S ` C ) ) )
224 217 223 eqeltrrd 
 |-  ( ph -> ( A ` K ) e. ran ( T ` ( S ` C ) ) )
225 uztrn 
 |-  ( ( ( P - 2 ) e. ( ZZ>= ` Q ) /\ Q e. ( ZZ>= ` 0 ) ) -> ( P - 2 ) e. ( ZZ>= ` 0 ) )
226 94 31 225 syl2anc 
 |-  ( ph -> ( P - 2 ) e. ( ZZ>= ` 0 ) )
227 elfzuzb 
 |-  ( ( P - 2 ) e. ( 0 ... ( # ` ( S ` C ) ) ) <-> ( ( P - 2 ) e. ( ZZ>= ` 0 ) /\ ( # ` ( S ` C ) ) e. ( ZZ>= ` ( P - 2 ) ) ) )
228 226 92 227 sylanbrc 
 |-  ( ph -> ( P - 2 ) e. ( 0 ... ( # ` ( S ` C ) ) ) )
229 1 2 3 4 efgtval 
 |-  ( ( ( S ` C ) e. W /\ ( P - 2 ) e. ( 0 ... ( # ` ( S ` C ) ) ) /\ U e. ( I X. 2o ) ) -> ( ( P - 2 ) ( T ` ( S ` C ) ) U ) = ( ( S ` C ) splice <. ( P - 2 ) , ( P - 2 ) , <" U ( M ` U ) "> >. ) )
230 29 228 16 229 syl3anc 
 |-  ( ph -> ( ( P - 2 ) ( T ` ( S ` C ) ) U ) = ( ( S ` C ) splice <. ( P - 2 ) , ( P - 2 ) , <" U ( M ` U ) "> >. ) )
231 pfxcl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) prefix ( P - 2 ) ) e. Word ( I X. 2o ) )
232 37 231 syl 
 |-  ( ph -> ( ( B ` L ) prefix ( P - 2 ) ) e. Word ( I X. 2o ) )
233 swrdcl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
234 37 233 syl 
 |-  ( ph -> ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
235 ccatswrd 
 |-  ( ( ( A ` K ) e. Word ( I X. 2o ) /\ ( ( Q + 2 ) e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` ( A ` K ) ) ) /\ ( # ` ( A ` K ) ) e. ( 0 ... ( # ` ( A ` K ) ) ) ) ) -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) )
236 41 182 14 62 235 syl13anc 
 |-  ( ph -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) )
237 205 simprd 
 |-  ( ph -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) )
238 elfzuzb 
 |-  ( Q e. ( 0 ... ( P - 2 ) ) <-> ( Q e. ( ZZ>= ` 0 ) /\ ( P - 2 ) e. ( ZZ>= ` Q ) ) )
239 31 94 238 sylanbrc 
 |-  ( ph -> Q e. ( 0 ... ( P - 2 ) ) )
240 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 efgredlemg 
 |-  ( ph -> ( # ` ( A ` K ) ) = ( # ` ( B ` L ) ) )
241 240 52 eqeltrrd 
 |-  ( ph -> ( # ` ( B ` L ) ) e. ( ZZ>= ` P ) )
242 0le2 
 |-  0 <_ 2
243 242 a1i 
 |-  ( ph -> 0 <_ 2 )
244 81 zred 
 |-  ( ph -> P e. RR )
245 2re 
 |-  2 e. RR
246 subge02 
 |-  ( ( P e. RR /\ 2 e. RR ) -> ( 0 <_ 2 <-> ( P - 2 ) <_ P ) )
247 244 245 246 sylancl 
 |-  ( ph -> ( 0 <_ 2 <-> ( P - 2 ) <_ P ) )
248 243 247 mpbid 
 |-  ( ph -> ( P - 2 ) <_ P )
249 eluz2 
 |-  ( P e. ( ZZ>= ` ( P - 2 ) ) <-> ( ( P - 2 ) e. ZZ /\ P e. ZZ /\ ( P - 2 ) <_ P ) )
250 83 81 248 249 syl3anbrc 
 |-  ( ph -> P e. ( ZZ>= ` ( P - 2 ) ) )
251 uztrn 
 |-  ( ( ( # ` ( B ` L ) ) e. ( ZZ>= ` P ) /\ P e. ( ZZ>= ` ( P - 2 ) ) ) -> ( # ` ( B ` L ) ) e. ( ZZ>= ` ( P - 2 ) ) )
252 241 250 251 syl2anc 
 |-  ( ph -> ( # ` ( B ` L ) ) e. ( ZZ>= ` ( P - 2 ) ) )
253 elfzuzb 
 |-  ( ( P - 2 ) e. ( 0 ... ( # ` ( B ` L ) ) ) <-> ( ( P - 2 ) e. ( ZZ>= ` 0 ) /\ ( # ` ( B ` L ) ) e. ( ZZ>= ` ( P - 2 ) ) ) )
254 226 252 253 sylanbrc 
 |-  ( ph -> ( P - 2 ) e. ( 0 ... ( # ` ( B ` L ) ) ) )
255 lencl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( # ` ( B ` L ) ) e. NN0 )
256 37 255 syl 
 |-  ( ph -> ( # ` ( B ` L ) ) e. NN0 )
257 256 59 eleqtrdi 
 |-  ( ph -> ( # ` ( B ` L ) ) e. ( ZZ>= ` 0 ) )
258 eluzfz2 
 |-  ( ( # ` ( B ` L ) ) e. ( ZZ>= ` 0 ) -> ( # ` ( B ` L ) ) e. ( 0 ... ( # ` ( B ` L ) ) ) )
259 257 258 syl 
 |-  ( ph -> ( # ` ( B ` L ) ) e. ( 0 ... ( # ` ( B ` L ) ) ) )
260 ccatswrd 
 |-  ( ( ( B ` L ) e. Word ( I X. 2o ) /\ ( Q e. ( 0 ... ( P - 2 ) ) /\ ( P - 2 ) e. ( 0 ... ( # ` ( B ` L ) ) ) /\ ( # ` ( B ` L ) ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) ) -> ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) )
261 37 239 254 259 260 syl13anc 
 |-  ( ph -> ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) )
262 237 261 eqtr4d 
 |-  ( ph -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) )
263 swrdcl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) e. Word ( I X. 2o ) )
264 37 263 syl 
 |-  ( ph -> ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) e. Word ( I X. 2o ) )
265 swrdcl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
266 37 265 syl 
 |-  ( ph -> ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
267 swrdlen 
 |-  ( ( ( A ` K ) e. Word ( I X. 2o ) /\ ( Q + 2 ) e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) = ( P - ( Q + 2 ) ) )
268 41 182 14 267 syl3anc 
 |-  ( ph -> ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) = ( P - ( Q + 2 ) ) )
269 swrdlen 
 |-  ( ( ( B ` L ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... ( P - 2 ) ) /\ ( P - 2 ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( # ` ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) = ( ( P - 2 ) - Q ) )
270 37 239 254 269 syl3anc 
 |-  ( ph -> ( # ` ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) = ( ( P - 2 ) - Q ) )
271 85 68 76 sub32d 
 |-  ( ph -> ( ( P - Q ) - 2 ) = ( ( P - 2 ) - Q ) )
272 85 68 76 subsub4d 
 |-  ( ph -> ( ( P - Q ) - 2 ) = ( P - ( Q + 2 ) ) )
273 270 271 272 3eqtr2d 
 |-  ( ph -> ( # ` ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) = ( P - ( Q + 2 ) ) )
274 268 273 eqtr4d 
 |-  ( ph -> ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) = ( # ` ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) )
275 ccatopth 
 |-  ( ( ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) e. Word ( I X. 2o ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) ) /\ ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) /\ ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) = ( # ` ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) ) -> ( ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) <-> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) = ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) ) )
276 189 145 264 266 274 275 syl221anc 
 |-  ( ph -> ( ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) <-> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) = ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) ) )
277 262 276 mpbid 
 |-  ( ph -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) = ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) /\ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) )
278 277 simpld 
 |-  ( ph -> ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) = ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) )
279 277 simprd 
 |-  ( ph -> ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) )
280 elfzuzb 
 |-  ( ( P - 2 ) e. ( 0 ... P ) <-> ( ( P - 2 ) e. ( ZZ>= ` 0 ) /\ P e. ( ZZ>= ` ( P - 2 ) ) ) )
281 226 250 280 sylanbrc 
 |-  ( ph -> ( P - 2 ) e. ( 0 ... P ) )
282 elfzuz 
 |-  ( P e. ( 0 ... ( # ` ( A ` K ) ) ) -> P e. ( ZZ>= ` 0 ) )
283 14 282 syl 
 |-  ( ph -> P e. ( ZZ>= ` 0 ) )
284 elfzuzb 
 |-  ( P e. ( 0 ... ( # ` ( B ` L ) ) ) <-> ( P e. ( ZZ>= ` 0 ) /\ ( # ` ( B ` L ) ) e. ( ZZ>= ` P ) ) )
285 283 241 284 sylanbrc 
 |-  ( ph -> P e. ( 0 ... ( # ` ( B ` L ) ) ) )
286 ccatswrd 
 |-  ( ( ( B ` L ) e. Word ( I X. 2o ) /\ ( ( P - 2 ) e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` ( B ` L ) ) ) /\ ( # ` ( B ` L ) ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) ) -> ( ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) )
287 37 281 285 259 286 syl13anc 
 |-  ( ph -> ( ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) )
288 279 287 eqtr4d 
 |-  ( ph -> ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
289 swrdcl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. ( P - 2 ) , P >. ) e. Word ( I X. 2o ) )
290 37 289 syl 
 |-  ( ph -> ( ( B ` L ) substr <. ( P - 2 ) , P >. ) e. Word ( I X. 2o ) )
291 s2len 
 |-  ( # ` <" U ( M ` U ) "> ) = 2
292 swrdlen 
 |-  ( ( ( B ` L ) e. Word ( I X. 2o ) /\ ( P - 2 ) e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( # ` ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) = ( P - ( P - 2 ) ) )
293 37 281 285 292 syl3anc 
 |-  ( ph -> ( # ` ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) = ( P - ( P - 2 ) ) )
294 nncan 
 |-  ( ( P e. CC /\ 2 e. CC ) -> ( P - ( P - 2 ) ) = 2 )
295 85 75 294 sylancl 
 |-  ( ph -> ( P - ( P - 2 ) ) = 2 )
296 293 295 eqtr2d 
 |-  ( ph -> 2 = ( # ` ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) )
297 291 296 syl5eq 
 |-  ( ph -> ( # ` <" U ( M ` U ) "> ) = ( # ` ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) )
298 ccatopth 
 |-  ( ( ( <" U ( M ` U ) "> e. Word ( I X. 2o ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) ) /\ ( ( ( B ` L ) substr <. ( P - 2 ) , P >. ) e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) /\ ( # ` <" U ( M ` U ) "> ) = ( # ` ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) ) -> ( ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) <-> ( <" U ( M ` U ) "> = ( ( B ` L ) substr <. ( P - 2 ) , P >. ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) = ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) )
299 125 127 290 234 297 298 syl221anc 
 |-  ( ph -> ( ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) <-> ( <" U ( M ` U ) "> = ( ( B ` L ) substr <. ( P - 2 ) , P >. ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) = ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) )
300 288 299 mpbid 
 |-  ( ph -> ( <" U ( M ` U ) "> = ( ( B ` L ) substr <. ( P - 2 ) , P >. ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) = ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
301 300 simprd 
 |-  ( ph -> ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) = ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) )
302 278 301 oveq12d 
 |-  ( ph -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
303 236 302 eqtr3d 
 |-  ( ph -> ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) = ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
304 303 oveq2d 
 |-  ( ph -> ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) )
305 ccatass 
 |-  ( ( ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) -> ( ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) )
306 39 264 234 305 syl3anc 
 |-  ( ph -> ( ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) ) )
307 304 306 eqtr4d 
 |-  ( ph -> ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
308 ccatpfx 
 |-  ( ( ( B ` L ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... ( P - 2 ) ) /\ ( P - 2 ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) = ( ( B ` L ) prefix ( P - 2 ) ) )
309 37 239 254 308 syl3anc 
 |-  ( ph -> ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) = ( ( B ` L ) prefix ( P - 2 ) ) )
310 309 oveq1d 
 |-  ( ph -> ( ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
311 23 307 310 3eqtrd 
 |-  ( ph -> ( S ` C ) = ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
312 ccatrid 
 |-  ( ( ( B ` L ) prefix ( P - 2 ) ) e. Word ( I X. 2o ) -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ (/) ) = ( ( B ` L ) prefix ( P - 2 ) ) )
313 232 312 syl 
 |-  ( ph -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ (/) ) = ( ( B ` L ) prefix ( P - 2 ) ) )
314 313 oveq1d 
 |-  ( ph -> ( ( ( ( B ` L ) prefix ( P - 2 ) ) ++ (/) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
315 311 314 eqtr4d 
 |-  ( ph -> ( S ` C ) = ( ( ( ( B ` L ) prefix ( P - 2 ) ) ++ (/) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
316 pfxlen 
 |-  ( ( ( B ` L ) e. Word ( I X. 2o ) /\ ( P - 2 ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( # ` ( ( B ` L ) prefix ( P - 2 ) ) ) = ( P - 2 ) )
317 37 254 316 syl2anc 
 |-  ( ph -> ( # ` ( ( B ` L ) prefix ( P - 2 ) ) ) = ( P - 2 ) )
318 317 eqcomd 
 |-  ( ph -> ( P - 2 ) = ( # ` ( ( B ` L ) prefix ( P - 2 ) ) ) )
319 174 oveq2i 
 |-  ( ( P - 2 ) + ( # ` (/) ) ) = ( ( P - 2 ) + 0 )
320 83 zcnd 
 |-  ( ph -> ( P - 2 ) e. CC )
321 320 addid1d 
 |-  ( ph -> ( ( P - 2 ) + 0 ) = ( P - 2 ) )
322 319 321 syl5req 
 |-  ( ph -> ( P - 2 ) = ( ( P - 2 ) + ( # ` (/) ) ) )
323 232 104 234 125 315 318 322 splval2 
 |-  ( ph -> ( ( S ` C ) splice <. ( P - 2 ) , ( P - 2 ) , <" U ( M ` U ) "> >. ) = ( ( ( ( B ` L ) prefix ( P - 2 ) ) ++ <" U ( M ` U ) "> ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
324 300 simpld 
 |-  ( ph -> <" U ( M ` U ) "> = ( ( B ` L ) substr <. ( P - 2 ) , P >. ) )
325 324 oveq2d 
 |-  ( ph -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ <" U ( M ` U ) "> ) = ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) )
326 ccatpfx 
 |-  ( ( ( B ` L ) e. Word ( I X. 2o ) /\ ( P - 2 ) e. ( 0 ... P ) /\ P e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) = ( ( B ` L ) prefix P ) )
327 37 281 285 326 syl3anc 
 |-  ( ph -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) = ( ( B ` L ) prefix P ) )
328 325 327 eqtrd 
 |-  ( ph -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ <" U ( M ` U ) "> ) = ( ( B ` L ) prefix P ) )
329 328 oveq1d 
 |-  ( ph -> ( ( ( ( B ` L ) prefix ( P - 2 ) ) ++ <" U ( M ` U ) "> ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( ( B ` L ) prefix P ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
330 ccatpfx 
 |-  ( ( ( B ` L ) e. Word ( I X. 2o ) /\ P e. ( 0 ... ( # ` ( B ` L ) ) ) /\ ( # ` ( B ` L ) ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( ( ( B ` L ) prefix P ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) prefix ( # ` ( B ` L ) ) ) )
331 37 285 259 330 syl3anc 
 |-  ( ph -> ( ( ( B ` L ) prefix P ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) prefix ( # ` ( B ` L ) ) ) )
332 pfxid 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) prefix ( # ` ( B ` L ) ) ) = ( B ` L ) )
333 37 332 syl 
 |-  ( ph -> ( ( B ` L ) prefix ( # ` ( B ` L ) ) ) = ( B ` L ) )
334 329 331 333 3eqtrd 
 |-  ( ph -> ( ( ( ( B ` L ) prefix ( P - 2 ) ) ++ <" U ( M ` U ) "> ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( B ` L ) )
335 230 323 334 3eqtrd 
 |-  ( ph -> ( ( P - 2 ) ( T ` ( S ` C ) ) U ) = ( B ` L ) )
336 fnovrn 
 |-  ( ( ( T ` ( S ` C ) ) Fn ( ( 0 ... ( # ` ( S ` C ) ) ) X. ( I X. 2o ) ) /\ ( P - 2 ) e. ( 0 ... ( # ` ( S ` C ) ) ) /\ U e. ( I X. 2o ) ) -> ( ( P - 2 ) ( T ` ( S ` C ) ) U ) e. ran ( T ` ( S ` C ) ) )
337 221 228 16 336 syl3anc 
 |-  ( ph -> ( ( P - 2 ) ( T ` ( S ` C ) ) U ) e. ran ( T ` ( S ` C ) ) )
338 335 337 eqeltrrd 
 |-  ( ph -> ( B ` L ) e. ran ( T ` ( S ` C ) ) )
339 224 338 jca 
 |-  ( ph -> ( ( A ` K ) e. ran ( T ` ( S ` C ) ) /\ ( B ` L ) e. ran ( T ` ( S ` C ) ) ) )