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 ffvelcdmi 
 |-  ( 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 sselid 
 |-  ( 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 sselid 
 |-  ( 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 15 elfzelzd 
 |-  ( ph -> Q e. ZZ )
67 66 zcnd 
 |-  ( ph -> Q e. CC )
68 58 nn0cnd 
 |-  ( ph -> ( # ` ( A ` K ) ) e. CC )
69 2z 
 |-  2 e. ZZ
70 zaddcl 
 |-  ( ( Q e. ZZ /\ 2 e. ZZ ) -> ( Q + 2 ) e. ZZ )
71 66 69 70 sylancl 
 |-  ( ph -> ( Q + 2 ) e. ZZ )
72 71 zcnd 
 |-  ( ph -> ( Q + 2 ) e. CC )
73 67 68 72 addsubassd 
 |-  ( ph -> ( ( Q + ( # ` ( A ` K ) ) ) - ( Q + 2 ) ) = ( Q + ( ( # ` ( A ` K ) ) - ( Q + 2 ) ) ) )
74 2cn 
 |-  2 e. CC
75 74 a1i 
 |-  ( ph -> 2 e. CC )
76 67 68 75 pnpcand 
 |-  ( ph -> ( ( Q + ( # ` ( A ` K ) ) ) - ( Q + 2 ) ) = ( ( # ` ( A ` K ) ) - 2 ) )
77 65 73 76 3eqtr2d 
 |-  ( ph -> ( ( # ` ( ( B ` L ) prefix Q ) ) + ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) ) = ( ( # ` ( A ` K ) ) - 2 ) )
78 32 45 77 3eqtrd 
 |-  ( ph -> ( # ` ( S ` C ) ) = ( ( # ` ( A ` K ) ) - 2 ) )
79 14 elfzelzd 
 |-  ( ph -> P e. ZZ )
80 zsubcl 
 |-  ( ( P e. ZZ /\ 2 e. ZZ ) -> ( P - 2 ) e. ZZ )
81 79 69 80 sylancl 
 |-  ( ph -> ( P - 2 ) e. ZZ )
82 69 a1i 
 |-  ( ph -> 2 e. ZZ )
83 79 zcnd 
 |-  ( ph -> P e. CC )
84 npcan 
 |-  ( ( P e. CC /\ 2 e. CC ) -> ( ( P - 2 ) + 2 ) = P )
85 83 74 84 sylancl 
 |-  ( ph -> ( ( P - 2 ) + 2 ) = P )
86 85 fveq2d 
 |-  ( ph -> ( ZZ>= ` ( ( P - 2 ) + 2 ) ) = ( ZZ>= ` P ) )
87 52 86 eleqtrrd 
 |-  ( ph -> ( # ` ( A ` K ) ) e. ( ZZ>= ` ( ( P - 2 ) + 2 ) ) )
88 eluzsub 
 |-  ( ( ( P - 2 ) e. ZZ /\ 2 e. ZZ /\ ( # ` ( A ` K ) ) e. ( ZZ>= ` ( ( P - 2 ) + 2 ) ) ) -> ( ( # ` ( A ` K ) ) - 2 ) e. ( ZZ>= ` ( P - 2 ) ) )
89 81 82 87 88 syl3anc 
 |-  ( ph -> ( ( # ` ( A ` K ) ) - 2 ) e. ( ZZ>= ` ( P - 2 ) ) )
90 78 89 eqeltrd 
 |-  ( ph -> ( # ` ( S ` C ) ) e. ( ZZ>= ` ( P - 2 ) ) )
91 eluzsub 
 |-  ( ( Q e. ZZ /\ 2 e. ZZ /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) -> ( P - 2 ) e. ( ZZ>= ` Q ) )
92 66 82 21 91 syl3anc 
 |-  ( ph -> ( P - 2 ) e. ( ZZ>= ` Q ) )
93 uztrn 
 |-  ( ( ( # ` ( S ` C ) ) e. ( ZZ>= ` ( P - 2 ) ) /\ ( P - 2 ) e. ( ZZ>= ` Q ) ) -> ( # ` ( S ` C ) ) e. ( ZZ>= ` Q ) )
94 90 92 93 syl2anc 
 |-  ( ph -> ( # ` ( S ` C ) ) e. ( ZZ>= ` Q ) )
95 elfzuzb 
 |-  ( Q e. ( 0 ... ( # ` ( S ` C ) ) ) <-> ( Q e. ( ZZ>= ` 0 ) /\ ( # ` ( S ` C ) ) e. ( ZZ>= ` Q ) ) )
96 31 94 95 sylanbrc 
 |-  ( ph -> Q e. ( 0 ... ( # ` ( S ` C ) ) ) )
97 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 ) "> >. ) )
98 29 96 17 97 syl3anc 
 |-  ( ph -> ( Q ( T ` ( S ` C ) ) V ) = ( ( S ` C ) splice <. Q , Q , <" V ( M ` V ) "> >. ) )
99 pfxcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) prefix Q ) e. Word ( I X. 2o ) )
100 41 99 syl 
 |-  ( ph -> ( ( A ` K ) prefix Q ) e. Word ( I X. 2o ) )
101 wrd0 
 |-  (/) e. Word ( I X. 2o )
102 101 a1i 
 |-  ( ph -> (/) e. Word ( I X. 2o ) )
103 3 efgmf 
 |-  M : ( I X. 2o ) --> ( I X. 2o )
104 103 ffvelcdmi 
 |-  ( V e. ( I X. 2o ) -> ( M ` V ) e. ( I X. 2o ) )
105 17 104 syl 
 |-  ( ph -> ( M ` V ) e. ( I X. 2o ) )
106 17 105 s2cld 
 |-  ( ph -> <" V ( M ` V ) "> e. Word ( I X. 2o ) )
107 66 zred 
 |-  ( ph -> Q e. RR )
108 nn0addge1 
 |-  ( ( Q e. RR /\ 2 e. NN0 ) -> Q <_ ( Q + 2 ) )
109 107 48 108 sylancl 
 |-  ( ph -> Q <_ ( Q + 2 ) )
110 eluz2 
 |-  ( ( Q + 2 ) e. ( ZZ>= ` Q ) <-> ( Q e. ZZ /\ ( Q + 2 ) e. ZZ /\ Q <_ ( Q + 2 ) ) )
111 66 71 109 110 syl3anbrc 
 |-  ( ph -> ( Q + 2 ) e. ( ZZ>= ` Q ) )
112 uztrn 
 |-  ( ( P e. ( ZZ>= ` ( Q + 2 ) ) /\ ( Q + 2 ) e. ( ZZ>= ` Q ) ) -> P e. ( ZZ>= ` Q ) )
113 21 111 112 syl2anc 
 |-  ( ph -> P e. ( ZZ>= ` Q ) )
114 elfzuzb 
 |-  ( Q e. ( 0 ... P ) <-> ( Q e. ( ZZ>= ` 0 ) /\ P e. ( ZZ>= ` Q ) ) )
115 31 113 114 sylanbrc 
 |-  ( ph -> Q e. ( 0 ... P ) )
116 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 ) )
117 41 115 14 116 syl3anc 
 |-  ( ph -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , P >. ) ) = ( ( A ` K ) prefix P ) )
118 117 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 ) ) >. ) ) ) )
119 pfxcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) )
120 41 119 syl 
 |-  ( ph -> ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) )
121 103 ffvelcdmi 
 |-  ( U e. ( I X. 2o ) -> ( M ` U ) e. ( I X. 2o ) )
122 16 121 syl 
 |-  ( ph -> ( M ` U ) e. ( I X. 2o ) )
123 16 122 s2cld 
 |-  ( ph -> <" U ( M ` U ) "> e. Word ( I X. 2o ) )
124 swrdcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) )
125 41 124 syl 
 |-  ( ph -> ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) )
126 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 ) ) >. ) ) ) )
127 120 123 125 126 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 ) ) >. ) ) ) )
128 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 ) "> >. ) )
129 40 14 16 128 syl3anc 
 |-  ( ph -> ( P ( T ` ( A ` K ) ) U ) = ( ( A ` K ) splice <. P , P , <" U ( M ` U ) "> >. ) )
130 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 ) ) >. ) ) )
131 40 14 14 123 130 syl13anc 
 |-  ( ph -> ( ( A ` K ) splice <. P , P , <" U ( M ` U ) "> >. ) = ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) )
132 18 129 131 3eqtrd 
 |-  ( ph -> ( S ` A ) = ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) )
133 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 ) "> >. ) )
134 36 15 17 133 syl3anc 
 |-  ( ph -> ( Q ( T ` ( B ` L ) ) V ) = ( ( B ` L ) splice <. Q , Q , <" V ( M ` V ) "> >. ) )
135 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 ) ) >. ) ) )
136 36 15 15 106 135 syl13anc 
 |-  ( ph -> ( ( B ` L ) splice <. Q , Q , <" V ( M ` V ) "> >. ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
137 19 134 136 3eqtrd 
 |-  ( ph -> ( S ` B ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
138 10 132 137 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 ) ) >. ) ) )
139 118 127 138 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 ) ) >. ) ) )
140 swrdcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. Q , P >. ) e. Word ( I X. 2o ) )
141 41 140 syl 
 |-  ( ph -> ( ( A ` K ) substr <. Q , P >. ) e. Word ( I X. 2o ) )
142 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 ) )
143 123 125 142 syl2anc 
 |-  ( ph -> ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) )
144 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 ) ) >. ) ) ) ) )
145 100 141 143 144 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 ) ) >. ) ) ) ) )
146 swrdcl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
147 37 146 syl 
 |-  ( ph -> ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
148 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 ) ) >. ) ) ) )
149 39 106 147 148 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 ) ) >. ) ) ) )
150 139 145 149 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 ) ) >. ) ) ) )
151 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 ) )
152 141 143 151 syl2anc 
 |-  ( ph -> ( ( ( A ` K ) substr <. Q , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) e. Word ( I X. 2o ) )
153 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 ) )
154 106 147 153 syl2anc 
 |-  ( ph -> ( <" V ( M ` V ) "> ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) e. Word ( I X. 2o ) )
155 uztrn 
 |-  ( ( ( # ` ( A ` K ) ) e. ( ZZ>= ` P ) /\ P e. ( ZZ>= ` Q ) ) -> ( # ` ( A ` K ) ) e. ( ZZ>= ` Q ) )
156 52 113 155 syl2anc 
 |-  ( ph -> ( # ` ( A ` K ) ) e. ( ZZ>= ` Q ) )
157 elfzuzb 
 |-  ( Q e. ( 0 ... ( # ` ( A ` K ) ) ) <-> ( Q e. ( ZZ>= ` 0 ) /\ ( # ` ( A ` K ) ) e. ( ZZ>= ` Q ) ) )
158 31 156 157 sylanbrc 
 |-  ( ph -> Q e. ( 0 ... ( # ` ( A ` K ) ) ) )
159 pfxlen 
 |-  ( ( ( A ` K ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( # ` ( ( A ` K ) prefix Q ) ) = Q )
160 41 158 159 syl2anc 
 |-  ( ph -> ( # ` ( ( A ` K ) prefix Q ) ) = Q )
161 160 47 eqtr4d 
 |-  ( ph -> ( # ` ( ( A ` K ) prefix Q ) ) = ( # ` ( ( B ` L ) prefix Q ) ) )
162 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 ) ) >. ) ) ) ) )
163 100 152 39 154 161 162 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 ) ) >. ) ) ) ) )
164 150 163 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 ) ) >. ) ) ) )
165 164 simpld 
 |-  ( ph -> ( ( A ` K ) prefix Q ) = ( ( B ` L ) prefix Q ) )
166 165 oveq1d 
 |-  ( ph -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )
167 ccatrid 
 |-  ( ( ( A ` K ) prefix Q ) e. Word ( I X. 2o ) -> ( ( ( A ` K ) prefix Q ) ++ (/) ) = ( ( A ` K ) prefix Q ) )
168 100 167 syl 
 |-  ( ph -> ( ( ( A ` K ) prefix Q ) ++ (/) ) = ( ( A ` K ) prefix Q ) )
169 168 oveq1d 
 |-  ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ (/) ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )
170 166 169 23 3eqtr4rd 
 |-  ( ph -> ( S ` C ) = ( ( ( ( A ` K ) prefix Q ) ++ (/) ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )
171 160 eqcomd 
 |-  ( ph -> Q = ( # ` ( ( A ` K ) prefix Q ) ) )
172 hash0 
 |-  ( # ` (/) ) = 0
173 172 oveq2i 
 |-  ( Q + ( # ` (/) ) ) = ( Q + 0 )
174 67 addridd 
 |-  ( ph -> ( Q + 0 ) = Q )
175 173 174 eqtr2id 
 |-  ( ph -> Q = ( Q + ( # ` (/) ) ) )
176 100 102 43 106 170 171 175 splval2 
 |-  ( ph -> ( ( S ` C ) splice <. Q , Q , <" V ( M ` V ) "> >. ) = ( ( ( ( A ` K ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )
177 elfzuzb 
 |-  ( Q e. ( 0 ... ( Q + 2 ) ) <-> ( Q e. ( ZZ>= ` 0 ) /\ ( Q + 2 ) e. ( ZZ>= ` Q ) ) )
178 31 111 177 sylanbrc 
 |-  ( ph -> Q e. ( 0 ... ( Q + 2 ) ) )
179 elfzuzb 
 |-  ( ( Q + 2 ) e. ( 0 ... P ) <-> ( ( Q + 2 ) e. ( ZZ>= ` 0 ) /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) )
180 50 21 179 sylanbrc 
 |-  ( ph -> ( Q + 2 ) e. ( 0 ... P ) )
181 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 >. ) )
182 41 178 180 14 181 syl13anc 
 |-  ( ph -> ( ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) = ( ( A ` K ) substr <. Q , P >. ) )
183 182 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 ) ) >. ) ) ) )
184 swrdcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) e. Word ( I X. 2o ) )
185 41 184 syl 
 |-  ( ph -> ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) e. Word ( I X. 2o ) )
186 swrdcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) e. Word ( I X. 2o ) )
187 41 186 syl 
 |-  ( ph -> ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) e. Word ( I X. 2o ) )
188 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 ) ) >. ) ) ) ) )
189 185 187 143 188 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 ) ) >. ) ) ) ) )
190 164 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 ) ) >. ) ) )
191 183 189 190 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 ) ) >. ) ) )
192 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 ) )
193 187 143 192 syl2anc 
 |-  ( ph -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) e. Word ( I X. 2o ) )
