Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . 6
Vtx Vtx |
2 | 1 | clwwlkbp 26883 |
. . . . 5
ClWWalks
Word Vtx
|
3 | | cshw0 13540 |
. . . . . . . 8
Word Vtx
cyclShift |
4 | 3 | 3ad2ant2 1083 |
. . . . . . 7
Word Vtx
cyclShift |
5 | 4 | eleq1d 2686 |
. . . . . 6
Word Vtx
cyclShift ClWWalks
ClWWalks |
6 | 5 | biimprd 238 |
. . . . 5
Word Vtx
ClWWalks cyclShift
ClWWalks |
7 | 2, 6 | mpcom 38 |
. . . 4
ClWWalks
cyclShift ClWWalks |
8 | | oveq2 6658 |
. . . . 5
cyclShift cyclShift |
9 | 8 | eleq1d 2686 |
. . . 4
cyclShift ClWWalks cyclShift ClWWalks |
10 | 7, 9 | syl5ibrcom 237 |
. . 3
ClWWalks
cyclShift ClWWalks |
11 | 10 | adantr 481 |
. 2
ClWWalks
..^ cyclShift ClWWalks |
12 | | fzo1fzo0n0 12518 |
. . . . . 6
..^ ..^ |
13 | | cshwcl 13544 |
. . . . . . . . . . . . 13
Word Vtx
cyclShift Word Vtx |
14 | 13 | adantr 481 |
. . . . . . . . . . . 12
Word Vtx cyclShift Word Vtx |
15 | 14 | 3ad2ant1 1082 |
. . . . . . . . . . 11
Word Vtx
..^ Edg lastS Edg cyclShift Word Vtx |
16 | 15 | adantr 481 |
. . . . . . . . . 10
Word Vtx
..^ Edg lastS Edg ..^
cyclShift Word Vtx |
17 | | simpl 473 |
. . . . . . . . . . . . . 14
Word Vtx Word Vtx |
18 | | elfzoelz 12470 |
. . . . . . . . . . . . . 14
..^
|
19 | | cshwlen 13545 |
. . . . . . . . . . . . . 14
Word Vtx cyclShift |
20 | 17, 18, 19 | syl2an 494 |
. . . . . . . . . . . . 13
Word Vtx ..^ cyclShift |
21 | | hasheq0 13154 |
. . . . . . . . . . . . . . . . 17
Word Vtx
|
22 | 21 | bicomd 213 |
. . . . . . . . . . . . . . . 16
Word Vtx
|
23 | 22 | necon3bid 2838 |
. . . . . . . . . . . . . . 15
Word Vtx
|
24 | 23 | biimpa 501 |
. . . . . . . . . . . . . 14
Word Vtx |
25 | 24 | adantr 481 |
. . . . . . . . . . . . 13
Word Vtx ..^ |
26 | 20, 25 | eqnetrd 2861 |
. . . . . . . . . . . 12
Word Vtx ..^ cyclShift |
27 | 14 | adantr 481 |
. . . . . . . . . . . . . 14
Word Vtx ..^ cyclShift Word Vtx |
28 | | hasheq0 13154 |
. . . . . . . . . . . . . 14
cyclShift Word Vtx cyclShift cyclShift |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . 13
Word Vtx ..^ cyclShift
cyclShift |
30 | 29 | necon3bid 2838 |
. . . . . . . . . . . 12
Word Vtx ..^ cyclShift
cyclShift |
31 | 26, 30 | mpbid 222 |
. . . . . . . . . . 11
Word Vtx ..^ cyclShift |
32 | 31 | 3ad2antl1 1223 |
. . . . . . . . . 10
Word Vtx
..^ Edg lastS Edg ..^
cyclShift |
33 | 16, 32 | jca 554 |
. . . . . . . . 9
Word Vtx
..^ Edg lastS Edg ..^ cyclShift Word Vtx
cyclShift |
34 | 17 | 3ad2ant1 1082 |
. . . . . . . . . . 11
Word Vtx
..^ Edg lastS Edg Word Vtx |
35 | 34 | anim1i 592 |
. . . . . . . . . 10
Word Vtx
..^ Edg lastS Edg ..^ Word Vtx ..^ |
36 | | 3simpc 1060 |
. . . . . . . . . . 11
Word Vtx
..^ Edg lastS Edg ..^ Edg lastS Edg |
37 | 36 | adantr 481 |
. . . . . . . . . 10
Word Vtx
..^ Edg lastS Edg ..^ ..^ Edg lastS Edg |
38 | | clwwisshclwwslem 26927 |
. . . . . . . . . 10
Word Vtx ..^
..^ Edg lastS Edg ..^ cyclShift
cyclShift cyclShift Edg |
39 | 35, 37, 38 | sylc 65 |
. . . . . . . . 9
Word Vtx
..^ Edg lastS Edg ..^
..^ cyclShift
cyclShift cyclShift Edg |
40 | | elfzofz 12485 |
. . . . . . . . . . . . . . . 16
..^
|
41 | | lswcshw 13561 |
. . . . . . . . . . . . . . . 16
Word Vtx
lastS cyclShift
|
42 | 40, 41 | sylan2 491 |
. . . . . . . . . . . . . . 15
Word Vtx ..^ lastS
cyclShift
|
43 | | fzo0ss1 12498 |
. . . . . . . . . . . . . . . . 17
..^ ..^ |
44 | 43 | sseli 3599 |
. . . . . . . . . . . . . . . 16
..^
..^ |
45 | | cshwidx0 13552 |
. . . . . . . . . . . . . . . 16
Word Vtx ..^ cyclShift |
46 | 44, 45 | sylan2 491 |
. . . . . . . . . . . . . . 15
Word Vtx ..^ cyclShift |
47 | 42, 46 | preq12d 4276 |
. . . . . . . . . . . . . 14
Word Vtx ..^ lastS cyclShift cyclShift |
48 | 47 | ex 450 |
. . . . . . . . . . . . 13
Word Vtx
..^
lastS cyclShift cyclShift |
49 | 48 | adantr 481 |
. . . . . . . . . . . 12
Word Vtx
..^ lastS cyclShift
cyclShift
|
50 | 49 | 3ad2ant1 1082 |
. . . . . . . . . . 11
Word Vtx
..^ Edg lastS Edg ..^
lastS cyclShift cyclShift |
51 | 50 | imp 445 |
. . . . . . . . . 10
Word Vtx
..^ Edg lastS Edg ..^
lastS cyclShift cyclShift |
52 | | elfzo1elm1fzo0 12569 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
53 | 52 | adantl 482 |
. . . . . . . . . . . . . . . 16
Word Vtx ..^ ..^ |
54 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
|
55 | 54 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
Word Vtx ..^
|
56 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
|
57 | 56 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
|
58 | 18 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . 22
..^
|
59 | 58 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
Word Vtx ..^ |
60 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . 21
Word Vtx ..^ |
61 | 59, 60 | npcand 10396 |
. . . . . . . . . . . . . . . . . . . 20
Word Vtx ..^ |
62 | 61 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx ..^ |
63 | 57, 62 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . 18
Word Vtx ..^
|
64 | 55, 63 | preq12d 4276 |
. . . . . . . . . . . . . . . . 17
Word Vtx ..^
|
65 | 64 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
Word Vtx ..^
Edg
Edg |
66 | 53, 65 | rspcdv 3312 |
. . . . . . . . . . . . . . 15
Word Vtx ..^ ..^ Edg Edg |
67 | 66 | a1d 25 |
. . . . . . . . . . . . . 14
Word Vtx ..^ lastS Edg
..^ Edg
Edg |
68 | 67 | ex 450 |
. . . . . . . . . . . . 13
Word Vtx
..^ lastS Edg
..^ Edg
Edg |
69 | 68 | adantr 481 |
. . . . . . . . . . . 12
Word Vtx
..^
lastS Edg ..^ Edg Edg |
70 | 69 | com24 95 |
. . . . . . . . . . 11
Word Vtx
..^ Edg lastS Edg
..^
Edg |
71 | 70 | 3imp1 1280 |
. . . . . . . . . 10
Word Vtx
..^ Edg lastS Edg ..^
Edg |
72 | 51, 71 | eqeltrd 2701 |
. . . . . . . . 9
Word Vtx
..^ Edg lastS Edg ..^
lastS cyclShift cyclShift Edg |
73 | 33, 39, 72 | 3jca 1242 |
. . . . . . . 8
Word Vtx
..^ Edg lastS Edg ..^ cyclShift Word Vtx cyclShift ..^ cyclShift cyclShift cyclShift Edg
lastS cyclShift
cyclShift Edg |
74 | 73 | expcom 451 |
. . . . . . 7
..^
Word Vtx
..^ Edg lastS Edg cyclShift Word Vtx cyclShift ..^ cyclShift cyclShift cyclShift Edg
lastS cyclShift
cyclShift Edg |
75 | | eqid 2622 |
. . . . . . . 8
Edg Edg |
76 | 1, 75 | isclwwlks 26880 |
. . . . . . 7
ClWWalks Word Vtx
..^ Edg lastS Edg |
77 | 1, 75 | isclwwlks 26880 |
. . . . . . 7
cyclShift ClWWalks
cyclShift Word Vtx cyclShift
..^ cyclShift cyclShift cyclShift Edg
lastS cyclShift
cyclShift Edg |
78 | 74, 76, 77 | 3imtr4g 285 |
. . . . . 6
..^
ClWWalks cyclShift
ClWWalks |
79 | 12, 78 | sylbir 225 |
. . . . 5
..^
ClWWalks
cyclShift ClWWalks |
80 | 79 | expcom 451 |
. . . 4
..^
ClWWalks
cyclShift ClWWalks |
81 | 80 | com13 88 |
. . 3
ClWWalks
..^ cyclShift
ClWWalks |
82 | 81 | imp 445 |
. 2
ClWWalks
..^ cyclShift
ClWWalks |
83 | 11, 82 | pm2.61dne 2880 |
1
ClWWalks
..^
cyclShift ClWWalks |