Step |
Hyp |
Ref |
Expression |
1 |
|
erclwwlk.r |
|- .~ = { <. u , w >. | ( u e. ( ClWWalks ` G ) /\ w e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) } |
2 |
|
anidm |
|- ( ( x e. ( ClWWalks ` G ) /\ x e. ( ClWWalks ` G ) ) <-> x e. ( ClWWalks ` G ) ) |
3 |
2
|
anbi1i |
|- ( ( ( x e. ( ClWWalks ` G ) /\ x e. ( ClWWalks ` G ) ) /\ E. n e. ( 0 ... ( # ` x ) ) x = ( x cyclShift n ) ) <-> ( x e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` x ) ) x = ( x cyclShift n ) ) ) |
4 |
|
df-3an |
|- ( ( x e. ( ClWWalks ` G ) /\ x e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` x ) ) x = ( x cyclShift n ) ) <-> ( ( x e. ( ClWWalks ` G ) /\ x e. ( ClWWalks ` G ) ) /\ E. n e. ( 0 ... ( # ` x ) ) x = ( x cyclShift n ) ) ) |
5 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
6 |
5
|
clwwlkbp |
|- ( x e. ( ClWWalks ` G ) -> ( G e. _V /\ x e. Word ( Vtx ` G ) /\ x =/= (/) ) ) |
7 |
|
cshw0 |
|- ( x e. Word ( Vtx ` G ) -> ( x cyclShift 0 ) = x ) |
8 |
|
0nn0 |
|- 0 e. NN0 |
9 |
8
|
a1i |
|- ( x e. Word ( Vtx ` G ) -> 0 e. NN0 ) |
10 |
|
lencl |
|- ( x e. Word ( Vtx ` G ) -> ( # ` x ) e. NN0 ) |
11 |
|
hashge0 |
|- ( x e. Word ( Vtx ` G ) -> 0 <_ ( # ` x ) ) |
12 |
|
elfz2nn0 |
|- ( 0 e. ( 0 ... ( # ` x ) ) <-> ( 0 e. NN0 /\ ( # ` x ) e. NN0 /\ 0 <_ ( # ` x ) ) ) |
13 |
9 10 11 12
|
syl3anbrc |
|- ( x e. Word ( Vtx ` G ) -> 0 e. ( 0 ... ( # ` x ) ) ) |
14 |
|
eqcom |
|- ( ( x cyclShift 0 ) = x <-> x = ( x cyclShift 0 ) ) |
15 |
14
|
biimpi |
|- ( ( x cyclShift 0 ) = x -> x = ( x cyclShift 0 ) ) |
16 |
|
oveq2 |
|- ( n = 0 -> ( x cyclShift n ) = ( x cyclShift 0 ) ) |
17 |
16
|
rspceeqv |
|- ( ( 0 e. ( 0 ... ( # ` x ) ) /\ x = ( x cyclShift 0 ) ) -> E. n e. ( 0 ... ( # ` x ) ) x = ( x cyclShift n ) ) |
18 |
13 15 17
|
syl2an |
|- ( ( x e. Word ( Vtx ` G ) /\ ( x cyclShift 0 ) = x ) -> E. n e. ( 0 ... ( # ` x ) ) x = ( x cyclShift n ) ) |
19 |
7 18
|
mpdan |
|- ( x e. Word ( Vtx ` G ) -> E. n e. ( 0 ... ( # ` x ) ) x = ( x cyclShift n ) ) |
20 |
19
|
3ad2ant2 |
|- ( ( G e. _V /\ x e. Word ( Vtx ` G ) /\ x =/= (/) ) -> E. n e. ( 0 ... ( # ` x ) ) x = ( x cyclShift n ) ) |
21 |
6 20
|
syl |
|- ( x e. ( ClWWalks ` G ) -> E. n e. ( 0 ... ( # ` x ) ) x = ( x cyclShift n ) ) |
22 |
21
|
pm4.71i |
|- ( x e. ( ClWWalks ` G ) <-> ( x e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` x ) ) x = ( x cyclShift n ) ) ) |
23 |
3 4 22
|
3bitr4ri |
|- ( x e. ( ClWWalks ` G ) <-> ( x e. ( ClWWalks ` G ) /\ x e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` x ) ) x = ( x cyclShift n ) ) ) |
24 |
1
|
erclwwlkeq |
|- ( ( x e. _V /\ x e. _V ) -> ( x .~ x <-> ( x e. ( ClWWalks ` G ) /\ x e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` x ) ) x = ( x cyclShift n ) ) ) ) |
25 |
24
|
el2v |
|- ( x .~ x <-> ( x e. ( ClWWalks ` G ) /\ x e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` x ) ) x = ( x cyclShift n ) ) ) |
26 |
23 25
|
bitr4i |
|- ( x e. ( ClWWalks ` G ) <-> x .~ x ) |