194 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 ) )
195 41 178 56 194 syl3anc 
 |-  ( ph -> ( # ` ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( ( Q + 2 ) - Q ) )
196 pncan2 
 |-  ( ( Q e. CC /\ 2 e. CC ) -> ( ( Q + 2 ) - Q ) = 2 )
197 67 74 196 sylancl 
 |-  ( ph -> ( ( Q + 2 ) - Q ) = 2 )
198 195 197 eqtrd 
 |-  ( ph -> ( # ` ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = 2 )
199 s2len 
 |-  ( # ` <" V ( M ` V ) "> ) = 2
200 198 199 eqtr4di 
 |-  ( ph -> ( # ` ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( # ` <" V ( M ` V ) "> ) )
201 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 ) ) >. ) ) ) )
202 185 193 106 147 200 201 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 ) ) >. ) ) ) )
203 191 202 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 ) ) >. ) ) )
204 203 simpld 
 |-  ( ph -> ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) = <" V ( M ` V ) "> )
205 204 oveq2d 
 |-  ( ph -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( ( ( A ` K ) prefix Q ) ++ <" V ( M ` V ) "> ) )
206 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 ) ) )
207 41 178 56 206 syl3anc 
 |-  ( ph -> ( ( ( A ` K ) prefix Q ) ++ ( ( A ` K ) substr <. Q , ( Q + 2 ) >. ) ) = ( ( A ` K ) prefix ( Q + 2 ) ) )
208 205 207 eqtr3d 
 |-  ( ph -> ( ( ( A ` K ) prefix Q ) ++ <" V ( M ` V ) "> ) = ( ( A ` K ) prefix ( Q + 2 ) ) )
209 208 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 ) ) >. ) ) )
210 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 ) ) ) )
211 41 56 62 210 syl3anc 
 |-  ( ph -> ( ( ( A ` K ) prefix ( Q + 2 ) ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( ( A ` K ) prefix ( # ` ( A ` K ) ) ) )
212 pfxid 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) prefix ( # ` ( A ` K ) ) ) = ( A ` K ) )
213 41 212 syl 
 |-  ( ph -> ( ( A ` K ) prefix ( # ` ( A ` K ) ) ) = ( A ` K ) )
214 209 211 213 3eqtrd 
 |-  ( ph -> ( ( ( ( A ` K ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( A ` K ) )
215 98 176 214 3eqtrd 
 |-  ( ph -> ( Q ( T ` ( S ` C ) ) V ) = ( A ` K ) )
216 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 ) )
217 29 216 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 ) )
218 217 simprd 
 |-  ( ph -> ( T ` ( S ` C ) ) : ( ( 0 ... ( # ` ( S ` C ) ) ) X. ( I X. 2o ) ) --> W )
219 218 ffnd 
 |-  ( ph -> ( T ` ( S ` C ) ) Fn ( ( 0 ... ( # ` ( S ` C ) ) ) X. ( I X. 2o ) ) )
220 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 ) ) )
221 219 96 17 220 syl3anc 
 |-  ( ph -> ( Q ( T ` ( S ` C ) ) V ) e. ran ( T ` ( S ` C ) ) )
222 215 221 eqeltrrd 
 |-  ( ph -> ( A ` K ) e. ran ( T ` ( S ` C ) ) )
223 uztrn 
 |-  ( ( ( P - 2 ) e. ( ZZ>= ` Q ) /\ Q e. ( ZZ>= ` 0 ) ) -> ( P - 2 ) e. ( ZZ>= ` 0 ) )
224 92 31 223 syl2anc 
 |-  ( ph -> ( P - 2 ) e. ( ZZ>= ` 0 ) )
225 elfzuzb 
 |-  ( ( P - 2 ) e. ( 0 ... ( # ` ( S ` C ) ) ) <-> ( ( P - 2 ) e. ( ZZ>= ` 0 ) /\ ( # ` ( S ` C ) ) e. ( ZZ>= ` ( P - 2 ) ) ) )
226 224 90 225 sylanbrc 
 |-  ( ph -> ( P - 2 ) e. ( 0 ... ( # ` ( S ` C ) ) ) )
227 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 ) "> >. ) )
228 29 226 16 227 syl3anc 
 |-  ( ph -> ( ( P - 2 ) ( T ` ( S ` C ) ) U ) = ( ( S ` C ) splice <. ( P - 2 ) , ( P - 2 ) , <" U ( M ` U ) "> >. ) )
229 pfxcl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) prefix ( P - 2 ) ) e. Word ( I X. 2o ) )
230 37 229 syl 
 |-  ( ph -> ( ( B ` L ) prefix ( P - 2 ) ) e. Word ( I X. 2o ) )
231 swrdcl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
232 37 231 syl 
 |-  ( ph -> ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
233 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 ) ) >. ) )
234 41 180 14 62 233 syl13anc 
 |-  ( ph -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) )
235 203 simprd 
 |-  ( ph -> ( ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ++ ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) )
236 elfzuzb 
 |-  ( Q e. ( 0 ... ( P - 2 ) ) <-> ( Q e. ( ZZ>= ` 0 ) /\ ( P - 2 ) e. ( ZZ>= ` Q ) ) )
237 31 92 236 sylanbrc 
 |-  ( ph -> Q e. ( 0 ... ( P - 2 ) ) )
238 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 ) ) )
239 238 52 eqeltrrd 
 |-  ( ph -> ( # ` ( B ` L ) ) e. ( ZZ>= ` P ) )
240 0le2 
 |-  0 <_ 2
241 240 a1i 
 |-  ( ph -> 0 <_ 2 )
242 79 zred 
 |-  ( ph -> P e. RR )
243 2re 
 |-  2 e. RR
244 subge02 
 |-  ( ( P e. RR /\ 2 e. RR ) -> ( 0 <_ 2 <-> ( P - 2 ) <_ P ) )
245 242 243 244 sylancl 
 |-  ( ph -> ( 0 <_ 2 <-> ( P - 2 ) <_ P ) )
246 241 245 mpbid 
 |-  ( ph -> ( P - 2 ) <_ P )
247 eluz2 
 |-  ( P e. ( ZZ>= ` ( P - 2 ) ) <-> ( ( P - 2 ) e. ZZ /\ P e. ZZ /\ ( P - 2 ) <_ P ) )
248 81 79 246 247 syl3anbrc 
 |-  ( ph -> P e. ( ZZ>= ` ( P - 2 ) ) )
249 uztrn 
 |-  ( ( ( # ` ( B ` L ) ) e. ( ZZ>= ` P ) /\ P e. ( ZZ>= ` ( P - 2 ) ) ) -> ( # ` ( B ` L ) ) e. ( ZZ>= ` ( P - 2 ) ) )
250 239 248 249 syl2anc 
 |-  ( ph -> ( # ` ( B ` L ) ) e. ( ZZ>= ` ( P - 2 ) ) )
251 elfzuzb 
 |-  ( ( P - 2 ) e. ( 0 ... ( # ` ( B ` L ) ) ) <-> ( ( P - 2 ) e. ( ZZ>= ` 0 ) /\ ( # ` ( B ` L ) ) e. ( ZZ>= ` ( P - 2 ) ) ) )
252 224 250 251 sylanbrc 
 |-  ( ph -> ( P - 2 ) e. ( 0 ... ( # ` ( B ` L ) ) ) )
253 lencl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( # ` ( B ` L ) ) e. NN0 )
254 37 253 syl 
 |-  ( ph -> ( # ` ( B ` L ) ) e. NN0 )
255 254 59 eleqtrdi 
 |-  ( ph -> ( # ` ( B ` L ) ) e. ( ZZ>= ` 0 ) )
256 eluzfz2 
 |-  ( ( # ` ( B ` L ) ) e. ( ZZ>= ` 0 ) -> ( # ` ( B ` L ) ) e. ( 0 ... ( # ` ( B ` L ) ) ) )
257 255 256 syl 
 |-  ( ph -> ( # ` ( B ` L ) ) e. ( 0 ... ( # ` ( B ` L ) ) ) )
258 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 ) ) >. ) )
259 37 237 252 257 258 syl13anc 
 |-  ( ph -> ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) )
260 235 259 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 ) ) >. ) ) )
261 swrdcl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) e. Word ( I X. 2o ) )
262 37 261 syl 
 |-  ( ph -> ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) e. Word ( I X. 2o ) )
263 swrdcl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
264 37 263 syl 
 |-  ( ph -> ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
265 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 ) ) )
266 41 180 14 265 syl3anc 
 |-  ( ph -> ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) = ( P - ( Q + 2 ) ) )
267 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 ) )
268 37 237 252 267 syl3anc 
 |-  ( ph -> ( # ` ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) = ( ( P - 2 ) - Q ) )
269 83 67 75 sub32d 
 |-  ( ph -> ( ( P - Q ) - 2 ) = ( ( P - 2 ) - Q ) )
270 83 67 75 subsub4d 
 |-  ( ph -> ( ( P - Q ) - 2 ) = ( P - ( Q + 2 ) ) )
271 268 269 270 3eqtr2d 
 |-  ( ph -> ( # ` ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) = ( P - ( Q + 2 ) ) )
272 266 271 eqtr4d 
 |-  ( ph -> ( # ` ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) ) = ( # ` ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) )
273 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 ) ) >. ) ) ) )
274 187 143 262 264 272 273 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 ) ) >. ) ) ) )
275 260 274 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 ) ) >. ) ) )
276 275 simpld 
 |-  ( ph -> ( ( A ` K ) substr <. ( Q + 2 ) , P >. ) = ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) )
277 275 simprd 
 |-  ( ph -> ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) )
278 elfzuzb 
 |-  ( ( P - 2 ) e. ( 0 ... P ) <-> ( ( P - 2 ) e. ( ZZ>= ` 0 ) /\ P e. ( ZZ>= ` ( P - 2 ) ) ) )
279 224 248 278 sylanbrc 
 |-  ( ph -> ( P - 2 ) e. ( 0 ... P ) )
280 elfzuz 
 |-  ( P e. ( 0 ... ( # ` ( A ` K ) ) ) -> P e. ( ZZ>= ` 0 ) )
281 14 280 syl 
 |-  ( ph -> P e. ( ZZ>= ` 0 ) )
282 elfzuzb 
 |-  ( P e. ( 0 ... ( # ` ( B ` L ) ) ) <-> ( P e. ( ZZ>= ` 0 ) /\ ( # ` ( B ` L ) ) e. ( ZZ>= ` P ) ) )
283 281 239 282 sylanbrc 
 |-  ( ph -> P e. ( 0 ... ( # ` ( B ` L ) ) ) )
284 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 ) ) >. ) )
285 37 279 283 257 284 syl13anc 
 |-  ( ph -> ( ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) substr <. ( P - 2 ) , ( # ` ( B ` L ) ) >. ) )
286 277 285 eqtr4d 
 |-  ( ph -> ( <" U ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
287 swrdcl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. ( P - 2 ) , P >. ) e. Word ( I X. 2o ) )
288 37 287 syl 
 |-  ( ph -> ( ( B ` L ) substr <. ( P - 2 ) , P >. ) e. Word ( I X. 2o ) )
289 s2len 
 |-  ( # ` <" U ( M ` U ) "> ) = 2
290 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 ) ) )
291 37 279 283 290 syl3anc 
 |-  ( ph -> ( # ` ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) = ( P - ( P - 2 ) ) )
292 nncan 
 |-  ( ( P e. CC /\ 2 e. CC ) -> ( P - ( P - 2 ) ) = 2 )
293 83 74 292 sylancl 
 |-  ( ph -> ( P - ( P - 2 ) ) = 2 )
294 291 293 eqtr2d 
 |-  ( ph -> 2 = ( # ` ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) )
295 289 294 eqtrid 
 |-  ( ph -> ( # ` <" U ( M ` U ) "> ) = ( # ` ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) )
296 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 ) ) >. ) ) ) )
297 123 125 288 232 295 296 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 ) ) >. ) ) ) )
298 286 297 mpbid 
 |-  ( ph -> ( <" U ( M ` U ) "> = ( ( B ` L ) substr <. ( P - 2 ) , P >. ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) = ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
299 298 simprd 
 |-  ( ph -> ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) = ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) )
300 276 299 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 ) ) >. ) ) )
301 234 300 eqtr3d 
 |-  ( ph -> ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) = ( ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
302 301 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 ) ) >. ) ) ) )
303 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 ) ) >. ) ) ) )
304 39 262 232 303 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 ) ) >. ) ) ) )
305 302 304 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 ) ) >. ) ) )
306 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 ) ) )
307 37 237 252 306 syl3anc 
 |-  ( ph -> ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( P - 2 ) >. ) ) = ( ( B ` L ) prefix ( P - 2 ) ) )
308 307 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 ) ) >. ) ) )
309 23 305 308 3eqtrd 
 |-  ( ph -> ( S ` C ) = ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
310 ccatrid 
 |-  ( ( ( B ` L ) prefix ( P - 2 ) ) e. Word ( I X. 2o ) -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ (/) ) = ( ( B ` L ) prefix ( P - 2 ) ) )
311 230 310 syl 
 |-  ( ph -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ (/) ) = ( ( B ` L ) prefix ( P - 2 ) ) )
312 311 oveq1d 
 |-  ( ph -> ( ( ( ( B ` L ) prefix ( P - 2 ) ) ++ (/) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
313 309 312 eqtr4d 
 |-  ( ph -> ( S ` C ) = ( ( ( ( B ` L ) prefix ( P - 2 ) ) ++ (/) ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) )
314 pfxlen 
 |-  ( ( ( B ` L ) e. Word ( I X. 2o ) /\ ( P - 2 ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( # ` ( ( B ` L ) prefix ( P - 2 ) ) ) = ( P - 2 ) )
315 37 252 314 syl2anc 
 |-  ( ph -> ( # ` ( ( B ` L ) prefix ( P - 2 ) ) ) = ( P - 2 ) )
316 315 eqcomd 
 |-  ( ph -> ( P - 2 ) = ( # ` ( ( B ` L ) prefix ( P - 2 ) ) ) )
317 172 oveq2i 
 |-  ( ( P - 2 ) + ( # ` (/) ) ) = ( ( P - 2 ) + 0 )
318 81 zcnd 
 |-  ( ph -> ( P - 2 ) e. CC )
319 318 addridd 
 |-  ( ph -> ( ( P - 2 ) + 0 ) = ( P - 2 ) )
320 317 319 eqtr2id 
 |-  ( ph -> ( P - 2 ) = ( ( P - 2 ) + ( # ` (/) ) ) )
321 230 102 232 123 313 316 320 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 ) ) >. ) ) )
322 298 simpld 
 |-  ( ph -> <" U ( M ` U ) "> = ( ( B ` L ) substr <. ( P - 2 ) , P >. ) )
323 322 oveq2d 
 |-  ( ph -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ <" U ( M ` U ) "> ) = ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) )
324 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 ) )
325 37 279 283 324 syl3anc 
 |-  ( ph -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ ( ( B ` L ) substr <. ( P - 2 ) , P >. ) ) = ( ( B ` L ) prefix P ) )
326 323 325 eqtrd 
 |-  ( ph -> ( ( ( B ` L ) prefix ( P - 2 ) ) ++ <" U ( M ` U ) "> ) = ( ( B ` L ) prefix P ) )
327 326 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 ) ) >. ) ) )
328 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 ) ) ) )
329 37 283 257 328 syl3anc 
 |-  ( ph -> ( ( ( B ` L ) prefix P ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) prefix ( # ` ( B ` L ) ) ) )
330 pfxid 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) prefix ( # ` ( B ` L ) ) ) = ( B ` L ) )
331 37 330 syl 
 |-  ( ph -> ( ( B ` L ) prefix ( # ` ( B ` L ) ) ) = ( B ` L ) )
332 327 329 331 3eqtrd 
 |-  ( ph -> ( ( ( ( B ` L ) prefix ( P - 2 ) ) ++ <" U ( M ` U ) "> ) ++ ( ( B ` L ) substr <. P , ( # ` ( B ` L ) ) >. ) ) = ( B ` L ) )
333 228 321 332 3eqtrd 
 |-  ( ph -> ( ( P - 2 ) ( T ` ( S ` C ) ) U ) = ( B ` L ) )
334 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 ) ) )
335 219 226 16 334 syl3anc 
 |-  ( ph -> ( ( P - 2 ) ( T ` ( S ` C ) ) U ) e. ran ( T ` ( S ` C ) ) )
336 333 335 eqeltrrd 
 |-  ( ph -> ( B ` L ) e. ran ( T ` ( S ` C ) ) )
337 222 336 jca 
 |-  ( ph -> ( ( A ` K ) e. ran ( T ` ( S ` C ) ) /\ ( B ` L ) e. ran ( T ` ( S ` C ) ) ) )