Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  wrd2ind Structured version   Visualization version   Unicode version

Theorem wrd2ind 12888
 Description: Perform induction over the structure of two words of the same length. (Contributed by AV, 23-Jan-2019.)
Hypotheses
Ref Expression
wrd2ind.1
wrd2ind.2
wrd2ind.3 ++ ++
wrd2ind.4
wrd2ind.5
wrd2ind.6
wrd2ind.7 Word Word
Assertion
Ref Expression
wrd2ind Word Word
Distinct variable groups:   ,,   ,,,,   ,,,,,,   ,,,,,,   ,,   ,,,,   ,   ,,   ,
Allowed substitution hints:   (,)   (,,,,,)   (,,,)   (,,,)   (,,,,)   (,,,,)   (,,,)   (,)

Proof of Theorem wrd2ind
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lencl 12737 . . . . 5 Word
2 eqeq2 2482 . . . . . . . . 9
32anbi2d 718 . . . . . . . 8
43imbi1d 324 . . . . . . 7
542ralbidv 2832 . . . . . 6 Word Word Word Word
6 eqeq2 2482 . . . . . . . . 9
76anbi2d 718 . . . . . . . 8
87imbi1d 324 . . . . . . 7
982ralbidv 2832 . . . . . 6 Word Word Word Word
10 eqeq2 2482 . . . . . . . . 9
1110anbi2d 718 . . . . . . . 8
1211imbi1d 324 . . . . . . 7
13122ralbidv 2832 . . . . . 6 Word Word Word Word
14 eqeq2 2482 . . . . . . . . 9
1514anbi2d 718 . . . . . . . 8
1615imbi1d 324 . . . . . . 7
17162ralbidv 2832 . . . . . 6 Word Word Word Word
18 eqeq1 2475 . . . . . . . . . . . 12
1918adantl 473 . . . . . . . . . . 11 Word Word
20 eqcom 2478 . . . . . . . . . . . . . . 15
21 hasheq0 12582 . . . . . . . . . . . . . . 15 Word
2220, 21syl5bb 265 . . . . . . . . . . . . . 14 Word
23 hasheq0 12582 . . . . . . . . . . . . . . . 16 Word
24 wrd2ind.6 . . . . . . . . . . . . . . . . . 18
25 wrd2ind.1 . . . . . . . . . . . . . . . . . 18
2624, 25mpbiri 241 . . . . . . . . . . . . . . . . 17
2726ex 441 . . . . . . . . . . . . . . . 16
2823, 27syl6bi 236 . . . . . . . . . . . . . . 15 Word
2928com13 82 . . . . . . . . . . . . . 14 Word
3022, 29syl6bi 236 . . . . . . . . . . . . 13 Word Word
3130com24 89 . . . . . . . . . . . 12 Word Word
3231imp31 439 . . . . . . . . . . 11 Word Word
3319, 32sylbid 223 . . . . . . . . . 10 Word Word
3433ex 441 . . . . . . . . 9 Word Word
3534com23 80 . . . . . . . 8 Word Word
3635impd 438 . . . . . . 7 Word Word
3736rgen2 2818 . . . . . 6 Word Word
38 fveq2 5879 . . . . . . . . . . . . 13
39 fveq2 5879 . . . . . . . . . . . . 13
4038, 39eqeqan12d 2487 . . . . . . . . . . . 12
4138eqeq1d 2473 . . . . . . . . . . . . 13
4241adantr 472 . . . . . . . . . . . 12
4340, 42anbi12d 725 . . . . . . . . . . 11
44 wrd2ind.2 . . . . . . . . . . 11
4543, 44imbi12d 327 . . . . . . . . . 10
4645ancoms 460 . . . . . . . . 9
4746cbvraldva 3011 . . . . . . . 8 Word Word
4847cbvralv 3005 . . . . . . 7 Word Word Word Word
49 swrdcl 12829 . . . . . . . . . . . . . . . . 17 Word substr Word
5049adantr 472 . . . . . . . . . . . . . . . 16 Word Word substr Word
5150ad2antrl 742 . . . . . . . . . . . . . . 15 Word Word substr Word
52 simprll 780 . . . . . . . . . . . . . . . 16 Word Word Word
53 eqeq1 2475 . . . . . . . . . . . . . . . . . . . . . 22
54 nn0p1nn 10933 . . . . . . . . . . . . . . . . . . . . . . 23
55 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . 24
5655eqcoms 2479 . . . . . . . . . . . . . . . . . . . . . . 23
5754, 56syl5ibr 229 . . . . . . . . . . . . . . . . . . . . . 22
5853, 57syl6bi 236 . . . . . . . . . . . . . . . . . . . . 21
5958impcom 437 . . . . . . . . . . . . . . . . . . . 20
6059adantl 473 . . . . . . . . . . . . . . . . . . 19 Word Word
6160impcom 437 . . . . . . . . . . . . . . . . . 18 Word Word
6261nnge1d 10674 . . . . . . . . . . . . . . . . 17 Word Word
63 wrdlenge1n0 12753 . . . . . . . . . . . . . . . . . 18 Word
6452, 63syl 17 . . . . . . . . . . . . . . . . 17 Word Word
6562, 64mpbird 240 . . . . . . . . . . . . . . . 16 Word Word
66 lswcl 12766 . . . . . . . . . . . . . . . 16 Word lastS
6752, 65, 66syl2anc 673 . . . . . . . . . . . . . . 15 Word Word lastS
6851, 67jca 541 . . . . . . . . . . . . . 14 Word Word substr Word lastS
69 swrdcl 12829 . . . . . . . . . . . . . . . 16 Word substr Word
7069adantl 473 . . . . . . . . . . . . . . 15 Word Word substr Word
7170ad2antrl 742 . . . . . . . . . . . . . 14 Word Word substr Word
72 simprlr 781 . . . . . . . . . . . . . . 15 Word Word Word
73 eleq1 2537 . . . . . . . . . . . . . . . . . . . 20
7454, 73syl5ibr 229 . . . . . . . . . . . . . . . . . . 19
7574ad2antll 743 . . . . . . . . . . . . . . . . . 18 Word Word
7675impcom 437 . . . . . . . . . . . . . . . . 17 Word Word
7776nnge1d 10674 . . . . . . . . . . . . . . . 16 Word Word
78 wrdlenge1n0 12753 . . . . . . . . . . . . . . . . 17 Word
7972, 78syl 17 . . . . . . . . . . . . . . . 16 Word Word
8077, 79mpbird 240 . . . . . . . . . . . . . . 15 Word Word
81 lswcl 12766 . . . . . . . . . . . . . . 15 Word lastS
8272, 80, 81syl2anc 673 . . . . . . . . . . . . . 14 Word Word lastS
8368, 71, 82jca32 544 . . . . . . . . . . . . 13 Word Word substr Word lastS substr Word lastS
8483adantlr 729 . . . . . . . . . . . 12 Word Word Word Word substr Word lastS substr Word lastS
85 simprl 772 . . . . . . . . . . . . . 14 Word Word Word Word Word Word
86 simplr 770 . . . . . . . . . . . . . 14 Word Word Word Word Word Word
87 simprrl 782 . . . . . . . . . . . . . . . . 17 Word Word Word Word
8887oveq1d 6323 . . . . . . . . . . . . . . . 16 Word Word Word Word
89 simprlr 781 . . . . . . . . . . . . . . . . 17 Word Word Word Word Word
90 fzossfz 11965 . . . . . . . . . . . . . . . . . 18 ..^
91 simprrr 783 . . . . . . . . . . . . . . . . . . . 20 Word Word Word Word
9254ad2antrr 740 . . . . . . . . . . . . . . . . . . . 20 Word Word Word Word
9391, 92eqeltrd 2549 . . . . . . . . . . . . . . . . . . 19 Word Word Word Word
94 fzo0end 12032 . . . . . . . . . . . . . . . . . . 19 ..^
9593, 94syl 17 . . . . . . . . . . . . . . . . . 18 Word Word Word Word ..^
9690, 95sseldi 3416 . . . . . . . . . . . . . . . . 17 Word Word Word Word
97 swrd0len 12832 . . . . . . . . . . . . . . . . 17 Word substr
9889, 96, 97syl2anc 673 . . . . . . . . . . . . . . . 16 Word Word Word Word substr
99 simprll 780 . . . . . . . . . . . . . . . . 17 Word Word Word Word Word
100 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . 22
101 oveq2 6316 . . . . . . . . . . . . . . . . . . . . . 22
102100, 101eleq12d 2543 . . . . . . . . . . . . . . . . . . . . 21
103102eqcoms 2479 . . . . . . . . . . . . . . . . . . . 20
104103adantr 472 . . . . . . . . . . . . . . . . . . 19
105104ad2antll 743 . . . . . . . . . . . . . . . . . 18 Word Word Word Word
10696, 105mpbird 240 . . . . . . . . . . . . . . . . 17 Word Word Word Word
107 swrd0len 12832 . . . . . . . . . . . . . . . . 17 Word substr
10899, 106, 107syl2anc 673 . . . . . . . . . . . . . . . 16 Word Word Word Word substr
10988, 98, 1083eqtr4d 2515 . . . . . . . . . . . . . . 15 Word Word Word Word substr substr
11091oveq1d 6323 . . . . . . . . . . . . . . . 16 Word Word Word Word
111 nn0cn 10903 . . . . . . . . . . . . . . . . . 18
112111ad2antrr 740 . . . . . . . . . . . . . . . . 17 Word Word Word Word
113 ax-1cn 9615 . . . . . . . . . . . . . . . . 17
114 pncan 9901 . . . . . . . . . . . . . . . . 17
115112, 113, 114sylancl 675 . . . . . . . . . . . . . . . 16 Word Word Word Word
11698, 110, 1153eqtrd 2509 . . . . . . . . . . . . . . 15 Word Word Word Word substr
117109, 116jca 541 . . . . . . . . . . . . . 14 Word Word Word Word substr substr substr
11870adantr 472 . . . . . . . . . . . . . . . 16 Word Word substr substr Word
119 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . 22 substr substr
120 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . 22 substr substr
121119, 120eqeqan12d 2487 . . . . . . . . . . . . . . . . . . . . 21 substr substr substr substr
122121expcom 442 . . . . . . . . . . . . . . . . . . . 20 substr substr substr substr
123122adantl 473 . . . . . . . . . . . . . . . . . . 19 Word Word substr substr substr substr
124123imp 436 . . . . . . . . . . . . . . . . . 18 Word Word substr substr substr substr
125119eqeq1d 2473 . . . . . . . . . . . . . . . . . . 19 substr substr
126125adantl 473 . . . . . . . . . . . . . . . . . 18 Word Word substr substr substr
127124, 126anbi12d 725 . . . . . . . . . . . . . . . . 17 Word Word substr substr substr substr substr
128 vex 3034 . . . . . . . . . . . . . . . . . . . . 21
129 vex 3034 . . . . . . . . . . . . . . . . . . . . 21
130128, 129, 44sbc2ie 3323 . . . . . . . . . . . . . . . . . . . 20
131130bicomi 207 . . . . . . . . . . . . . . . . . . 19
132131a1i 11 . . . . . . . . . . . . . . . . . 18 Word Word substr substr
133 simpr 468 . . . . . . . . . . . . . . . . . . 19 Word Word substr substr substr
134133sbceq1d 3260 . . . . . . . . . . . . . . . . . 18 Word Word substr substr substr
135 dfsbcq 3257 . . . . . . . . . . . . . . . . . . . . 21 substr substr
136135sbcbidv 3310 . . . . . . . . . . . . . . . . . . . 20 substr substr substr substr
137136adantl 473 . . . . . . . . . . . . . . . . . . 19 Word Word substr substr substr substr
138137adantr 472 . . . . . . . . . . . . . . . . . 18 Word Word substr substr substr substr substr
139132, 134, 1383bitrd 287 . . . . . . . . . . . . . . . . 17 Word Word substr substr substr substr
140127, 139imbi12d 327 . . . . . . . . . . . . . . . 16 Word Word substr substr substr substr substr substr substr
141118, 140rspcdv 3139 . . . . . . . . . . . . . . 15 Word Word substr Word substr substr substr substr substr
14250, 141rspcimdv 3137 . . . . . . . . . . . . . 14 Word Word Word Word substr substr substr substr substr
14385, 86, 117, 142syl3c 62 . . . . . . . . . . . . 13 Word Word Word Word substr substr
144143, 109jca 541 . . . . . . . . . . . 12 Word Word Word Word substr substr substr substr
145 dfsbcq 3257 . . . . . . . . . . . . . . . 16 substr substr
146 sbccom 3327 . . . . . . . . . . . . . . . 16 substr substr
147145, 146syl6bb 269 . . . . . . . . . . . . . . 15 substr substr
148120eqeq2d 2481 . . . . . . . . . . . . . . 15 substr substr
149147, 148anbi12d 725 . . . . . . . . . . . . . 14 substr substr substr
150 oveq1 6315 . . . . . . . . . . . . . . 15 substr ++ substr ++
151150sbceq1d 3260 . . . . . . . . . . . . . 14 substr ++ ++ substr ++ ++
152149, 151imbi12d 327 . . . . . . . . . . . . 13 substr ++ ++ substr substr substr ++ ++
153 s1eq 12792 . . . . . . . . . . . . . . . . 17 lastS lastS
154153oveq2d 6324 . . . . . . . . . . . . . . . 16 lastS substr ++ substr ++ lastS
155154sbceq1d 3260 . . . . . . . . . . . . . . 15 lastS substr ++ ++ substr ++ lastS ++
156155imbi2d 323 . . . . . . . . . . . . . 14 lastS substr substr substr ++ ++ substr substr substr ++ lastS ++
157 sbccom 3327 . . . . . . . . . . . . . . . 16 substr ++ lastS ++ ++ substr ++ lastS
158157a1i 11 . . . . . . . . . . . . . . 15 lastS substr ++ lastS ++ ++ substr ++ lastS
159158imbi2d 323 . . . . . . . . . . . . . 14 lastS substr substr substr ++ lastS ++ substr substr ++ substr ++ lastS
160156, 159bitrd 261 . . . . . . . . . . . . 13 lastS substr substr substr ++ ++ substr substr ++ substr ++ lastS
161 dfsbcq 3257 . . . . . . . . . . . . . . 15 substr substr substr substr
162119eqeq1d 2473 . . . . . . . . . . . . . . 15 substr substr substr substr
163161, 162anbi12d 725 . . . . . . . . . . . . . 14 substr substr substr substr substr substr substr
164 oveq1 6315 . . . . . . . . . . . . . . 15 substr ++ substr ++
165164sbceq1d 3260 . . . . . . . . . . . . . 14 substr ++ substr ++ lastS substr ++ substr ++ lastS
166163, 165imbi12d 327 . . . . . . . . . . . . 13 substr substr substr ++ substr ++ lastS substr substr substr substr substr ++ substr ++ lastS
167 s1eq 12792 . . . . . . . . . . . . . . . 16 lastS lastS
168167oveq2d 6324 . . . . . . . . . . . . . . 15 lastS substr ++ substr ++ lastS
169168sbceq1d 3260 . . . . . . . . . . . . . 14 lastS substr ++ substr ++ lastS substr ++ lastS substr ++ lastS
170169imbi2d 323 . . . . . . . . . . . . 13 lastS substr substr substr substr substr ++ substr ++ lastS substr substr substr substr substr ++ lastS substr ++ lastS
171 simplr 770 . . . . . . . . . . . . . . . . . 18 Word Word Word
172 simpll 768 . . . . . . . . . . . . . . . . . 18 Word Word Word
173 simpr 468 . . . . . . . . . . . . . . . . . 18 Word Word
174 wrd2ind.7 . . . . . . . . . . . . . . . . . 18 Word Word
175171, 172, 173, 174syl3anc 1292 . . . . . . . . . . . . . . . . 17 Word Word
17644ancoms 460 . . . . . . . . . . . . . . . . . 18
177129, 128, 176sbc2ie 3323 . . . . . . . . . . . . . . . . 17
178 ovex 6336 . . . . . . . . . . . . . . . . . 18 ++
179 ovex 6336 . . . . . . . . . . . . . . . . . 18 ++
180 wrd2ind.3 . . . . . . . . . . . . . . . . . . 19 ++ ++
181180ancoms 460 . . . . . . . . . . . . . . . . . 18 ++ ++
182178, 179, 181sbc2ie 3323 . . . . . . . . . . . . . . . . 17 ++ ++
183175, 177, 1823imtr4g 278 . . . . . . . . . . . . . . . 16 Word Word ++ ++
184183ex 441 . . . . . . . . . . . . . . 15 Word Word ++ ++
185184com23 80 . . . . . . . . . . . . . 14 Word Word ++ ++
186185impd 438 . . . . . . . . . . . . 13 Word Word ++ ++
187152, 160, 166, 170, 186vtocl4ga 3105 . . . . . . . . . . . 12 substr Word lastS substr Word lastS substr substr substr substr substr ++ lastS substr ++ lastS
18884, 144, 187sylc 61 . . . . . . . . . . 11 Word Word Word Word substr ++ lastS substr ++ lastS
189 eqtr2 2491 . . . . . . . . . . . . . . . 16
190189ad2antll 743 . . . . . . . . . . . . . . 15 Word Word Word Word
191190, 92eqeltrd 2549 . . . . . . . . . . . . . 14 Word Word Word Word
192 wrdfin 12736 . . . . . . . . . . . . . . . . 17 Word
193192adantr 472 . . . . . . . . . . . . . . . 16 Word Word
194193ad2antrl 742 . . . . . . . . . . . . . . 15 Word Word Word Word
195 hashnncl 12585 . . . . . . . . . . . . . . 15
196194, 195syl 17 . . . . . . . . . . . . . 14 Word Word Word Word
197191, 196mpbid 215 . . . . . . . . . . . . 13 Word Word Word Word
198 swrdccatwrd 12878 . . . . . . . . . . . . . 14 Word substr ++ lastS
199198eqcomd 2477 . . . . . . . . . . . . 13 Word substr ++ lastS
20099, 197, 199syl2anc 673 . . . . . . . . . . . 12 Word Word Word Word substr ++ lastS
201 wrdfin 12736 . . . . . . . . . . . . . . . . 17 Word
202201adantl 473 . . . . . . . . . . . . . . . 16 Word Word
203202ad2antrl 742 . . . . . . . . . . . . . . 15 Word Word Word Word
204 hashnncl 12585 . . . . . . . . . . . . . . 15
205203, 204syl 17 . . . . . . . . . . . . . 14 Word Word Word Word
20693, 205mpbid 215 . . . . . . . . . . . . 13 Word Word Word Word
207 swrdccatwrd 12878 . . . . . . . . . . . . . 14 Word substr ++ lastS
208207eqcomd 2477 . . . . . . . . . . . . 13 Word substr ++ lastS
20989, 206, 208syl2anc 673 . . . . . . . . . . . 12 Word Word Word Word substr ++ lastS
210 sbceq1a 3266 . . . . . . . . . . . . 13 substr ++ lastS substr ++ lastS
211 sbceq1a 3266 . . . . . . . . . . . . 13 substr ++ lastS substr ++ lastS substr ++ lastS substr ++ lastS
212210, 211sylan9bb 714 . . . . . . . . . . . 12 substr ++ lastS substr ++ lastS substr ++ lastS substr ++ lastS
213200, 209, 212syl2anc 673 . . . . . . . . . . 11 Word Word Word Word substr ++ lastS substr ++ lastS
214188, 213mpbird 240 . . . . . . . . . 10 Word Word Word Word
215214expr 626 . . . . . . . . 9 Word Word Word Word
216215ralrimivva 2814 . . . . . . . 8 Word Word Word Word
217216ex 441 . . . . . . 7 Word Word Word Word
21848, 217syl5bi 225 . . . . . 6 Word Word Word Word
2195, 9, 13, 17, 37, 218nn0ind 11053 . . . . 5 Word Word
2201, 219syl 17 . . . 4 Word Word Word
2212203ad2ant1 1051 . . 3 Word Word Word Word
222 fveq2 5879 . . . . . . . . 9
223222eqeq2d 2481 . . . . . . . 8
224223anbi1d 719 . . . . . . 7
225 wrd2ind.5 . . . . . . 7
226224, 225imbi12d 327 . . . . . 6
227226ralbidv 2829 . . . . 5 Word Word
228227rspcv 3132 . . . 4 Word Word Word Word
2292283ad2ant2 1052 . . 3 Word Word Word Word Word
230221, 229mpd 15 . 2 Word Word Word
231 eqidd 2472 . 2 Word Word
232 fveq2 5879 . . . . . . . . . . 11
233232eqeq1d 2473 . . . . . . . . . 10
234232eqeq1d 2473 . . . . . . . . . 10
235233, 234anbi12d 725 . . . . . . . . 9
236 wrd2ind.4 . . . . . . . . 9
237235, 236imbi12d 327 . . . . . . . 8
238237rspcv 3132 . . . . . . 7 Word Word
239238com23 80 . . . . . 6 Word Word
240239expd 443 . . . . 5 Word Word
241240com34 85 . . . 4 Word Word
242241imp 436 . . 3 Word Word
2432423adant2 1049 . 2 Word Word Word