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
UMGraph
cyclShift ClWWalksN
cyclShift |
6 | | prmnn 15388 |
. . . . . . . . . . . 12
|
7 | 6 | nnnn0d 11351 |
. . . . . . . . . . 11
|
8 | 7 | adantl 482 |
. . . . . . . . . 10
UMGraph
|
9 | 1 | eleq2i 2693 |
. . . . . . . . . . 11
ClWWalksN |
10 | 9 | biimpi 206 |
. . . . . . . . . 10
ClWWalksN
|
11 | | clwwlksnscsh 26940 |
. . . . . . . . . 10
ClWWalksN ClWWalksN cyclShift Word Vtx
cyclShift |
12 | 8, 10, 11 | syl2an 494 |
. . . . . . . . 9
UMGraph ClWWalksN cyclShift Word Vtx
cyclShift |
13 | 5, 12 | eqtrd 2656 |
. . . . . . . 8
UMGraph
cyclShift Word
Vtx cyclShift |
14 | 13 | eqeq2d 2632 |
. . . . . . 7
UMGraph
cyclShift
Word Vtx
cyclShift |
15 | 6 | adantl 482 |
. . . . . . . . . . . 12
UMGraph
|
16 | | simpll 790 |
. . . . . . . . . . . . . . . 16
Word Vtx Word Vtx |
17 | | elnnne0 11306 |
. . . . . . . . . . . . . . . . . 18
|
18 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . 22
|
19 | 18 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . 21
|
20 | | hasheq0 13154 |
. . . . . . . . . . . . . . . . . . . . 21
Word Vtx
|
21 | 19, 20 | sylan9bbr 737 |
. . . . . . . . . . . . . . . . . . . 20
Word Vtx
|
22 | 21 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . . 19
Word Vtx
|
23 | 22 | biimpcd 239 |
. . . . . . . . . . . . . . . . . 18
Word Vtx |
24 | 17, 23 | simplbiim 659 |
. . . . . . . . . . . . . . . . 17
Word Vtx |
25 | 24 | impcom 446 |
. . . . . . . . . . . . . . . 16
Word Vtx |
26 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
Word Vtx |
27 | 26 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
Word Vtx |
28 | 16, 25, 27 | 3jca 1242 |
. . . . . . . . . . . . . . 15
Word Vtx Word
Vtx
|
29 | 28 | ex 450 |
. . . . . . . . . . . . . 14
Word Vtx
Word Vtx |
30 | | eqid 2622 |
. . . . . . . . . . . . . . 15
Vtx Vtx |
31 | 30 | clwwlknbp 26885 |
. . . . . . . . . . . . . 14
ClWWalksN Word Vtx |
32 | 29, 31 | syl11 33 |
. . . . . . . . . . . . 13
ClWWalksN Word
Vtx
|
33 | 9, 32 | syl5bi 232 |
. . . . . . . . . . . 12
Word Vtx |
34 | 15, 33 | syl 17 |
. . . . . . . . . . 11
UMGraph
Word
Vtx
|
35 | 34 | imp 445 |
. . . . . . . . . 10
UMGraph Word
Vtx
|
36 | | scshwfzeqfzo 13572 |
. . . . . . . . . 10
Word Vtx Word Vtx cyclShift Word Vtx
..^ cyclShift
|
37 | 35, 36 | syl 17 |
. . . . . . . . 9
UMGraph Word Vtx cyclShift Word Vtx
..^ cyclShift
|
38 | 37 | eqeq2d 2632 |
. . . . . . . 8
UMGraph
Word Vtx cyclShift
Word Vtx
..^ cyclShift
|
39 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
Word Vtx ..^ cyclShift
Word Vtx
..^ cyclShift
|
40 | | simprl 794 |
. . . . . . . . . . . . . . . . 17
Word Vtx ClWWalksN
UMGraph UMGraph |
41 | | prmuz2 15408 |
. . . . . . . . . . . . . . . . . . 19
|
42 | 41 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
UMGraph
|
43 | 42 | adantl 482 |
. . . . . . . . . . . . . . . . 17
Word Vtx ClWWalksN
UMGraph |
44 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
Word Vtx ClWWalksN
UMGraph ClWWalksN |
45 | | umgr2cwwkdifex 26942 |
. . . . . . . . . . . . . . . . 17
UMGraph
ClWWalksN
..^ |
46 | 40, 43, 44, 45 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
Word Vtx ClWWalksN
UMGraph ..^ |
47 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . 22
cyclShift cyclShift |
48 | 47 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . 21
cyclShift
cyclShift |
49 | 48 | cbvrexv 3172 |
. . . . . . . . . . . . . . . . . . . 20
..^ cyclShift
..^ cyclShift
|
50 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . 22
cyclShift
cyclShift |
51 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . 22
cyclShift cyclShift |
52 | 50, 51 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . . . 21
cyclShift
cyclShift |
53 | 52 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . 20
..^ cyclShift
..^ cyclShift |
54 | 49, 53 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . 19
..^ cyclShift
..^ cyclShift |
55 | 54 | cbvrabv 3199 |
. . . . . . . . . . . . . . . . . 18
Word Vtx ..^ cyclShift Word
Vtx ..^ cyclShift |
56 | 55 | cshwshashnsame 15810 |
. . . . . . . . . . . . . . . . 17
Word Vtx
..^
Word
Vtx ..^ cyclShift |
57 | 56 | ad2ant2rl 785 |
. . . . . . . . . . . . . . . 16
Word Vtx ClWWalksN
UMGraph
..^
Word
Vtx ..^ cyclShift |
58 | 46, 57 | mpd 15 |
. . . . . . . . . . . . . . 15
Word Vtx ClWWalksN
UMGraph Word Vtx ..^ cyclShift
|
59 | 39, 58 | sylan9eqr 2678 |
. . . . . . . . . . . . . 14
Word Vtx
ClWWalksN
UMGraph Word Vtx
..^ cyclShift
|
60 | 59 | exp41 638 |
. . . . . . . . . . . . 13
Word Vtx
ClWWalksN UMGraph
Word Vtx ..^ cyclShift
|
61 | 60 | adantr 481 |
. . . . . . . . . . . 12
Word Vtx ClWWalksN
UMGraph Word Vtx
..^ cyclShift
|
62 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
ClWWalksN ClWWalksN |
63 | 62 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
ClWWalksN
ClWWalksN
|
64 | | eleq1 2689 |
. . . . . . . . . . . . . . . . 17
|
65 | 64 | anbi2d 740 |
. . . . . . . . . . . . . . . 16
UMGraph
UMGraph |
66 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ |
67 | 66 | rexeqdv 3145 |
. . . . . . . . . . . . . . . . . . 19
..^ cyclShift
..^ cyclShift
|
68 | 67 | rabbidv 3189 |
. . . . . . . . . . . . . . . . . 18
Word Vtx ..^ cyclShift Word
Vtx ..^ cyclShift |
69 | 68 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
Word Vtx
..^ cyclShift
Word Vtx ..^ cyclShift |
70 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . 17
|
71 | 69, 70 | imbi12d 334 |
. . . . . . . . . . . . . . . 16
Word Vtx ..^ cyclShift
Word Vtx
..^ cyclShift
|
72 | 65, 71 | imbi12d 334 |
. . . . . . . . . . . . . . 15
UMGraph
Word Vtx ..^ cyclShift
UMGraph Word Vtx
..^ cyclShift
|
73 | 63, 72 | imbi12d 334 |
. . . . . . . . . . . . . 14
ClWWalksN UMGraph
Word Vtx ..^ cyclShift ClWWalksN UMGraph
Word Vtx ..^ cyclShift
|
74 | 73 | eqcoms 2630 |
. . . . . . . . . . . . 13
ClWWalksN UMGraph
Word Vtx ..^ cyclShift ClWWalksN UMGraph
Word Vtx ..^ cyclShift
|
75 | 74 | adantl 482 |
. . . . . . . . . . . 12
Word Vtx ClWWalksN UMGraph
Word Vtx ..^ cyclShift ClWWalksN UMGraph
Word Vtx ..^ cyclShift
|
76 | 61, 75 | mpbird 247 |
. . . . . . . . . . 11
Word Vtx ClWWalksN UMGraph
Word Vtx ..^ cyclShift |
77 | 31, 76 | mpcom 38 |
. . . . . . . . . 10
ClWWalksN UMGraph Word Vtx
..^ cyclShift
|
78 | 77, 1 | eleq2s 2719 |
. . . . . . . . 9
UMGraph
Word Vtx ..^ cyclShift |
79 | 78 | impcom 446 |
. . . . . . . 8
UMGraph
Word Vtx ..^ cyclShift |
80 | 38, 79 | sylbid 230 |
. . . . . . 7
UMGraph
Word Vtx cyclShift |
81 | 14, 80 | sylbid 230 |
. . . . . 6
UMGraph
cyclShift |
82 | 81 | rexlimdva 3031 |
. . . . 5
UMGraph
cyclShift |
83 | 82 | com12 32 |
. . . 4
cyclShift UMGraph |
84 | 3, 83 | syl6bi 243 |
. . 3
UMGraph |
85 | 84 | pm2.43i 52 |
. 2
UMGraph
|
86 | 85 | com12 32 |
1
UMGraph
|