Step |
Hyp |
Ref |
Expression |
1 |
|
clwwlkclwwlkn |
|- ( W e. ( N ClWWalksN G ) -> W e. ( ClWWalks ` G ) ) |
2 |
|
clwwlknlen |
|- ( W e. ( N ClWWalksN G ) -> ( # ` W ) = N ) |
3 |
2
|
eqcomd |
|- ( W e. ( N ClWWalksN G ) -> N = ( # ` W ) ) |
4 |
3
|
oveq2d |
|- ( W e. ( N ClWWalksN G ) -> ( 0 ... N ) = ( 0 ... ( # ` W ) ) ) |
5 |
4
|
eleq2d |
|- ( W e. ( N ClWWalksN G ) -> ( M e. ( 0 ... N ) <-> M e. ( 0 ... ( # ` W ) ) ) ) |
6 |
5
|
biimpa |
|- ( ( W e. ( N ClWWalksN G ) /\ M e. ( 0 ... N ) ) -> M e. ( 0 ... ( # ` W ) ) ) |
7 |
|
clwwisshclwwsn |
|- ( ( W e. ( ClWWalks ` G ) /\ M e. ( 0 ... ( # ` W ) ) ) -> ( W cyclShift M ) e. ( ClWWalks ` G ) ) |
8 |
1 6 7
|
syl2an2r |
|- ( ( W e. ( N ClWWalksN G ) /\ M e. ( 0 ... N ) ) -> ( W cyclShift M ) e. ( ClWWalks ` G ) ) |
9 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
10 |
9
|
clwwlknwrd |
|- ( W e. ( N ClWWalksN G ) -> W e. Word ( Vtx ` G ) ) |
11 |
|
elfzelz |
|- ( M e. ( 0 ... N ) -> M e. ZZ ) |
12 |
|
cshwlen |
|- ( ( W e. Word ( Vtx ` G ) /\ M e. ZZ ) -> ( # ` ( W cyclShift M ) ) = ( # ` W ) ) |
13 |
10 11 12
|
syl2an |
|- ( ( W e. ( N ClWWalksN G ) /\ M e. ( 0 ... N ) ) -> ( # ` ( W cyclShift M ) ) = ( # ` W ) ) |
14 |
2
|
adantr |
|- ( ( W e. ( N ClWWalksN G ) /\ M e. ( 0 ... N ) ) -> ( # ` W ) = N ) |
15 |
13 14
|
eqtrd |
|- ( ( W e. ( N ClWWalksN G ) /\ M e. ( 0 ... N ) ) -> ( # ` ( W cyclShift M ) ) = N ) |
16 |
|
isclwwlkn |
|- ( ( W cyclShift M ) e. ( N ClWWalksN G ) <-> ( ( W cyclShift M ) e. ( ClWWalks ` G ) /\ ( # ` ( W cyclShift M ) ) = N ) ) |
17 |
8 15 16
|
sylanbrc |
|- ( ( W e. ( N ClWWalksN G ) /\ M e. ( 0 ... N ) ) -> ( W cyclShift M ) e. ( N ClWWalksN G ) ) |