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 × 2 𝑜
efgval.r ˙ = ~ FG I
efgval2.m M = y I , z 2 𝑜 y 1 𝑜 z
efgval2.t T = v W n 0 v , w I × 2 𝑜 v splice n n ⟨“ w M w ”⟩
efgred.d D = W x W ran T x
efgred.s S = m t Word W | t 0 D k 1 ..^ t t k ran T t k 1 m m 1
efgredlem.1 φ a dom S b dom S S a < S A S a = S b a 0 = b 0
efgredlem.2 φ A dom S
efgredlem.3 φ B dom S
efgredlem.4 φ S A = S B
efgredlem.5 φ ¬ A 0 = B 0
efgredlemb.k K = A - 1 - 1
efgredlemb.l L = B - 1 - 1
efgredlemb.p φ P 0 A K
efgredlemb.q φ Q 0 B L
efgredlemb.u φ U I × 2 𝑜
efgredlemb.v φ V I × 2 𝑜
efgredlemb.6 φ S A = P T A K U
efgredlemb.7 φ S B = Q T B L V
efgredlemb.8 φ ¬ A K = B L
Assertion efgredlemc φ P Q A 0 = B 0

Proof

Step Hyp Ref Expression
1 efgval.w W = I Word I × 2 𝑜
2 efgval.r ˙ = ~ FG I
3 efgval2.m M = y I , z 2 𝑜 y 1 𝑜 z
4 efgval2.t T = v W n 0 v , w I × 2 𝑜 v splice n n ⟨“ w M w ”⟩
5 efgred.d D = W x W ran T x
6 efgred.s S = m t Word W | t 0 D k 1 ..^ t t k ran T t k 1 m m 1
7 efgredlem.1 φ a dom S b dom S S a < S A S a = S b a 0 = b 0
8 efgredlem.2 φ A dom S
9 efgredlem.3 φ B dom S
10 efgredlem.4 φ S A = S B
11 efgredlem.5 φ ¬ A 0 = B 0
12 efgredlemb.k K = A - 1 - 1
13 efgredlemb.l L = B - 1 - 1
14 efgredlemb.p φ P 0 A K
15 efgredlemb.q φ Q 0 B L
16 efgredlemb.u φ U I × 2 𝑜
17 efgredlemb.v φ V I × 2 𝑜
18 efgredlemb.6 φ S A = P T A K U
19 efgredlemb.7 φ S B = Q T B L V
20 efgredlemb.8 φ ¬ A K = B L
21 uzp1 P Q P = Q P Q + 1
22 fviss I Word I × 2 𝑜 Word I × 2 𝑜
23 1 22 eqsstri W Word I × 2 𝑜
24 1 2 3 4 5 6 efgsdm A dom S A Word W A 0 D i 1 ..^ A A i ran T A i 1
25 24 simp1bi A dom S A Word W
26 8 25 syl φ A Word W
27 26 eldifad φ A Word W
28 wrdf A Word W A : 0 ..^ A W
29 27 28 syl φ A : 0 ..^ A W
30 fzossfz 0 ..^ A 1 0 A 1
31 1 2 3 4 5 6 7 8 9 10 11 efgredlema φ A 1 B 1
32 31 simpld φ A 1
33 fzo0end A 1 A - 1 - 1 0 ..^ A 1
34 32 33 syl φ A - 1 - 1 0 ..^ A 1
35 12 34 eqeltrid φ K 0 ..^ A 1
36 30 35 sselid φ K 0 A 1
37 lencl A Word W A 0
38 27 37 syl φ A 0
39 38 nn0zd φ A
40 fzoval A 0 ..^ A = 0 A 1
41 39 40 syl φ 0 ..^ A = 0 A 1
42 36 41 eleqtrrd φ K 0 ..^ A
43 29 42 ffvelrnd φ A K W
44 23 43 sselid φ A K Word I × 2 𝑜
45 lencl A K Word I × 2 𝑜 A K 0
46 44 45 syl φ A K 0
47 nn0uz 0 = 0
48 46 47 eleqtrdi φ A K 0
49 eluzfz2 A K 0 A K 0 A K
50 48 49 syl φ A K 0 A K
51 ccatpfx A K Word I × 2 𝑜 P 0 A K A K 0 A K A K prefix P ++ A K substr P A K = A K prefix A K
52 44 14 50 51 syl3anc φ A K prefix P ++ A K substr P A K = A K prefix A K
53 pfxid A K Word I × 2 𝑜 A K prefix A K = A K
54 44 53 syl φ A K prefix A K = A K
55 52 54 eqtrd φ A K prefix P ++ A K substr P A K = A K
56 1 2 3 4 5 6 efgsdm B dom S B Word W B 0 D i 1 ..^ B B i ran T B i 1
57 56 simp1bi B dom S B Word W
58 9 57 syl φ B Word W
59 58 eldifad φ B Word W
60 wrdf B Word W B : 0 ..^ B W
61 59 60 syl φ B : 0 ..^ B W
62 fzossfz 0 ..^ B 1 0 B 1
63 31 simprd φ B 1
64 fzo0end B 1 B - 1 - 1 0 ..^ B 1
65 63 64 syl φ B - 1 - 1 0 ..^ B 1
66 13 65 eqeltrid φ L 0 ..^ B 1
67 62 66 sselid φ L 0 B 1
68 lencl B Word W B 0
69 59 68 syl φ B 0
70 69 nn0zd φ B
71 fzoval B 0 ..^ B = 0 B 1
72 70 71 syl φ 0 ..^ B = 0 B 1
73 67 72 eleqtrrd φ L 0 ..^ B
74 61 73 ffvelrnd φ B L W
75 23 74 sselid φ B L Word I × 2 𝑜
76 lencl B L Word I × 2 𝑜 B L 0
77 75 76 syl φ B L 0
78 77 47 eleqtrdi φ B L 0
79 eluzfz2 B L 0 B L 0 B L
80 78 79 syl φ B L 0 B L
81 ccatpfx B L Word I × 2 𝑜 Q 0 B L B L 0 B L B L prefix Q ++ B L substr Q B L = B L prefix B L
82 75 15 80 81 syl3anc φ B L prefix Q ++ B L substr Q B L = B L prefix B L
83 pfxid B L Word I × 2 𝑜 B L prefix B L = B L
84 75 83 syl φ B L prefix B L = B L
85 82 84 eqtrd φ B L prefix Q ++ B L substr Q B L = B L
86 55 85 eqeq12d φ 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 φ ¬ 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 W P 0 A K U I × 2 𝑜 P T A K U = A K splice P P ⟨“ U M U ”⟩
89 43 14 16 88 syl3anc φ P T A K U = A K splice P P ⟨“ U M U ”⟩
90 3 efgmf M : I × 2 𝑜 I × 2 𝑜
91 90 ffvelrni U I × 2 𝑜 M U I × 2 𝑜
92 16 91 syl φ M U I × 2 𝑜
93 16 92 s2cld φ ⟨“ U M U ”⟩ Word I × 2 𝑜
94 splval A K W P 0 A K P 0 A K ⟨“ U M U ”⟩ Word I × 2 𝑜 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 φ 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 φ S A = A K prefix P ++ ⟨“ U M U ”⟩ ++ A K substr P A K
97 1 2 3 4 efgtval B L W Q 0 B L V I × 2 𝑜 Q T B L V = B L splice Q Q ⟨“ V M V ”⟩
98 74 15 17 97 syl3anc φ Q T B L V = B L splice Q Q ⟨“ V M V ”⟩
99 90 ffvelrni V I × 2 𝑜 M V I × 2 𝑜
100 17 99 syl φ M V I × 2 𝑜
101 17 100 s2cld φ ⟨“ V M V ”⟩ Word I × 2 𝑜
102 splval B L W Q 0 B L Q 0 B L ⟨“ V M V ”⟩ Word I × 2 𝑜 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 φ 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 φ S B = B L prefix Q ++ ⟨“ V M V ”⟩ ++ B L substr Q B L
105 10 96 104 3eqtr3d φ 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 φ 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 Word I × 2 𝑜 A K prefix P Word I × 2 𝑜
108 44 107 syl φ A K prefix P Word I × 2 𝑜
109 108 adantr φ P = Q A K prefix P Word I × 2 𝑜
110 93 adantr φ P = Q ⟨“ U M U ”⟩ Word I × 2 𝑜
111 ccatcl A K prefix P Word I × 2 𝑜 ⟨“ U M U ”⟩ Word I × 2 𝑜 A K prefix P ++ ⟨“ U M U ”⟩ Word I × 2 𝑜
112 109 110 111 syl2anc φ P = Q A K prefix P ++ ⟨“ U M U ”⟩ Word I × 2 𝑜
113 swrdcl A K Word I × 2 𝑜 A K substr P A K Word I × 2 𝑜
114 44 113 syl φ A K substr P A K Word I × 2 𝑜
115 114 adantr φ P = Q A K substr P A K Word I × 2 𝑜
116 pfxcl B L Word I × 2 𝑜 B L prefix Q Word I × 2 𝑜
117 75 116 syl φ B L prefix Q Word I × 2 𝑜
118 117 adantr φ P = Q B L prefix Q Word I × 2 𝑜
119 101 adantr φ P = Q ⟨“ V M V ”⟩ Word I × 2 𝑜
120 ccatcl B L prefix Q Word I × 2 𝑜 ⟨“ V M V ”⟩ Word I × 2 𝑜 B L prefix Q ++ ⟨“ V M V ”⟩ Word I × 2 𝑜
121 118 119 120 syl2anc φ P = Q B L prefix Q ++ ⟨“ V M V ”⟩ Word I × 2 𝑜
122 swrdcl B L Word I × 2 𝑜 B L substr Q B L Word I × 2 𝑜
123 75 122 syl φ B L substr Q B L Word I × 2 𝑜
124 123 adantr φ P = Q B L substr Q B L Word I × 2 𝑜
125 pfxlen A K Word I × 2 𝑜 P 0 A K A K prefix P = P
126 44 14 125 syl2anc φ A K prefix P = P
127 pfxlen B L Word I × 2 𝑜 Q 0 B L B L prefix Q = Q
128 75 15 127 syl2anc φ B L prefix Q = Q
129 126 128 eqeq12d φ A K prefix P = B L prefix Q P = Q
130 129 biimpar φ 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 φ P = Q ⟨“ U M U ”⟩ = ⟨“ V M V ”⟩
135 130 134 oveq12d φ P = Q A K prefix P + ⟨“ U M U ”⟩ = B L prefix Q + ⟨“ V M V ”⟩
136 ccatlen A K prefix P Word I × 2 𝑜 ⟨“ U M U ”⟩ Word I × 2 𝑜 A K prefix P ++ ⟨“ U M U ”⟩ = A K prefix P + ⟨“ U M U ”⟩
137 109 110 136 syl2anc φ P = Q A K prefix P ++ ⟨“ U M U ”⟩ = A K prefix P + ⟨“ U M U ”⟩
138 ccatlen B L prefix Q Word I × 2 𝑜 ⟨“ V M V ”⟩ Word I × 2 𝑜 B L prefix Q ++ ⟨“ V M V ”⟩ = B L prefix Q + ⟨“ V M V ”⟩
139 118 119 138 syl2anc φ P = Q B L prefix Q ++ ⟨“ V M V ”⟩ = B L prefix Q + ⟨“ V M V ”⟩
140 135 137 139 3eqtr4d φ 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 ”⟩ Word I × 2 𝑜 A K substr P A K Word I × 2 𝑜 B L prefix Q ++ ⟨“ V M V ”⟩ Word I × 2 𝑜 B L substr Q B L Word I × 2 𝑜 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 φ 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 φ 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 φ P = Q A K prefix P ++ ⟨“ U M U ”⟩ = B L prefix Q ++ ⟨“ V M V ”⟩
145 ccatopth A K prefix P Word I × 2 𝑜 ⟨“ U M U ”⟩ Word I × 2 𝑜 B L prefix Q Word I × 2 𝑜 ⟨“ V M V ”⟩ Word I × 2 𝑜 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 φ 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 φ P = Q A K prefix P = B L prefix Q ⟨“ U M U ”⟩ = ⟨“ V M V ”⟩
148 147 simpld φ P = Q A K prefix P = B L prefix Q
149 143 simprd φ P = Q A K substr P A K = B L substr Q B L
150 148 149 oveq12d φ 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 φ ¬ P = Q
152 151 pm2.21d φ P = Q A 0 = B 0
153 uzp1 P Q + 1 P = Q + 1 P Q + 1 + 1
154 16 s1cld φ ⟨“ U ”⟩ Word I × 2 𝑜
155 ccatcl A K prefix P Word I × 2 𝑜 ⟨“ U ”⟩ Word I × 2 𝑜 A K prefix P ++ ⟨“ U ”⟩ Word I × 2 𝑜
156 108 154 155 syl2anc φ A K prefix P ++ ⟨“ U ”⟩ Word I × 2 𝑜
157 92 s1cld φ ⟨“ M U ”⟩ Word I × 2 𝑜
158 ccatass A K prefix P ++ ⟨“ U ”⟩ Word I × 2 𝑜 ⟨“ M U ”⟩ Word I × 2 𝑜 A K substr P A K Word I × 2 𝑜 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 φ 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 Word I × 2 𝑜 ⟨“ U ”⟩ Word I × 2 𝑜 ⟨“ M U ”⟩ Word I × 2 𝑜 A K prefix P ++ ⟨“ U ”⟩ ++ ⟨“ M U ”⟩ = A K prefix P ++ ⟨“ U ”⟩ ++ ⟨“ M U ”⟩
161 108 154 157 160 syl3anc φ 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 φ A K prefix P ++ ⟨“ U ”⟩ ++ ⟨“ M U ”⟩ = A K prefix P ++ ⟨“ U M U ”⟩
165 164 oveq1d φ 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 φ ⟨“ V ”⟩ Word I × 2 𝑜
167 100 s1cld φ ⟨“ M V ”⟩ Word I × 2 𝑜
168 ccatass B L prefix Q Word I × 2 𝑜 ⟨“ V ”⟩ Word I × 2 𝑜 ⟨“ M V ”⟩ Word I × 2 𝑜 B L prefix Q ++ ⟨“ V ”⟩ ++ ⟨“ M V ”⟩ = B L prefix Q ++ ⟨“ V ”⟩ ++ ⟨“ M V ”⟩
169 117 166 167 168 syl3anc φ 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 φ B L prefix Q ++ ⟨“ V ”⟩ ++ ⟨“ M V ”⟩ = B L prefix Q ++ ⟨“ V M V ”⟩
173 172 oveq1d φ 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 φ 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 φ 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 φ 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 φ P = Q + 1 A K prefix P ++ ⟨“ U ”⟩ Word I × 2 𝑜
178 157 adantr φ P = Q + 1 ⟨“ M U ”⟩ Word I × 2 𝑜
179 114 adantr φ P = Q + 1 A K substr P A K Word I × 2 𝑜
180 ccatcl ⟨“ M U ”⟩ Word I × 2 𝑜 A K substr P A K Word I × 2 𝑜 ⟨“ M U ”⟩ ++ A K substr P A K Word I × 2 𝑜
181 178 179 180 syl2anc φ P = Q + 1 ⟨“ M U ”⟩ ++ A K substr P A K Word I × 2 𝑜
182 ccatcl B L prefix Q Word I × 2 𝑜 ⟨“ V ”⟩ Word I × 2 𝑜 B L prefix Q ++ ⟨“ V ”⟩ Word I × 2 𝑜
183 117 166 182 syl2anc φ B L prefix Q ++ ⟨“ V ”⟩ Word I × 2 𝑜
184 183 adantr φ P = Q + 1 B L prefix Q ++ ⟨“ V ”⟩ Word I × 2 𝑜
185 167 adantr φ P = Q + 1 ⟨“ M V ”⟩ Word I × 2 𝑜
186 ccatcl B L prefix Q ++ ⟨“ V ”⟩ Word I × 2 𝑜 ⟨“ M V ”⟩ Word I × 2 𝑜 B L prefix Q ++ ⟨“ V ”⟩ ++ ⟨“ M V ”⟩ Word I × 2 𝑜
187 184 185 186 syl2anc φ P = Q + 1 B L prefix Q ++ ⟨“ V ”⟩ ++ ⟨“ M V ”⟩ Word I × 2 𝑜
188 123 adantr φ P = Q + 1 B L substr Q B L Word I × 2 𝑜
189 ccatlen B L prefix Q Word I × 2 𝑜 ⟨“ V ”⟩ Word I × 2 𝑜 B L prefix Q ++ ⟨“ V ”⟩ = B L prefix Q + ⟨“ V ”⟩
190 117 166 189 syl2anc φ B L prefix Q ++ ⟨“ V ”⟩ = B L prefix Q + ⟨“ V ”⟩
191 s1len ⟨“ V ”⟩ = 1
192 191 a1i φ ⟨“ V ”⟩ = 1
193 128 192 oveq12d φ B L prefix Q + ⟨“ V ”⟩ = Q + 1
194 190 193 eqtrd φ B L prefix Q ++ ⟨“ V ”⟩ = Q + 1
195 126 194 eqeq12d φ A K prefix P = B L prefix Q ++ ⟨“ V ”⟩ P = Q + 1
196 195 biimpar φ 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 φ P = Q + 1 ⟨“ U ”⟩ = ⟨“ M V ”⟩
201 196 200 oveq12d φ P = Q + 1 A K prefix P + ⟨“ U ”⟩ = B L prefix Q ++ ⟨“ V ”⟩ + ⟨“ M V ”⟩
202 108 adantr φ P = Q + 1 A K prefix P Word I × 2 𝑜
203 154 adantr φ P = Q + 1 ⟨“ U ”⟩ Word I × 2 𝑜
204 ccatlen A K prefix P Word I × 2 𝑜 ⟨“ U ”⟩ Word I × 2 𝑜 A K prefix P ++ ⟨“ U ”⟩ = A K prefix P + ⟨“ U ”⟩
205 202 203 204 syl2anc φ P = Q + 1 A K prefix P ++ ⟨“ U ”⟩ = A K prefix P + ⟨“ U ”⟩
206 ccatlen B L prefix Q ++ ⟨“ V ”⟩ Word I × 2 𝑜 ⟨“ M V ”⟩ Word I × 2 𝑜 B L prefix Q ++ ⟨“ V ”⟩ ++ ⟨“ M V ”⟩ = B L prefix Q ++ ⟨“ V ”⟩ + ⟨“ M V ”⟩
207 184 185 206 syl2anc φ P = Q + 1 B L prefix Q ++ ⟨“ V ”⟩ ++ ⟨“ M V ”⟩ = B L prefix Q ++ ⟨“ V ”⟩ + ⟨“ M V ”⟩
208 201 205 207 3eqtr4d φ P = Q + 1 A K prefix P ++ ⟨“ U ”⟩ = B L prefix Q ++ ⟨“ V ”⟩ ++ ⟨“ M V ”⟩
209 ccatopth A K prefix P ++ ⟨“ U ”⟩ Word I × 2 𝑜 ⟨“ M U ”⟩ ++ A K substr P A K Word I × 2 𝑜 B L prefix Q ++ ⟨“ V ”⟩ ++ ⟨“ M V ”⟩ Word I × 2 𝑜 B L substr Q B L Word I × 2 𝑜 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 φ 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 φ 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 φ P = Q + 1 A K prefix P ++ ⟨“ U ”⟩ = B L prefix Q ++ ⟨“ V ”⟩ ++ ⟨“ M V ”⟩
213 ccatopth A K prefix P Word I × 2 𝑜 ⟨“ U ”⟩ Word I × 2 𝑜 B L prefix Q ++ ⟨“ V ”⟩ Word I × 2 𝑜 ⟨“ M V ”⟩ Word I × 2 𝑜 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 φ 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 φ P = Q + 1 A K prefix P = B L prefix Q ++ ⟨“ V ”⟩ ⟨“ U ”⟩ = ⟨“ M V ”⟩
216 215 simpld φ P = Q + 1 A K prefix P = B L prefix Q ++ ⟨“ V ”⟩
217 216 oveq1d φ 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 φ P = Q + 1 B L prefix Q Word I × 2 𝑜
219 166 adantr φ P = Q + 1 ⟨“ V ”⟩ Word I × 2 𝑜
220 ccatass B L prefix Q Word I × 2 𝑜 ⟨“ V ”⟩ Word I × 2 𝑜 A K substr P A K Word I × 2 𝑜 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 φ 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 φ P = Q + 1 ⟨“ U ”⟩ = ⟨“ M V ”⟩
223 s111 U I × 2 𝑜 M V I × 2 𝑜 ⟨“ U ”⟩ = ⟨“ M V ”⟩ U = M V
224 16 100 223 syl2anc φ ⟨“ U ”⟩ = ⟨“ M V ”⟩ U = M V
225 224 adantr φ P = Q + 1 ⟨“ U ”⟩ = ⟨“ M V ”⟩ U = M V
226 222 225 mpbid φ P = Q + 1 U = M V
227 226 fveq2d φ P = Q + 1 M U = M M V
228 3 efgmnvl V I × 2 𝑜 M M V = V
229 17 228 syl φ M M V = V
230 229 adantr φ P = Q + 1 M M V = V
231 227 230 eqtrd φ P = Q + 1 M U = V
232 231 s1eqd φ P = Q + 1 ⟨“ M U ”⟩ = ⟨“ V ”⟩
233 232 oveq1d φ P = Q + 1 ⟨“ M U ”⟩ ++ A K substr P A K = ⟨“ V ”⟩ ++ A K substr P A K
234 211 simprd φ P = Q + 1 ⟨“ M U ”⟩ ++ A K substr P A K = B L substr Q B L
235 233 234 eqtr3d φ P = Q + 1 ⟨“ V ”⟩ ++ A K substr P A K = B L substr Q B L
236 235 oveq2d φ 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 φ 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 φ ¬ P = Q + 1
239 238 pm2.21d φ P = Q + 1 A 0 = B 0
240 15 elfzelzd φ Q
241 240 zcnd φ Q
242 1cnd φ 1
243 241 242 242 addassd φ Q + 1 + 1 = Q + 1 + 1
244 df-2 2 = 1 + 1
245 244 oveq2i Q + 2 = Q + 1 + 1
246 243 245 eqtr4di φ Q + 1 + 1 = Q + 2
247 246 fveq2d φ Q + 1 + 1 = Q + 2
248 247 eleq2d φ P Q + 1 + 1 P Q + 2
249 1 2 3 4 5 6 efgsfo S : dom S onto W
250 swrdcl A K Word I × 2 𝑜 A K substr Q + 2 A K Word I × 2 𝑜
251 44 250 syl φ A K substr Q + 2 A K Word I × 2 𝑜
252 ccatcl B L prefix Q Word I × 2 𝑜 A K substr Q + 2 A K Word I × 2 𝑜 B L prefix Q ++ A K substr Q + 2 A K Word I × 2 𝑜
253 117 251 252 syl2anc φ B L prefix Q ++ A K substr Q + 2 A K Word I × 2 𝑜
254 1 efgrcl A K W I V W = Word I × 2 𝑜
255 43 254 syl φ I V W = Word I × 2 𝑜
256 255 simprd φ W = Word I × 2 𝑜
257 253 256 eleqtrrd φ B L prefix Q ++ A K substr Q + 2 A K W
258 foelrn S : dom S onto W B L prefix Q ++ A K substr Q + 2 A K W c dom S B L prefix Q ++ A K substr Q + 2 A K = S c
259 249 257 258 sylancr φ c dom S B L prefix Q ++ A K substr Q + 2 A K = S c
260 259 adantr φ P Q + 2 c dom S B L prefix Q ++ A K substr Q + 2 A K = S c
261 7 ad2antrr φ P Q + 2 c dom S B L prefix Q ++ A K substr Q + 2 A K = S c a dom S b dom S S a < S A S a = S b a 0 = b 0
262 8 ad2antrr φ P Q + 2 c dom S B L prefix Q ++ A K substr Q + 2 A K = S c A dom S
263 9 ad2antrr φ P Q + 2 c dom S B L prefix Q ++ A K substr Q + 2 A K = S c B dom S
264 10 ad2antrr φ P Q + 2 c dom S B L prefix Q ++ A K substr Q + 2 A K = S c S A = S B
265 11 ad2antrr φ P Q + 2 c dom S B L prefix Q ++ A K substr Q + 2 A K = S c ¬ A 0 = B 0
266 14 ad2antrr φ P Q + 2 c dom S B L prefix Q ++ A K substr Q + 2 A K = S c P 0 A K
267 15 ad2antrr φ P Q + 2 c dom S B L prefix Q ++ A K substr Q + 2 A K = S c Q 0 B L
268 16 ad2antrr φ P Q + 2 c dom S B L prefix Q ++ A K substr Q + 2 A K = S c U I × 2 𝑜
269 17 ad2antrr φ P Q + 2 c dom S B L prefix Q ++ A K substr Q + 2 A K = S c V I × 2 𝑜
270 18 ad2antrr φ P Q + 2 c 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 φ P Q + 2 c 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 φ P Q + 2 c dom S B L prefix Q ++ A K substr Q + 2 A K = S c ¬ A K = B L
273 simplr φ P Q + 2 c dom S B L prefix Q ++ A K substr Q + 2 A K = S c P Q + 2
274 simprl φ P Q + 2 c dom S B L prefix Q ++ A K substr Q + 2 A K = S c c dom S
275 simprr φ P Q + 2 c 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 φ P Q + 2 c 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 φ P Q + 2 c dom S B L prefix Q ++ A K substr Q + 2 A K = S c A 0 = B 0
278 260 277 rexlimddv φ P Q + 2 A 0 = B 0
279 278 ex φ P Q + 2 A 0 = B 0
280 248 279 sylbid φ P Q + 1 + 1 A 0 = B 0
281 239 280 jaod φ P = Q + 1 P Q + 1 + 1 A 0 = B 0
282 153 281 syl5 φ P Q + 1 A 0 = B 0
283 152 282 jaod φ P = Q P Q + 1 A 0 = B 0
284 21 283 syl5 φ P Q A 0 = B 0