Step | Hyp | Ref
| Expression |
1 | | erclwwlksn.w |
. . . . 5
ClWWalksN
|
2 | | erclwwlksn.r |
. . . . 5
cyclShift |
3 | 1, 2 | eclclwwlksn1 26952 |
. . . 4
cyclShift |
4 | | rabeq 3192 |
. . . . . . . . . 10
ClWWalksN cyclShift ClWWalksN
cyclShift |
5 | 1, 4 | mp1i 13 |
. . . . . . . . 9
cyclShift ClWWalksN
cyclShift |
6 | | prmnn 15388 |
. . . . . . . . . . 11
|
7 | 6 | nnnn0d 11351 |
. . . . . . . . . 10
|
8 | 1 | eleq2i 2693 |
. . . . . . . . . . 11
ClWWalksN |
9 | 8 | biimpi 206 |
. . . . . . . . . 10
ClWWalksN
|
10 | | clwwlksnscsh 26940 |
. . . . . . . . . 10
ClWWalksN ClWWalksN cyclShift Word Vtx
cyclShift |
11 | 7, 9, 10 | syl2an 494 |
. . . . . . . . 9
ClWWalksN cyclShift Word Vtx
cyclShift |
12 | 5, 11 | eqtrd 2656 |
. . . . . . . 8
cyclShift Word
Vtx cyclShift |
13 | 12 | eqeq2d 2632 |
. . . . . . 7
cyclShift
Word Vtx
cyclShift |
14 | | simpll 790 |
. . . . . . . . . . . . . . . 16
Word Vtx Word Vtx |
15 | | elnnne0 11306 |
. . . . . . . . . . . . . . . . . 18
|
16 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . 22
|
17 | 16 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . 21
|
18 | | hasheq0 13154 |
. . . . . . . . . . . . . . . . . . . . 21
Word Vtx
|
19 | 17, 18 | sylan9bbr 737 |
. . . . . . . . . . . . . . . . . . . 20
Word Vtx
|
20 | 19 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx
|
21 | 20 | biimpcd 239 |
. . . . . . . . . . . . . . . . . 18
Word Vtx |
22 | 15, 21 | simplbiim 659 |
. . . . . . . . . . . . . . . . 17
Word Vtx |
23 | 22 | impcom 446 |
. . . . . . . . . . . . . . . 16
Word Vtx |
24 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
Word Vtx |
25 | 24 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
Word Vtx |
26 | 14, 23, 25 | 3jca 1242 |
. . . . . . . . . . . . . . 15
Word Vtx Word
Vtx
|
27 | 26 | ex 450 |
. . . . . . . . . . . . . 14
Word Vtx
Word Vtx |
28 | | eqid 2622 |
. . . . . . . . . . . . . . 15
Vtx Vtx |
29 | 28 | clwwlknbp 26885 |
. . . . . . . . . . . . . 14
ClWWalksN Word Vtx |
30 | 27, 29 | syl11 33 |
. . . . . . . . . . . . 13
ClWWalksN Word
Vtx
|
31 | 8, 30 | syl5bi 232 |
. . . . . . . . . . . 12
Word Vtx |
32 | 6, 31 | syl 17 |
. . . . . . . . . . 11
Word
Vtx
|
33 | 32 | imp 445 |
. . . . . . . . . 10
Word
Vtx
|
34 | | scshwfzeqfzo 13572 |
. . . . . . . . . 10
Word Vtx Word Vtx cyclShift Word Vtx
..^ cyclShift
|
35 | 33, 34 | syl 17 |
. . . . . . . . 9
Word Vtx cyclShift Word Vtx
..^ cyclShift
|
36 | 35 | eqeq2d 2632 |
. . . . . . . 8
Word Vtx cyclShift
Word Vtx
..^ cyclShift
|
37 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . 23
cyclShift cyclShift |
38 | 37 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . 22
cyclShift
cyclShift |
39 | 38 | cbvrexv 3172 |
. . . . . . . . . . . . . . . . . . . . 21
..^ cyclShift
..^ cyclShift
|
40 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . 23
cyclShift
cyclShift |
41 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . 23
cyclShift cyclShift |
42 | 40, 41 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . . . 22
cyclShift
cyclShift |
43 | 42 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . 21
..^ cyclShift
..^ cyclShift |
44 | 39, 43 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . . 20
..^ cyclShift
..^ cyclShift |
45 | 44 | cbvrabv 3199 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx ..^ cyclShift Word
Vtx ..^ cyclShift |
46 | 45 | cshwshash 15811 |
. . . . . . . . . . . . . . . . . 18
Word Vtx
Word Vtx ..^ cyclShift
Word
Vtx ..^ cyclShift |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Word Vtx
Word Vtx
..^ cyclShift
Word Vtx ..^ cyclShift Word Vtx
..^ cyclShift
|
48 | 47 | orcomd 403 |
. . . . . . . . . . . . . . . 16
Word Vtx
Word Vtx
..^ cyclShift
Word Vtx ..^ cyclShift Word Vtx
..^ cyclShift
|
49 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx ..^ cyclShift
Word Vtx
..^ cyclShift
|
50 | 49 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . 18
Word Vtx ..^ cyclShift
Word Vtx ..^ cyclShift |
51 | 49 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . 18
Word Vtx ..^ cyclShift
Word Vtx ..^ cyclShift
|
52 | 50, 51 | orbi12d 746 |
. . . . . . . . . . . . . . . . 17
Word Vtx ..^ cyclShift
Word Vtx ..^ cyclShift
Word
Vtx ..^ cyclShift |
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . . 16
Word Vtx
Word Vtx
..^ cyclShift
Word Vtx ..^ cyclShift
Word
Vtx ..^ cyclShift |
54 | 48, 53 | mpbird 247 |
. . . . . . . . . . . . . . 15
Word Vtx
Word Vtx
..^ cyclShift
|
55 | 54 | ex 450 |
. . . . . . . . . . . . . 14
Word Vtx
Word Vtx ..^ cyclShift
|
56 | 55 | ex 450 |
. . . . . . . . . . . . 13
Word Vtx
Word Vtx
..^ cyclShift
|
57 | 56 | adantr 481 |
. . . . . . . . . . . 12
Word Vtx
Word Vtx ..^ cyclShift
|
58 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
|
59 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
60 | 59 | rexeqdv 3145 |
. . . . . . . . . . . . . . . . . 18
..^ cyclShift
..^ cyclShift
|
61 | 60 | rabbidv 3189 |
. . . . . . . . . . . . . . . . 17
Word Vtx ..^ cyclShift Word
Vtx ..^ cyclShift |
62 | 61 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
Word Vtx
..^ cyclShift
Word Vtx ..^ cyclShift |
63 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . 17
|
64 | 63 | orbi2d 738 |
. . . . . . . . . . . . . . . 16
|
65 | 62, 64 | imbi12d 334 |
. . . . . . . . . . . . . . 15
Word Vtx ..^ cyclShift
Word Vtx
..^ cyclShift
|
66 | 58, 65 | imbi12d 334 |
. . . . . . . . . . . . . 14
Word Vtx ..^ cyclShift Word Vtx ..^ cyclShift |
67 | 66 | eqcoms 2630 |
. . . . . . . . . . . . 13
Word Vtx ..^ cyclShift
Word Vtx
..^ cyclShift
|
68 | 67 | adantl 482 |
. . . . . . . . . . . 12
Word Vtx Word
Vtx ..^ cyclShift
Word Vtx
..^ cyclShift
|
69 | 57, 68 | mpbird 247 |
. . . . . . . . . . 11
Word Vtx
Word Vtx ..^ cyclShift |
70 | 29, 69 | syl 17 |
. . . . . . . . . 10
ClWWalksN Word Vtx
..^ cyclShift
|
71 | 70, 1 | eleq2s 2719 |
. . . . . . . . 9
Word Vtx ..^ cyclShift |
72 | 71 | impcom 446 |
. . . . . . . 8
Word Vtx ..^ cyclShift |
73 | 36, 72 | sylbid 230 |
. . . . . . 7
Word Vtx cyclShift |
74 | 13, 73 | sylbid 230 |
. . . . . 6
cyclShift |
75 | 74 | rexlimdva 3031 |
. . . . 5
cyclShift |
76 | 75 | com12 32 |
. . . 4
cyclShift |
77 | 3, 76 | syl6bi 243 |
. . 3
|
78 | 77 | pm2.43i 52 |
. 2
|
79 | 78 | impcom 446 |
1
|