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

Theorem wrd2ind 12703
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
Assertion
Ref Expression
wrd2ind
Distinct variable groups:   , ,   , , , ,   , , , , , ,   , , , , , ,   , ,   , , , ,   ,   , ,   ,

Proof of Theorem wrd2ind
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lencl 12562 . . . . 5
2 eqeq2 2472 . . . . . . . . 9
32anbi2d 703 . . . . . . . 8
43imbi1d 317 . . . . . . 7
542ralbidv 2901 . . . . . 6
6 eqeq2 2472 . . . . . . . . 9
76anbi2d 703 . . . . . . . 8
87imbi1d 317 . . . . . . 7
982ralbidv 2901 . . . . . 6
10 eqeq2 2472 . . . . . . . . 9
1110anbi2d 703 . . . . . . . 8
1211imbi1d 317 . . . . . . 7
13122ralbidv 2901 . . . . . 6
14 eqeq2 2472 . . . . . . . . 9
1514anbi2d 703 . . . . . . . 8
1615imbi1d 317 . . . . . . 7
17162ralbidv 2901 . . . . . 6
18 eqeq1 2461 . . . . . . . . . . . 12
1918adantl 466 . . . . . . . . . . 11
20 eqcom 2466 . . . . . . . . . . . . . . 15
21 hasheq0 12433 . . . . . . . . . . . . . . 15
2220, 21syl5bb 257 . . . . . . . . . . . . . 14
23 hasheq0 12433 . . . . . . . . . . . . . . . 16
24 wrd2ind.6 . . . . . . . . . . . . . . . . . 18
25 wrd2ind.1 . . . . . . . . . . . . . . . . . 18
2624, 25mpbiri 233 . . . . . . . . . . . . . . . . 17
2726ex 434 . . . . . . . . . . . . . . . 16
2823, 27syl6bi 228 . . . . . . . . . . . . . . 15
2928com13 80 . . . . . . . . . . . . . 14
3022, 29syl6bi 228 . . . . . . . . . . . . 13
3130com24 87 . . . . . . . . . . . 12
3231imp31 432 . . . . . . . . . . 11
3319, 32sylbid 215 . . . . . . . . . 10
3433ex 434 . . . . . . . . 9
3534com23 78 . . . . . . . 8
3635impd 431 . . . . . . 7
3736rgen2 2882 . . . . . 6
38 fveq2 5871 . . . . . . . . . . . . 13
39 fveq2 5871 . . . . . . . . . . . . 13
4038, 39eqeqan12d 2480 . . . . . . . . . . . 12
4138eqeq1d 2459 . . . . . . . . . . . . 13
4241adantr 465 . . . . . . . . . . . 12
4340, 42anbi12d 710 . . . . . . . . . . 11
44 wrd2ind.2 . . . . . . . . . . 11
4543, 44imbi12d 320 . . . . . . . . . 10
4645ancoms 453 . . . . . . . . 9
4746cbvraldva 3090 . . . . . . . 8
4847cbvralv 3084 . . . . . . 7
49 swrdcl 12646 . . . . . . . . . . . . . . . . 17
5049adantr 465 . . . . . . . . . . . . . . . 16
5150ad2antrl 727 . . . . . . . . . . . . . . 15
52 wrdf 12553 . . . . . . . . . . . . . . . . . 18
5352adantr 465 . . . . . . . . . . . . . . . . 17
5453ad2antrl 727 . . . . . . . . . . . . . . . 16
55 eqeq1 2461 . . . . . . . . . . . . . . . . . . . . 21
56 nn0p1nn 10860 . . . . . . . . . . . . . . . . . . . . . 22
57 eleq1 2529 . . . . . . . . . . . . . . . . . . . . . . 23
5857eqcoms 2469 . . . . . . . . . . . . . . . . . . . . . 22
5956, 58syl5ibr 221 . . . . . . . . . . . . . . . . . . . . 21
6055, 59syl6bi 228 . . . . . . . . . . . . . . . . . . . 20
6160impcom 430 . . . . . . . . . . . . . . . . . . 19
6261adantl 466 . . . . . . . . . . . . . . . . . 18
6362impcom 430 . . . . . . . . . . . . . . . . 17
64 fzo0end 11904 . . . . . . . . . . . . . . . . 17
6563, 64syl 16 . . . . . . . . . . . . . . . 16
6654, 65ffvelrnd 6032 . . . . . . . . . . . . . . 15
6751, 66jca 532 . . . . . . . . . . . . . 14
68 swrdcl 12646 . . . . . . . . . . . . . . . 16
6968adantl 466 . . . . . . . . . . . . . . 15
7069ad2antrl 727 . . . . . . . . . . . . . 14
71 wrdf 12553 . . . . . . . . . . . . . . . . 17
7271adantl 466 . . . . . . . . . . . . . . . 16
7372ad2antrl 727 . . . . . . . . . . . . . . 15
74 eleq1 2529 . . . . . . . . . . . . . . . . . . 19
7556, 74syl5ibr 221 . . . . . . . . . . . . . . . . . 18
7675ad2antll 728 . . . . . . . . . . . . . . . . 17
7776impcom 430 . . . . . . . . . . . . . . . 16
78 fzo0end 11904 . . . . . . . . . . . . . . . 16
7977, 78syl 16 . . . . . . . . . . . . . . 15
8073, 79ffvelrnd 6032 . . . . . . . . . . . . . 14
8167, 70, 80jca32 535 . . . . . . . . . . . . 13
8281adantlr 714 . . . . . . . . . . . 12
83 simprl 756 . . . . . . . . . . . . . 14
84 simplr 755 . . . . . . . . . . . . . 14
85 simprrl 765 . . . . . . . . . . . . . . . . 17
8685oveq1d 6311 . . . . . . . . . . . . . . . 16
87 simprlr 764 . . . . . . . . . . . . . . . . 17
88 fzossfz 11846 . . . . . . . . . . . . . . . . . 18
89 simprrr 766 . . . . . . . . . . . . . . . . . . . 20
9056ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20
9189, 90eqeltrd 2545 . . . . . . . . . . . . . . . . . . 19
9291, 78syl 16 . . . . . . . . . . . . . . . . . 18
9388, 92sseldi 3501 . . . . . . . . . . . . . . . . 17
94 swrd0len 12649 . . . . . . . . . . . . . . . . 17
9587, 93, 94syl2anc 661 . . . . . . . . . . . . . . . 16
96 simprll 763 . . . . . . . . . . . . . . . . 17
97 oveq1 6303 . . . . . . . . . . . . . . . . . . . . . 22
98 oveq2 6304 . . . . . . . . . . . . . . . . . . . . . 22
9997, 98eleq12d 2539 . . . . . . . . . . . . . . . . . . . . 21
10099eqcoms 2469 . . . . . . . . . . . . . . . . . . . 20
101100adantr 465 . . . . . . . . . . . . . . . . . . 19
102101ad2antll 728 . . . . . . . . . . . . . . . . . 18
10393, 102mpbird 232 . . . . . . . . . . . . . . . . 17
104 swrd0len 12649 . . . . . . . . . . . . . . . . 17
10596, 103, 104syl2anc 661 . . . . . . . . . . . . . . . 16
10686, 95, 1053eqtr4d 2508 . . . . . . . . . . . . . . 15
10789oveq1d 6311 . . . . . . . . . . . . . . . 16
108 nn0cn 10830 . . . . . . . . . . . . . . . . . 18
109108ad2antrr 725 . . . . . . . . . . . . . . . . 17
110 ax-1cn 9571 . . . . . . . . . . . . . . . . 17
111 pncan 9849 . . . . . . . . . . . . . . . . 17
112109, 110, 111sylancl 662 . . . . . . . . . . . . . . . 16
11395, 107, 1123eqtrd 2502 . . . . . . . . . . . . . . 15
114106, 113jca 532 . . . . . . . . . . . . . 14
11569adantr 465 . . . . . . . . . . . . . . . 16
116 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . 22
117 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . 22
118116, 117eqeqan12d 2480 . . . . . . . . . . . . . . . . . . . . 21
119118expcom 435 . . . . . . . . . . . . . . . . . . . 20
120119adantl 466 . . . . . . . . . . . . . . . . . . 19
121120imp 429 . . . . . . . . . . . . . . . . . 18
122116eqeq1d 2459 . . . . . . . . . . . . . . . . . . 19
123122adantl 466 . . . . . . . . . . . . . . . . . 18
124121, 123anbi12d 710 . . . . . . . . . . . . . . . . 17
125 vex 3112 . . . . . . . . . . . . . . . . . . . . 21
126 vex 3112 . . . . . . . . . . . . . . . . . . . . 21
127125, 126, 44sbc2ie 3403 . . . . . . . . . . . . . . . . . . . 20
128127bicomi 202 . . . . . . . . . . . . . . . . . . 19
129128a1i 11 . . . . . . . . . . . . . . . . . 18
130 simpr 461 . . . . . . . . . . . . . . . . . . 19
131130sbceq1d 3332 . . . . . . . . . . . . . . . . . 18
132 dfsbcq 3329 . . . . . . . . . . . . . . . . . . . . 21
133132sbcbidv 3386 . . . . . . . . . . . . . . . . . . . 20
134133adantl 466 . . . . . . . . . . . . . . . . . . 19
135134adantr 465 . . . . . . . . . . . . . . . . . 18
136129, 131, 1353bitrd 279 . . . . . . . . . . . . . . . . 17
137124, 136imbi12d 320 . . . . . . . . . . . . . . . 16
138115, 137rspcdv 3213 . . . . . . . . . . . . . . 15
13950, 138rspcimdv 3211 . . . . . . . . . . . . . 14
14083, 84, 114, 139syl3c 61 . . . . . . . . . . . . 13
141140, 106jca 532 . . . . . . . . . . . 12
142 dfsbcq 3329 . . . . . . . . . . . . . . . 16