Metamath Proof Explorer

Theorem efgredlemc

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the ending representation. (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 ) )
Assertion efgredlemc 
|- ( ph -> ( P e. ( ZZ>= ` Q ) -> ( A ` 0 ) = ( B ` 0 ) ) )

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 uzp1 
 |-  ( P e. ( ZZ>= ` Q ) -> ( P = Q \/ P e. ( ZZ>= ` ( Q + 1 ) ) ) )
22 fviss 
 |-  ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
23 1 22 eqsstri 
 |-  W C_ Word ( I X. 2o )
24 1 2 3 4 5 6 efgsdm 
 |-  ( A e. dom S <-> ( A e. ( Word W \ { (/) } ) /\ ( A ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` A ) ) ( A ` i ) e. ran ( T ` ( A ` ( i - 1 ) ) ) ) )
25 24 simp1bi 
 |-  ( A e. dom S -> A e. ( Word W \ { (/) } ) )
26 8 25 syl 
 |-  ( ph -> A e. ( Word W \ { (/) } ) )
27 26 eldifad 
 |-  ( ph -> A e. Word W )
28 wrdf 
 |-  ( A e. Word W -> A : ( 0 ..^ ( # ` A ) ) --> W )
29 27 28 syl 
 |-  ( ph -> A : ( 0 ..^ ( # ` A ) ) --> W )
30 fzossfz 
 |-  ( 0 ..^ ( ( # ` A ) - 1 ) ) C_ ( 0 ... ( ( # ` A ) - 1 ) )
31 1 2 3 4 5 6 7 8 9 10 11 efgredlema 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) e. NN /\ ( ( # ` B ) - 1 ) e. NN ) )
32 31 simpld 
 |-  ( ph -> ( ( # ` A ) - 1 ) e. NN )
33 fzo0end 
 |-  ( ( ( # ` A ) - 1 ) e. NN -> ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` A ) - 1 ) ) )
34 32 33 syl 
 |-  ( ph -> ( ( ( # ` A ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` A ) - 1 ) ) )
35 12 34 eqeltrid 
 |-  ( ph -> K e. ( 0 ..^ ( ( # ` A ) - 1 ) ) )
36 30 35 sselid 
 |-  ( ph -> K e. ( 0 ... ( ( # ` A ) - 1 ) ) )
37 lencl 
 |-  ( A e. Word W -> ( # ` A ) e. NN0 )
38 27 37 syl 
 |-  ( ph -> ( # ` A ) e. NN0 )
39 38 nn0zd 
 |-  ( ph -> ( # ` A ) e. ZZ )
40 fzoval 
 |-  ( ( # ` A ) e. ZZ -> ( 0 ..^ ( # ` A ) ) = ( 0 ... ( ( # ` A ) - 1 ) ) )
41 39 40 syl 
 |-  ( ph -> ( 0 ..^ ( # ` A ) ) = ( 0 ... ( ( # ` A ) - 1 ) ) )
42 36 41 eleqtrrd 
 |-  ( ph -> K e. ( 0 ..^ ( # ` A ) ) )
43 29 42 ffvelcdmd 
 |-  ( ph -> ( A ` K ) e. W )
44 23 43 sselid 
 |-  ( ph -> ( A ` K ) e. Word ( I X. 2o ) )
45 lencl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( # ` ( A ` K ) ) e. NN0 )
46 44 45 syl 
 |-  ( ph -> ( # ` ( A ` K ) ) e. NN0 )
47 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
48 46 47 eleqtrdi 
 |-  ( ph -> ( # ` ( A ` K ) ) e. ( ZZ>= ` 0 ) )
49 eluzfz2 
 |-  ( ( # ` ( A ` K ) ) e. ( ZZ>= ` 0 ) -> ( # ` ( A ` K ) ) e. ( 0 ... ( # ` ( A ` K ) ) ) )
50 48 49 syl 
 |-  ( ph -> ( # ` ( A ` K ) ) e. ( 0 ... ( # ` ( A ` K ) ) ) )
51 ccatpfx 
 |-  ( ( ( A ` K ) e. Word ( I X. 2o ) /\ P e. ( 0 ... ( # ` ( A ` K ) ) ) /\ ( # ` ( A ` K ) ) e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( ( ( A ` K ) prefix P ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( A ` K ) prefix ( # ` ( A ` K ) ) ) )
52 44 14 50 51 syl3anc 
 |-  ( ph -> ( ( ( A ` K ) prefix P ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( A ` K ) prefix ( # ` ( A ` K ) ) ) )
53 pfxid 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) prefix ( # ` ( A ` K ) ) ) = ( A ` K ) )
54 44 53 syl 
 |-  ( ph -> ( ( A ` K ) prefix ( # ` ( A ` K ) ) ) = ( A ` K ) )
55 52 54 eqtrd 
 |-  ( ph -> ( ( ( A ` K ) prefix P ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( A ` K ) )
56 1 2 3 4 5 6 efgsdm 
 |-  ( B e. dom S <-> ( B e. ( Word W \ { (/) } ) /\ ( B ` 0 ) e. D /\ A. i e. ( 1 ..^ ( # ` B ) ) ( B ` i ) e. ran ( T ` ( B ` ( i - 1 ) ) ) ) )
57 56 simp1bi 
 |-  ( B e. dom S -> B e. ( Word W \ { (/) } ) )
58 9 57 syl 
 |-  ( ph -> B e. ( Word W \ { (/) } ) )
59 58 eldifad 
 |-  ( ph -> B e. Word W )
60 wrdf 
 |-  ( B e. Word W -> B : ( 0 ..^ ( # ` B ) ) --> W )
61 59 60 syl 
 |-  ( ph -> B : ( 0 ..^ ( # ` B ) ) --> W )
62 fzossfz 
 |-  ( 0 ..^ ( ( # ` B ) - 1 ) ) C_ ( 0 ... ( ( # ` B ) - 1 ) )
63 31 simprd 
 |-  ( ph -> ( ( # ` B ) - 1 ) e. NN )
64 fzo0end 
 |-  ( ( ( # ` B ) - 1 ) e. NN -> ( ( ( # ` B ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` B ) - 1 ) ) )
65 63 64 syl 
 |-  ( ph -> ( ( ( # ` B ) - 1 ) - 1 ) e. ( 0 ..^ ( ( # ` B ) - 1 ) ) )
66 13 65 eqeltrid 
 |-  ( ph -> L e. ( 0 ..^ ( ( # ` B ) - 1 ) ) )
67 62 66 sselid 
 |-  ( ph -> L e. ( 0 ... ( ( # ` B ) - 1 ) ) )
68 lencl 
 |-  ( B e. Word W -> ( # ` B ) e. NN0 )
69 59 68 syl 
 |-  ( ph -> ( # ` B ) e. NN0 )
70 69 nn0zd 
 |-  ( ph -> ( # ` B ) e. ZZ )
71 fzoval 
 |-  ( ( # ` B ) e. ZZ -> ( 0 ..^ ( # ` B ) ) = ( 0 ... ( ( # ` B ) - 1 ) ) )
72 70 71 syl 
 |-  ( ph -> ( 0 ..^ ( # ` B ) ) = ( 0 ... ( ( # ` B ) - 1 ) ) )
73 67 72 eleqtrrd 
 |-  ( ph -> L e. ( 0 ..^ ( # ` B ) ) )
74 61 73 ffvelcdmd 
 |-  ( ph -> ( B ` L ) e. W )
75 23 74 sselid 
 |-  ( ph -> ( B ` L ) e. Word ( I X. 2o ) )
76 lencl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( # ` ( B ` L ) ) e. NN0 )
77 75 76 syl 
 |-  ( ph -> ( # ` ( B ` L ) ) e. NN0 )
78 77 47 eleqtrdi 
 |-  ( ph -> ( # ` ( B ` L ) ) e. ( ZZ>= ` 0 ) )
79 eluzfz2 
 |-  ( ( # ` ( B ` L ) ) e. ( ZZ>= ` 0 ) -> ( # ` ( B ` L ) ) e. ( 0 ... ( # ` ( B ` L ) ) ) )
80 78 79 syl 
 |-  ( ph -> ( # ` ( B ` L ) ) e. ( 0 ... ( # ` ( B ` L ) ) ) )
81 ccatpfx 
 |-  ( ( ( B ` L ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... ( # ` ( B ` L ) ) ) /\ ( # ` ( B ` L ) ) e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) prefix ( # ` ( B ` L ) ) ) )
82 75 15 80 81 syl3anc 
 |-  ( ph -> ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) = ( ( B ` L ) prefix ( # ` ( B ` L ) ) ) )
83 pfxid 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) prefix ( # ` ( B ` L ) ) ) = ( B ` L ) )
84 75 83 syl 
 |-  ( ph -> ( ( B ` L ) prefix ( # ` ( B ` L ) ) ) = ( B ` L ) )
85 82 84 eqtrd 
 |-  ( ph -> ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) = ( B ` L ) )
86 55 85 eqeq12d 
 |-  ( ph -> ( ( ( ( A ` K ) prefix P ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) <-> ( A ` K ) = ( B ` L ) ) )
87 20 86 mtbird 
 |-  ( ph -> -. ( ( ( A ` K ) prefix P ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
88 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 ) "> >. ) )
89 43 14 16 88 syl3anc 
 |-  ( ph -> ( P ( T ` ( A ` K ) ) U ) = ( ( A ` K ) splice <. P , P , <" U ( M ` U ) "> >. ) )
90 3 efgmf 
 |-  M : ( I X. 2o ) --> ( I X. 2o )
91 90 ffvelcdmi 
 |-  ( U e. ( I X. 2o ) -> ( M ` U ) e. ( I X. 2o ) )
92 16 91 syl 
 |-  ( ph -> ( M ` U ) e. ( I X. 2o ) )
93 16 92 s2cld 
 |-  ( ph -> <" U ( M ` U ) "> e. Word ( I X. 2o ) )
94 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 ) ) >. ) ) )
95 43 14 14 93 94 syl13anc 
 |-  ( ph -> ( ( A ` K ) splice <. P , P , <" U ( M ` U ) "> >. ) = ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) )
96 18 89 95 3eqtrd 
 |-  ( ph -> ( S ` A ) = ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) )
97 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 ) "> >. ) )
98 74 15 17 97 syl3anc 
 |-  ( ph -> ( Q ( T ` ( B ` L ) ) V ) = ( ( B ` L ) splice <. Q , Q , <" V ( M ` V ) "> >. ) )
99 90 ffvelcdmi 
 |-  ( V e. ( I X. 2o ) -> ( M ` V ) e. ( I X. 2o ) )
100 17 99 syl 
 |-  ( ph -> ( M ` V ) e. ( I X. 2o ) )
101 17 100 s2cld 
 |-  ( ph -> <" V ( M ` V ) "> e. Word ( I X. 2o ) )
102 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 ) ) >. ) ) )
103 74 15 15 101 102 syl13anc 
 |-  ( ph -> ( ( B ` L ) splice <. Q , Q , <" V ( M ` V ) "> >. ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
104 19 98 103 3eqtrd 
 |-  ( ph -> ( S ` B ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
105 10 96 104 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 ) ) >. ) ) )
106 105 adantr 
 |-  ( ( ph /\ P = Q ) -> ( ( ( ( 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 ) ) >. ) ) )
107 pfxcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) )
108 44 107 syl 
 |-  ( ph -> ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) )
109 108 adantr 
 |-  ( ( ph /\ P = Q ) -> ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) )
110 93 adantr 
 |-  ( ( ph /\ P = Q ) -> <" U ( M ` U ) "> e. Word ( I X. 2o ) )
111 ccatcl 
 |-  ( ( ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) /\ <" U ( M ` U ) "> e. Word ( I X. 2o ) ) -> ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) e. Word ( I X. 2o ) )
112 109 110 111 syl2anc 
 |-  ( ( ph /\ P = Q ) -> ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) e. Word ( I X. 2o ) )
113 swrdcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) )
114 44 113 syl 
 |-  ( ph -> ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) )
115 114 adantr 
 |-  ( ( ph /\ P = Q ) -> ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) )
116 pfxcl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) )
117 75 116 syl 
 |-  ( ph -> ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) )
118 117 adantr 
 |-  ( ( ph /\ P = Q ) -> ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) )
119 101 adantr 
 |-  ( ( ph /\ P = Q ) -> <" V ( M ` V ) "> e. Word ( I X. 2o ) )
120 ccatcl 
 |-  ( ( ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) /\ <" V ( M ` V ) "> e. Word ( I X. 2o ) ) -> ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) e. Word ( I X. 2o ) )
121 118 119 120 syl2anc 
 |-  ( ( ph /\ P = Q ) -> ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) e. Word ( I X. 2o ) )
122 swrdcl 
 |-  ( ( B ` L ) e. Word ( I X. 2o ) -> ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
123 75 122 syl 
 |-  ( ph -> ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
124 123 adantr 
 |-  ( ( ph /\ P = Q ) -> ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
125 pfxlen 
 |-  ( ( ( A ` K ) e. Word ( I X. 2o ) /\ P e. ( 0 ... ( # ` ( A ` K ) ) ) ) -> ( # ` ( ( A ` K ) prefix P ) ) = P )
126 44 14 125 syl2anc 
 |-  ( ph -> ( # ` ( ( A ` K ) prefix P ) ) = P )
127 pfxlen 
 |-  ( ( ( B ` L ) e. Word ( I X. 2o ) /\ Q e. ( 0 ... ( # ` ( B ` L ) ) ) ) -> ( # ` ( ( B ` L ) prefix Q ) ) = Q )
128 75 15 127 syl2anc 
 |-  ( ph -> ( # ` ( ( B ` L ) prefix Q ) ) = Q )
129 126 128 eqeq12d 
 |-  ( ph -> ( ( # ` ( ( A ` K ) prefix P ) ) = ( # ` ( ( B ` L ) prefix Q ) ) <-> P = Q ) )
130 129 biimpar 
 |-  ( ( ph /\ P = Q ) -> ( # ` ( ( A ` K ) prefix P ) ) = ( # ` ( ( B ` L ) prefix Q ) ) )
131 s2len 
 |-  ( # ` <" U ( M ` U ) "> ) = 2
132 s2len 
 |-  ( # ` <" V ( M ` V ) "> ) = 2
133 131 132 eqtr4i 
 |-  ( # ` <" U ( M ` U ) "> ) = ( # ` <" V ( M ` V ) "> )
134 133 a1i 
 |-  ( ( ph /\ P = Q ) -> ( # ` <" U ( M ` U ) "> ) = ( # ` <" V ( M ` V ) "> ) )
135 130 134 oveq12d 
 |-  ( ( ph /\ P = Q ) -> ( ( # ` ( ( A ` K ) prefix P ) ) + ( # ` <" U ( M ` U ) "> ) ) = ( ( # ` ( ( B ` L ) prefix Q ) ) + ( # ` <" V ( M ` V ) "> ) ) )
136 ccatlen 
 |-  ( ( ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) /\ <" U ( M ` U ) "> e. Word ( I X. 2o ) ) -> ( # ` ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ) = ( ( # ` ( ( A ` K ) prefix P ) ) + ( # ` <" U ( M ` U ) "> ) ) )
137 109 110 136 syl2anc 
 |-  ( ( ph /\ P = Q ) -> ( # ` ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ) = ( ( # ` ( ( A ` K ) prefix P ) ) + ( # ` <" U ( M ` U ) "> ) ) )
138 ccatlen 
 |-  ( ( ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) /\ <" V ( M ` V ) "> e. Word ( I X. 2o ) ) -> ( # ` ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ) = ( ( # ` ( ( B ` L ) prefix Q ) ) + ( # ` <" V ( M ` V ) "> ) ) )
139 118 119 138 syl2anc 
 |-  ( ( ph /\ P = Q ) -> ( # ` ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ) = ( ( # ` ( ( B ` L ) prefix Q ) ) + ( # ` <" V ( M ` V ) "> ) ) )
140 135 137 139 3eqtr4d 
 |-  ( ( ph /\ P = Q ) -> ( # ` ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ) = ( # ` ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ) )
141 ccatopth 
 |-  ( ( ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) e. Word ( I X. 2o ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) ) /\ ( ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) /\ ( # ` ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) ) = ( # ` ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) ) ) -> ( ( ( ( ( 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 ) ) >. ) ) <-> ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) = ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) )
142 112 115 121 124 140 141 syl221anc 
 |-  ( ( ph /\ P = Q ) -> ( ( ( ( ( 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 ) ) >. ) ) <-> ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) = ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) )
143 106 142 mpbid 
 |-  ( ( ph /\ P = Q ) -> ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) = ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
144 143 simpld 
 |-  ( ( ph /\ P = Q ) -> ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) = ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) )
145 ccatopth 
 |-  ( ( ( ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) /\ <" U ( M ` U ) "> e. Word ( I X. 2o ) ) /\ ( ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) /\ <" V ( M ` V ) "> e. Word ( I X. 2o ) ) /\ ( # ` ( ( A ` K ) prefix P ) ) = ( # ` ( ( B ` L ) prefix Q ) ) ) -> ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) = ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) <-> ( ( ( A ` K ) prefix P ) = ( ( B ` L ) prefix Q ) /\ <" U ( M ` U ) "> = <" V ( M ` V ) "> ) ) )
146 109 110 118 119 130 145 syl221anc 
 |-  ( ( ph /\ P = Q ) -> ( ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) = ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) <-> ( ( ( A ` K ) prefix P ) = ( ( B ` L ) prefix Q ) /\ <" U ( M ` U ) "> = <" V ( M ` V ) "> ) ) )
147 144 146 mpbid 
 |-  ( ( ph /\ P = Q ) -> ( ( ( A ` K ) prefix P ) = ( ( B ` L ) prefix Q ) /\ <" U ( M ` U ) "> = <" V ( M ` V ) "> ) )
148 147 simpld 
 |-  ( ( ph /\ P = Q ) -> ( ( A ` K ) prefix P ) = ( ( B ` L ) prefix Q ) )
149 143 simprd 
 |-  ( ( ph /\ P = Q ) -> ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) )
150 148 149 oveq12d 
 |-  ( ( ph /\ P = Q ) -> ( ( ( A ` K ) prefix P ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
151 87 150 mtand 
 |-  ( ph -> -. P = Q )
152 151 pm2.21d 
 |-  ( ph -> ( P = Q -> ( A ` 0 ) = ( B ` 0 ) ) )
153 uzp1 
 |-  ( P e. ( ZZ>= ` ( Q + 1 ) ) -> ( P = ( Q + 1 ) \/ P e. ( ZZ>= ` ( ( Q + 1 ) + 1 ) ) ) )
154 16 s1cld 
 |-  ( ph -> <" U "> e. Word ( I X. 2o ) )
155 ccatcl 
 |-  ( ( ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) /\ <" U "> e. Word ( I X. 2o ) ) -> ( ( ( A ` K ) prefix P ) ++ <" U "> ) e. Word ( I X. 2o ) )
156 108 154 155 syl2anc 
 |-  ( ph -> ( ( ( A ` K ) prefix P ) ++ <" U "> ) e. Word ( I X. 2o ) )
157 92 s1cld 
 |-  ( ph -> <" ( M ` U ) "> e. Word ( I X. 2o ) )
158 ccatass 
 |-  ( ( ( ( ( A ` K ) prefix P ) ++ <" U "> ) e. Word ( I X. 2o ) /\ <" ( 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 ) ) >. ) ) ) )
159 156 157 114 158 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 ) ) >. ) ) ) )
160 ccatass 
 |-  ( ( ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) /\ <" U "> e. Word ( I X. 2o ) /\ <" ( M ` U ) "> e. Word ( I X. 2o ) ) -> ( ( ( ( A ` K ) prefix P ) ++ <" U "> ) ++ <" ( M ` U ) "> ) = ( ( ( A ` K ) prefix P ) ++ ( <" U "> ++ <" ( M ` U ) "> ) ) )
161 108 154 157 160 syl3anc 
 |-  ( ph -> ( ( ( ( A ` K ) prefix P ) ++ <" U "> ) ++ <" ( M ` U ) "> ) = ( ( ( A ` K ) prefix P ) ++ ( <" U "> ++ <" ( M ` U ) "> ) ) )
162 df-s2 
 |-  <" U ( M ` U ) "> = ( <" U "> ++ <" ( M ` U ) "> )
163 162 oveq2i 
 |-  ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) = ( ( ( A ` K ) prefix P ) ++ ( <" U "> ++ <" ( M ` U ) "> ) )
164 161 163 eqtr4di 
 |-  ( ph -> ( ( ( ( A ` K ) prefix P ) ++ <" U "> ) ++ <" ( M ` U ) "> ) = ( ( ( A ` K ) prefix P ) ++ <" U ( M ` U ) "> ) )
165 164 oveq1d 
 |-  ( 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 ) ) >. ) ) )
166 17 s1cld 
 |-  ( ph -> <" V "> e. Word ( I X. 2o ) )
167 100 s1cld 
 |-  ( ph -> <" ( M ` V ) "> e. Word ( I X. 2o ) )
168 ccatass 
 |-  ( ( ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) /\ <" V "> e. Word ( I X. 2o ) /\ <" ( M ` V ) "> e. Word ( I X. 2o ) ) -> ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) = ( ( ( B ` L ) prefix Q ) ++ ( <" V "> ++ <" ( M ` V ) "> ) ) )
169 117 166 167 168 syl3anc 
 |-  ( ph -> ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) = ( ( ( B ` L ) prefix Q ) ++ ( <" V "> ++ <" ( M ` V ) "> ) ) )
170 df-s2 
 |-  <" V ( M ` V ) "> = ( <" V "> ++ <" ( M ` V ) "> )
171 170 oveq2i 
 |-  ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) = ( ( ( B ` L ) prefix Q ) ++ ( <" V "> ++ <" ( M ` V ) "> ) )
172 169 171 eqtr4di 
 |-  ( ph -> ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) = ( ( ( B ` L ) prefix Q ) ++ <" V ( M ` V ) "> ) )
173 172 oveq1d 
 |-  ( 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 ) ) >. ) ) )
174 105 165 173 3eqtr4d 
 |-  ( 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 ) ) >. ) ) )
175 159 174 eqtr3d 
 |-  ( 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 ) ) >. ) ) )
176 175 adantr 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( ( ( 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 ) ) >. ) ) )
177 156 adantr 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( ( A ` K ) prefix P ) ++ <" U "> ) e. Word ( I X. 2o ) )
178 157 adantr 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> <" ( M ` U ) "> e. Word ( I X. 2o ) )
179 114 adantr 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) )
180 ccatcl 
 |-  ( ( <" ( M ` U ) "> e. Word ( I X. 2o ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) ) -> ( <" ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) )
181 178 179 180 syl2anc 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( <" ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) )
182 ccatcl 
 |-  ( ( ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) /\ <" V "> e. Word ( I X. 2o ) ) -> ( ( ( B ` L ) prefix Q ) ++ <" V "> ) e. Word ( I X. 2o ) )
183 117 166 182 syl2anc 
 |-  ( ph -> ( ( ( B ` L ) prefix Q ) ++ <" V "> ) e. Word ( I X. 2o ) )
184 183 adantr 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( ( B ` L ) prefix Q ) ++ <" V "> ) e. Word ( I X. 2o ) )
185 167 adantr 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> <" ( M ` V ) "> e. Word ( I X. 2o ) )
186 ccatcl 
 |-  ( ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) e. Word ( I X. 2o ) /\ <" ( M ` V ) "> e. Word ( I X. 2o ) ) -> ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) e. Word ( I X. 2o ) )
187 184 185 186 syl2anc 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) e. Word ( I X. 2o ) )
188 123 adantr 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) )
189 ccatlen 
 |-  ( ( ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) /\ <" V "> e. Word ( I X. 2o ) ) -> ( # ` ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ) = ( ( # ` ( ( B ` L ) prefix Q ) ) + ( # ` <" V "> ) ) )
190 117 166 189 syl2anc 
 |-  ( ph -> ( # ` ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ) = ( ( # ` ( ( B ` L ) prefix Q ) ) + ( # ` <" V "> ) ) )
191 s1len 
 |-  ( # ` <" V "> ) = 1
192 191 a1i 
 |-  ( ph -> ( # ` <" V "> ) = 1 )
193 128 192 oveq12d 
 |-  ( ph -> ( ( # ` ( ( B ` L ) prefix Q ) ) + ( # ` <" V "> ) ) = ( Q + 1 ) )
194 190 193 eqtrd 
 |-  ( ph -> ( # ` ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ) = ( Q + 1 ) )
195 126 194 eqeq12d 
 |-  ( ph -> ( ( # ` ( ( A ` K ) prefix P ) ) = ( # ` ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ) <-> P = ( Q + 1 ) ) )
196 195 biimpar 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( # ` ( ( A ` K ) prefix P ) ) = ( # ` ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ) )
197 s1len 
 |-  ( # ` <" U "> ) = 1
198 s1len 
 |-  ( # ` <" ( M ` V ) "> ) = 1
199 197 198 eqtr4i 
 |-  ( # ` <" U "> ) = ( # ` <" ( M ` V ) "> )
200 199 a1i 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( # ` <" U "> ) = ( # ` <" ( M ` V ) "> ) )
201 196 200 oveq12d 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( # ` ( ( A ` K ) prefix P ) ) + ( # ` <" U "> ) ) = ( ( # ` ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ) + ( # ` <" ( M ` V ) "> ) ) )
202 108 adantr 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) )
203 154 adantr 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> <" U "> e. Word ( I X. 2o ) )
204 ccatlen 
 |-  ( ( ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) /\ <" U "> e. Word ( I X. 2o ) ) -> ( # ` ( ( ( A ` K ) prefix P ) ++ <" U "> ) ) = ( ( # ` ( ( A ` K ) prefix P ) ) + ( # ` <" U "> ) ) )
205 202 203 204 syl2anc 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( # ` ( ( ( A ` K ) prefix P ) ++ <" U "> ) ) = ( ( # ` ( ( A ` K ) prefix P ) ) + ( # ` <" U "> ) ) )
206 ccatlen 
 |-  ( ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) e. Word ( I X. 2o ) /\ <" ( M ` V ) "> e. Word ( I X. 2o ) ) -> ( # ` ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) ) = ( ( # ` ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ) + ( # ` <" ( M ` V ) "> ) ) )
207 184 185 206 syl2anc 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( # ` ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) ) = ( ( # ` ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ) + ( # ` <" ( M ` V ) "> ) ) )
208 201 205 207 3eqtr4d 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( # ` ( ( ( A ` K ) prefix P ) ++ <" U "> ) ) = ( # ` ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) ) )
209 ccatopth 
 |-  ( ( ( ( ( ( A ` K ) prefix P ) ++ <" U "> ) e. Word ( I X. 2o ) /\ ( <" ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) ) /\ ( ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) e. Word ( I X. 2o ) /\ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) e. Word ( I X. 2o ) ) /\ ( # ` ( ( ( A ` K ) prefix P ) ++ <" U "> ) ) = ( # ` ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) ) ) -> ( ( ( ( ( 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 ) ) >. ) ) <-> ( ( ( ( A ` K ) prefix P ) ++ <" U "> ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) /\ ( <" ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) )
210 177 181 187 188 208 209 syl221anc 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( ( ( ( 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 ) ) >. ) ) <-> ( ( ( ( A ` K ) prefix P ) ++ <" U "> ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) /\ ( <" ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) ) )
211 176 210 mpbid 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( ( ( A ` K ) prefix P ) ++ <" U "> ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) /\ ( <" ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
212 211 simpld 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( ( A ` K ) prefix P ) ++ <" U "> ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) )
213 ccatopth 
 |-  ( ( ( ( ( A ` K ) prefix P ) e. Word ( I X. 2o ) /\ <" U "> e. Word ( I X. 2o ) ) /\ ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) e. Word ( I X. 2o ) /\ <" ( M ` V ) "> e. Word ( I X. 2o ) ) /\ ( # ` ( ( A ` K ) prefix P ) ) = ( # ` ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ) ) -> ( ( ( ( A ` K ) prefix P ) ++ <" U "> ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) <-> ( ( ( A ` K ) prefix P ) = ( ( ( B ` L ) prefix Q ) ++ <" V "> ) /\ <" U "> = <" ( M ` V ) "> ) ) )
214 202 203 184 185 196 213 syl221anc 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( ( ( A ` K ) prefix P ) ++ <" U "> ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ <" ( M ` V ) "> ) <-> ( ( ( A ` K ) prefix P ) = ( ( ( B ` L ) prefix Q ) ++ <" V "> ) /\ <" U "> = <" ( M ` V ) "> ) ) )
215 212 214 mpbid 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( ( A ` K ) prefix P ) = ( ( ( B ` L ) prefix Q ) ++ <" V "> ) /\ <" U "> = <" ( M ` V ) "> ) )
216 215 simpld 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( A ` K ) prefix P ) = ( ( ( B ` L ) prefix Q ) ++ <" V "> ) )
217 216 oveq1d 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( ( A ` K ) prefix P ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) )
218 117 adantr 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) )
219 166 adantr 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> <" V "> e. Word ( I X. 2o ) )
220 ccatass 
 |-  ( ( ( ( B ` L ) prefix Q ) e. Word ( I X. 2o ) /\ <" V "> e. Word ( I X. 2o ) /\ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) ) -> ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( <" V "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) )
221 218 219 179 220 syl3anc 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( ( ( B ` L ) prefix Q ) ++ <" V "> ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( <" V "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) )
222 215 simprd 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> <" U "> = <" ( M ` V ) "> )
223 s111 
 |-  ( ( U e. ( I X. 2o ) /\ ( M ` V ) e. ( I X. 2o ) ) -> ( <" U "> = <" ( M ` V ) "> <-> U = ( M ` V ) ) )
224 16 100 223 syl2anc 
 |-  ( ph -> ( <" U "> = <" ( M ` V ) "> <-> U = ( M ` V ) ) )
225 224 adantr 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( <" U "> = <" ( M ` V ) "> <-> U = ( M ` V ) ) )
226 222 225 mpbid 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> U = ( M ` V ) )
227 226 fveq2d 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( M ` U ) = ( M ` ( M ` V ) ) )
228 3 efgmnvl 
 |-  ( V e. ( I X. 2o ) -> ( M ` ( M ` V ) ) = V )
229 17 228 syl 
 |-  ( ph -> ( M ` ( M ` V ) ) = V )
230 229 adantr 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( M ` ( M ` V ) ) = V )
231 227 230 eqtrd 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( M ` U ) = V )
232 231 s1eqd 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> <" ( M ` U ) "> = <" V "> )
233 232 oveq1d 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( <" ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( <" V "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) )
234 211 simprd 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( <" ( M ` U ) "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) )
235 233 234 eqtr3d 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( <" V "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) )
236 235 oveq2d 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( ( B ` L ) prefix Q ) ++ ( <" V "> ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) ) = ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
237 217 221 236 3eqtrd 
 |-  ( ( ph /\ P = ( Q + 1 ) ) -> ( ( ( A ` K ) prefix P ) ++ ( ( A ` K ) substr <. P , ( # ` ( A ` K ) ) >. ) ) = ( ( ( B ` L ) prefix Q ) ++ ( ( B ` L ) substr <. Q , ( # ` ( B ` L ) ) >. ) ) )
238 87 237 mtand 
 |-  ( ph -> -. P = ( Q + 1 ) )
239 238 pm2.21d 
 |-  ( ph -> ( P = ( Q + 1 ) -> ( A ` 0 ) = ( B ` 0 ) ) )
240 15 elfzelzd 
 |-  ( ph -> Q e. ZZ )
241 240 zcnd 
 |-  ( ph -> Q e. CC )
242 1cnd 
 |-  ( ph -> 1 e. CC )
243 241 242 242 addassd 
 |-  ( ph -> ( ( Q + 1 ) + 1 ) = ( Q + ( 1 + 1 ) ) )
244 df-2 
 |-  2 = ( 1 + 1 )
245 244 oveq2i 
 |-  ( Q + 2 ) = ( Q + ( 1 + 1 ) )
246 243 245 eqtr4di 
 |-  ( ph -> ( ( Q + 1 ) + 1 ) = ( Q + 2 ) )
247 246 fveq2d 
 |-  ( ph -> ( ZZ>= ` ( ( Q + 1 ) + 1 ) ) = ( ZZ>= ` ( Q + 2 ) ) )
248 247 eleq2d 
 |-  ( ph -> ( P e. ( ZZ>= ` ( ( Q + 1 ) + 1 ) ) <-> P e. ( ZZ>= ` ( Q + 2 ) ) ) )
249 1 2 3 4 5 6 efgsfo 
 |-  S : dom S -onto-> W
250 swrdcl 
 |-  ( ( A ` K ) e. Word ( I X. 2o ) -> ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) )
251 44 250 syl 
 |-  ( ph -> ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) e. Word ( I X. 2o ) )
252 ccatcl 
 |-  ( ( ( ( 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 ) ) >. ) ) e. Word ( I X. 2o ) )
253 117 251 252 syl2anc 
 |-  ( ph -> ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) e. Word ( I X. 2o ) )
254 1 efgrcl 
 |-  ( ( A ` K ) e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
255 43 254 syl 
 |-  ( ph -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
256 255 simprd 
 |-  ( ph -> W = Word ( I X. 2o ) )
257 253 256 eleqtrrd 
 |-  ( ph -> ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) e. W )
258 foelrn 
 |-  ( ( S : dom S -onto-> W /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) e. W ) -> E. c e. dom S ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) )
259 249 257 258 sylancr 
 |-  ( ph -> E. c e. dom S ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) )
260 259 adantr 
 |-  ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) -> E. c e. dom S ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) )
261 7 ad2antrr 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` A ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
262 8 ad2antrr 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> A e. dom S )
263 9 ad2antrr 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> B e. dom S )
264 10 ad2antrr 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> ( S ` A ) = ( S ` B ) )
265 11 ad2antrr 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> -. ( A ` 0 ) = ( B ` 0 ) )
266 14 ad2antrr 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> P e. ( 0 ... ( # ` ( A ` K ) ) ) )
267 15 ad2antrr 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> Q e. ( 0 ... ( # ` ( B ` L ) ) ) )
268 16 ad2antrr 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> U e. ( I X. 2o ) )
269 17 ad2antrr 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> V e. ( I X. 2o ) )
270 18 ad2antrr 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> ( S ` A ) = ( P ( T ` ( A ` K ) ) U ) )
271 19 ad2antrr 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> ( S ` B ) = ( Q ( T ` ( B ` L ) ) V ) )
272 20 ad2antrr 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> -. ( A ` K ) = ( B ` L ) )
273 simplr 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> P e. ( ZZ>= ` ( Q + 2 ) ) )
274 simprl 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> c e. dom S )
275 simprr 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) )
276 275 eqcomd 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> ( S ` c ) = ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) )
277 1 2 3 4 5 6 261 262 263 264 265 12 13 266 267 268 269 270 271 272 273 274 276 efgredlemd 
 |-  ( ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) /\ ( c e. dom S /\ ( ( ( B ` L ) prefix Q ) ++ ( ( A ` K ) substr <. ( Q + 2 ) , ( # ` ( A ` K ) ) >. ) ) = ( S ` c ) ) ) -> ( A ` 0 ) = ( B ` 0 ) )
278 260 277 rexlimddv 
 |-  ( ( ph /\ P e. ( ZZ>= ` ( Q + 2 ) ) ) -> ( A ` 0 ) = ( B ` 0 ) )
279 278 ex 
 |-  ( ph -> ( P e. ( ZZ>= ` ( Q + 2 ) ) -> ( A ` 0 ) = ( B ` 0 ) ) )
280 248 279 sylbid 
 |-  ( ph -> ( P e. ( ZZ>= ` ( ( Q + 1 ) + 1 ) ) -> ( A ` 0 ) = ( B ` 0 ) ) )
281 239 280 jaod 
 |-  ( ph -> ( ( P = ( Q + 1 ) \/ P e. ( ZZ>= ` ( ( Q + 1 ) + 1 ) ) ) -> ( A ` 0 ) = ( B ` 0 ) ) )
282 153 281 syl5 
 |-  ( ph -> ( P e. ( ZZ>= ` ( Q + 1 ) ) -> ( A ` 0 ) = ( B ` 0 ) ) )
283 152 282 jaod 
 |-  ( ph -> ( ( P = Q \/ P e. ( ZZ>= ` ( Q + 1 ) ) ) -> ( A ` 0 ) = ( B ` 0 ) ) )
284 21 283 syl5 
 |-  ( ph -> ( P e. ( ZZ>= ` Q ) -> ( A ` 0 ) = ( B ` 0 ) ) )