Metamath Proof Explorer


Theorem efgredlemd

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
efgredlemd.9 φ P Q + 2
efgredlemd.c φ C dom S
efgredlemd.sc φ S C = B L prefix Q ++ A K substr Q + 2 A K
Assertion efgredlemd φ 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 efgredlemd.9 φ P Q + 2
22 efgredlemd.c φ C dom S
23 efgredlemd.sc φ S C = B L prefix Q ++ A K substr Q + 2 A K
24 1 2 3 4 5 6 efgsdm C dom S C Word W C 0 D i 1 ..^ C C i ran T C i 1
25 24 simp1bi C dom S C Word W
26 22 25 syl φ C Word W
27 26 eldifad φ C Word W
28 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
29 28 simp1bi A dom S A Word W
30 8 29 syl φ A Word W
31 30 eldifad φ A Word W
32 wrdf A Word W A : 0 ..^ A W
33 31 32 syl φ A : 0 ..^ A W
34 fzossfz 0 ..^ A 1 0 A 1
35 lencl A Word W A 0
36 31 35 syl φ A 0
37 36 nn0zd φ A
38 fzoval A 0 ..^ A = 0 A 1
39 37 38 syl φ 0 ..^ A = 0 A 1
40 34 39 sseqtrrid φ 0 ..^ A 1 0 ..^ A
41 1 2 3 4 5 6 7 8 9 10 11 efgredlema φ A 1 B 1
42 41 simpld φ A 1
43 fzo0end A 1 A - 1 - 1 0 ..^ A 1
44 42 43 syl φ A - 1 - 1 0 ..^ A 1
45 12 44 eqeltrid φ K 0 ..^ A 1
46 40 45 sseldd φ K 0 ..^ A
47 33 46 ffvelrnd φ A K W
48 47 s1cld φ ⟨“ A K ”⟩ Word W
49 eldifsn C Word W C Word W C
50 lennncl C Word W C C
51 49 50 sylbi C Word W C
52 26 51 syl φ C
53 lbfzo0 0 0 ..^ C C
54 52 53 sylibr φ 0 0 ..^ C
55 ccatval1 C Word W ⟨“ A K ”⟩ Word W 0 0 ..^ C C ++ ⟨“ A K ”⟩ 0 = C 0
56 27 48 54 55 syl3anc φ C ++ ⟨“ A K ”⟩ 0 = C 0
57 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
58 57 simp1bi B dom S B Word W
59 9 58 syl φ B Word W
60 59 eldifad φ B Word W
61 wrdf B Word W B : 0 ..^ B W
62 60 61 syl φ B : 0 ..^ B W
63 fzossfz 0 ..^ B 1 0 B 1
64 lencl B Word W B 0
65 60 64 syl φ B 0
66 65 nn0zd φ B
67 fzoval B 0 ..^ B = 0 B 1
68 66 67 syl φ 0 ..^ B = 0 B 1
69 63 68 sseqtrrid φ 0 ..^ B 1 0 ..^ B
70 41 simprd φ B 1
71 fzo0end B 1 B - 1 - 1 0 ..^ B 1
72 70 71 syl φ B - 1 - 1 0 ..^ B 1
73 13 72 eqeltrid φ L 0 ..^ B 1
74 69 73 sseldd φ L 0 ..^ B
75 62 74 ffvelrnd φ B L W
76 75 s1cld φ ⟨“ B L ”⟩ Word W
77 ccatval1 C Word W ⟨“ B L ”⟩ Word W 0 0 ..^ C C ++ ⟨“ B L ”⟩ 0 = C 0
78 27 76 54 77 syl3anc φ C ++ ⟨“ B L ”⟩ 0 = C 0
79 56 78 eqtr4d φ C ++ ⟨“ A K ”⟩ 0 = C ++ ⟨“ B L ”⟩ 0
80 fviss I Word I × 2 𝑜 Word I × 2 𝑜
81 1 80 eqsstri W Word I × 2 𝑜
82 81 47 sseldi φ A K Word I × 2 𝑜
83 lencl A K Word I × 2 𝑜 A K 0
84 82 83 syl φ A K 0
85 84 nn0red φ A K
86 2rp 2 +
87 ltaddrp A K 2 + A K < A K + 2
88 85 86 87 sylancl φ A K < A K + 2
89 36 nn0red φ A
90 89 lem1d φ A 1 A
91 fznn A A 1 1 A A 1 A 1 A
92 37 91 syl φ A 1 1 A A 1 A 1 A
93 42 90 92 mpbir2and φ A 1 1 A
94 1 2 3 4 5 6 efgsres A dom S A 1 1 A A 0 ..^ A 1 dom S
95 8 93 94 syl2anc φ A 0 ..^ A 1 dom S
96 1 2 3 4 5 6 efgsval A 0 ..^ A 1 dom S S A 0 ..^ A 1 = A 0 ..^ A 1 A 0 ..^ A 1 1
97 95 96 syl φ S A 0 ..^ A 1 = A 0 ..^ A 1 A 0 ..^ A 1 1
98 fz1ssfz0 1 A 0 A
99 98 93 sseldi φ A 1 0 A
100 pfxres A Word W A 1 0 A A prefix A 1 = A 0 ..^ A 1
101 31 99 100 syl2anc φ A prefix A 1 = A 0 ..^ A 1
102 101 fveq2d φ A prefix A 1 = A 0 ..^ A 1
103 pfxlen A Word W A 1 0 A A prefix A 1 = A 1
104 31 99 103 syl2anc φ A prefix A 1 = A 1
105 102 104 eqtr3d φ A 0 ..^ A 1 = A 1
106 105 oveq1d φ A 0 ..^ A 1 1 = A - 1 - 1
107 106 12 eqtr4di φ A 0 ..^ A 1 1 = K
108 107 fveq2d φ A 0 ..^ A 1 A 0 ..^ A 1 1 = A 0 ..^ A 1 K
109 45 fvresd φ A 0 ..^ A 1 K = A K
110 97 108 109 3eqtrd φ S A 0 ..^ A 1 = A K
111 110 fveq2d φ S A 0 ..^ A 1 = A K
112 1 2 3 4 5 6 efgsdmi A dom S A 1 S A ran T A A - 1 - 1
113 8 42 112 syl2anc φ S A ran T A A - 1 - 1
114 12 fveq2i A K = A A - 1 - 1
115 114 fveq2i T A K = T A A - 1 - 1
116 115 rneqi ran T A K = ran T A A - 1 - 1
117 113 116 eleqtrrdi φ S A ran T A K
118 1 2 3 4 efgtlen A K W S A ran T A K S A = A K + 2
119 47 117 118 syl2anc φ S A = A K + 2
120 88 111 119 3brtr4d φ S A 0 ..^ A 1 < S A
121 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 efgredleme φ A K ran T S C B L ran T S C
122 121 simpld φ A K ran T S C
123 1 2 3 4 5 6 efgsp1 C dom S A K ran T S C C ++ ⟨“ A K ”⟩ dom S
124 22 122 123 syl2anc φ C ++ ⟨“ A K ”⟩ dom S
125 1 2 3 4 5 6 efgsval2 C Word W A K W C ++ ⟨“ A K ”⟩ dom S S C ++ ⟨“ A K ”⟩ = A K
126 27 47 124 125 syl3anc φ S C ++ ⟨“ A K ”⟩ = A K
127 110 126 eqtr4d φ S A 0 ..^ A 1 = S C ++ ⟨“ A K ”⟩
128 2fveq3 a = A 0 ..^ A 1 S a = S A 0 ..^ A 1
129 128 breq1d a = A 0 ..^ A 1 S a < S A S A 0 ..^ A 1 < S A
130 fveqeq2 a = A 0 ..^ A 1 S a = S b S A 0 ..^ A 1 = S b
131 fveq1 a = A 0 ..^ A 1 a 0 = A 0 ..^ A 1 0
132 131 eqeq1d a = A 0 ..^ A 1 a 0 = b 0 A 0 ..^ A 1 0 = b 0
133 130 132 imbi12d a = A 0 ..^ A 1 S a = S b a 0 = b 0 S A 0 ..^ A 1 = S b A 0 ..^ A 1 0 = b 0
134 129 133 imbi12d a = A 0 ..^ A 1 S a < S A S a = S b a 0 = b 0 S A 0 ..^ A 1 < S A S A 0 ..^ A 1 = S b A 0 ..^ A 1 0 = b 0
135 fveq2 b = C ++ ⟨“ A K ”⟩ S b = S C ++ ⟨“ A K ”⟩
136 135 eqeq2d b = C ++ ⟨“ A K ”⟩ S A 0 ..^ A 1 = S b S A 0 ..^ A 1 = S C ++ ⟨“ A K ”⟩
137 fveq1 b = C ++ ⟨“ A K ”⟩ b 0 = C ++ ⟨“ A K ”⟩ 0
138 137 eqeq2d b = C ++ ⟨“ A K ”⟩ A 0 ..^ A 1 0 = b 0 A 0 ..^ A 1 0 = C ++ ⟨“ A K ”⟩ 0
139 136 138 imbi12d b = C ++ ⟨“ A K ”⟩ S A 0 ..^ A 1 = S b A 0 ..^ A 1 0 = b 0 S A 0 ..^ A 1 = S C ++ ⟨“ A K ”⟩ A 0 ..^ A 1 0 = C ++ ⟨“ A K ”⟩ 0
140 139 imbi2d b = C ++ ⟨“ A K ”⟩ S A 0 ..^ A 1 < S A S A 0 ..^ A 1 = S b A 0 ..^ A 1 0 = b 0 S A 0 ..^ A 1 < S A S A 0 ..^ A 1 = S C ++ ⟨“ A K ”⟩ A 0 ..^ A 1 0 = C ++ ⟨“ A K ”⟩ 0
141 134 140 rspc2va A 0 ..^ A 1 dom S C ++ ⟨“ A K ”⟩ dom S a dom S b dom S S a < S A S a = S b a 0 = b 0 S A 0 ..^ A 1 < S A S A 0 ..^ A 1 = S C ++ ⟨“ A K ”⟩ A 0 ..^ A 1 0 = C ++ ⟨“ A K ”⟩ 0
142 95 124 7 141 syl21anc φ S A 0 ..^ A 1 < S A S A 0 ..^ A 1 = S C ++ ⟨“ A K ”⟩ A 0 ..^ A 1 0 = C ++ ⟨“ A K ”⟩ 0
143 120 127 142 mp2d φ A 0 ..^ A 1 0 = C ++ ⟨“ A K ”⟩ 0
144 81 75 sseldi φ B L Word I × 2 𝑜
145 lencl B L Word I × 2 𝑜 B L 0
146 144 145 syl φ B L 0
147 146 nn0red φ B L
148 ltaddrp B L 2 + B L < B L + 2
149 147 86 148 sylancl φ B L < B L + 2
150 65 nn0red φ B
151 150 lem1d φ B 1 B
152 fznn B B 1 1 B B 1 B 1 B
153 66 152 syl φ B 1 1 B B 1 B 1 B
154 70 151 153 mpbir2and φ B 1 1 B
155 1 2 3 4 5 6 efgsres B dom S B 1 1 B B 0 ..^ B 1 dom S
156 9 154 155 syl2anc φ B 0 ..^ B 1 dom S
157 1 2 3 4 5 6 efgsval B 0 ..^ B 1 dom S S B 0 ..^ B 1 = B 0 ..^ B 1 B 0 ..^ B 1 1
158 156 157 syl φ S B 0 ..^ B 1 = B 0 ..^ B 1 B 0 ..^ B 1 1
159 fz1ssfz0 1 B 0 B
160 159 154 sseldi φ B 1 0 B
161 pfxres B Word W B 1 0 B B prefix B 1 = B 0 ..^ B 1
162 60 160 161 syl2anc φ B prefix B 1 = B 0 ..^ B 1
163 162 fveq2d φ B prefix B 1 = B 0 ..^ B 1
164 pfxlen B Word W B 1 0 B B prefix B 1 = B 1
165 60 160 164 syl2anc φ B prefix B 1 = B 1
166 163 165 eqtr3d φ B 0 ..^ B 1 = B 1
167 166 oveq1d φ B 0 ..^ B 1 1 = B - 1 - 1
168 167 13 eqtr4di φ B 0 ..^ B 1 1 = L
169 168 fveq2d φ B 0 ..^ B 1 B 0 ..^ B 1 1 = B 0 ..^ B 1 L
170 73 fvresd φ B 0 ..^ B 1 L = B L
171 158 169 170 3eqtrd φ S B 0 ..^ B 1 = B L
172 171 fveq2d φ S B 0 ..^ B 1 = B L
173 1 2 3 4 5 6 efgsdmi B dom S B 1 S B ran T B B - 1 - 1
174 9 70 173 syl2anc φ S B ran T B B - 1 - 1
175 10 174 eqeltrd φ S A ran T B B - 1 - 1
176 13 fveq2i B L = B B - 1 - 1
177 176 fveq2i T B L = T B B - 1 - 1
178 177 rneqi ran T B L = ran T B B - 1 - 1
179 175 178 eleqtrrdi φ S A ran T B L
180 1 2 3 4 efgtlen B L W S A ran T B L S A = B L + 2
181 75 179 180 syl2anc φ S A = B L + 2
182 149 172 181 3brtr4d φ S B 0 ..^ B 1 < S A
183 121 simprd φ B L ran T S C
184 1 2 3 4 5 6 efgsp1 C dom S B L ran T S C C ++ ⟨“ B L ”⟩ dom S
185 22 183 184 syl2anc φ C ++ ⟨“ B L ”⟩ dom S
186 1 2 3 4 5 6 efgsval2 C Word W B L W C ++ ⟨“ B L ”⟩ dom S S C ++ ⟨“ B L ”⟩ = B L
187 27 75 185 186 syl3anc φ S C ++ ⟨“ B L ”⟩ = B L
188 171 187 eqtr4d φ S B 0 ..^ B 1 = S C ++ ⟨“ B L ”⟩
189 2fveq3 a = B 0 ..^ B 1 S a = S B 0 ..^ B 1
190 189 breq1d a = B 0 ..^ B 1 S a < S A S B 0 ..^ B 1 < S A
191 fveqeq2 a = B 0 ..^ B 1 S a = S b S B 0 ..^ B 1 = S b
192 fveq1 a = B 0 ..^ B 1 a 0 = B 0 ..^ B 1 0
193 192 eqeq1d a = B 0 ..^ B 1 a 0 = b 0 B 0 ..^ B 1 0 = b 0
194 191 193 imbi12d a = B 0 ..^ B 1 S a = S b a 0 = b 0 S B 0 ..^ B 1 = S b B 0 ..^ B 1 0 = b 0
195 190 194 imbi12d a = B 0 ..^ B 1 S a < S A S a = S b a 0 = b 0 S B 0 ..^ B 1 < S A S B 0 ..^ B 1 = S b B 0 ..^ B 1 0 = b 0
196 fveq2 b = C ++ ⟨“ B L ”⟩ S b = S C ++ ⟨“ B L ”⟩
197 196 eqeq2d b = C ++ ⟨“ B L ”⟩ S B 0 ..^ B 1 = S b S B 0 ..^ B 1 = S C ++ ⟨“ B L ”⟩
198 fveq1 b = C ++ ⟨“ B L ”⟩ b 0 = C ++ ⟨“ B L ”⟩ 0
199 198 eqeq2d b = C ++ ⟨“ B L ”⟩ B 0 ..^ B 1 0 = b 0 B 0 ..^ B 1 0 = C ++ ⟨“ B L ”⟩ 0
200 197 199 imbi12d b = C ++ ⟨“ B L ”⟩ S B 0 ..^ B 1 = S b B 0 ..^ B 1 0 = b 0 S B 0 ..^ B 1 = S C ++ ⟨“ B L ”⟩ B 0 ..^ B 1 0 = C ++ ⟨“ B L ”⟩ 0
201 200 imbi2d b = C ++ ⟨“ B L ”⟩ S B 0 ..^ B 1 < S A S B 0 ..^ B 1 = S b B 0 ..^ B 1 0 = b 0 S B 0 ..^ B 1 < S A S B 0 ..^ B 1 = S C ++ ⟨“ B L ”⟩ B 0 ..^ B 1 0 = C ++ ⟨“ B L ”⟩ 0
202 195 201 rspc2va B 0 ..^ B 1 dom S C ++ ⟨“ B L ”⟩ dom S a dom S b dom S S a < S A S a = S b a 0 = b 0 S B 0 ..^ B 1 < S A S B 0 ..^ B 1 = S C ++ ⟨“ B L ”⟩ B 0 ..^ B 1 0 = C ++ ⟨“ B L ”⟩ 0
203 156 185 7 202 syl21anc φ S B 0 ..^ B 1 < S A S B 0 ..^ B 1 = S C ++ ⟨“ B L ”⟩ B 0 ..^ B 1 0 = C ++ ⟨“ B L ”⟩ 0
204 182 188 203 mp2d φ B 0 ..^ B 1 0 = C ++ ⟨“ B L ”⟩ 0
205 79 143 204 3eqtr4d φ A 0 ..^ A 1 0 = B 0 ..^ B 1 0
206 lbfzo0 0 0 ..^ A 1 A 1
207 42 206 sylibr φ 0 0 ..^ A 1
208 207 fvresd φ A 0 ..^ A 1 0 = A 0
209 lbfzo0 0 0 ..^ B 1 B 1
210 70 209 sylibr φ 0 0 ..^ B 1
211 210 fvresd φ B 0 ..^ B 1 0 = B 0
212 205 208 211 3eqtr3d φ A 0 = B 0