Step |
Hyp |
Ref |
Expression |
1 |
|
erclwwlkn.w |
|- W = ( N ClWWalksN G ) |
2 |
|
erclwwlkn.r |
|- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) } |
3 |
|
df-3an |
|- ( ( x e. W /\ x e. W /\ E. n e. ( 0 ... N ) x = ( x cyclShift n ) ) <-> ( ( x e. W /\ x e. W ) /\ E. n e. ( 0 ... N ) x = ( x cyclShift n ) ) ) |
4 |
|
anidm |
|- ( ( x e. W /\ x e. W ) <-> x e. W ) |
5 |
4
|
anbi1i |
|- ( ( ( x e. W /\ x e. W ) /\ E. n e. ( 0 ... N ) x = ( x cyclShift n ) ) <-> ( x e. W /\ E. n e. ( 0 ... N ) x = ( x cyclShift n ) ) ) |
6 |
3 5
|
bitri |
|- ( ( x e. W /\ x e. W /\ E. n e. ( 0 ... N ) x = ( x cyclShift n ) ) <-> ( x e. W /\ E. n e. ( 0 ... N ) x = ( x cyclShift n ) ) ) |
7 |
1 2
|
erclwwlkneq |
|- ( ( x e. _V /\ x e. _V ) -> ( x .~ x <-> ( x e. W /\ x e. W /\ E. n e. ( 0 ... N ) x = ( x cyclShift n ) ) ) ) |
8 |
7
|
el2v |
|- ( x .~ x <-> ( x e. W /\ x e. W /\ E. n e. ( 0 ... N ) x = ( x cyclShift n ) ) ) |
9 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
10 |
9
|
clwwlknwrd |
|- ( x e. ( N ClWWalksN G ) -> x e. Word ( Vtx ` G ) ) |
11 |
|
clwwlknnn |
|- ( x e. ( N ClWWalksN G ) -> N e. NN ) |
12 |
|
cshw0 |
|- ( x e. Word ( Vtx ` G ) -> ( x cyclShift 0 ) = x ) |
13 |
|
nnnn0 |
|- ( N e. NN -> N e. NN0 ) |
14 |
|
0elfz |
|- ( N e. NN0 -> 0 e. ( 0 ... N ) ) |
15 |
13 14
|
syl |
|- ( N e. NN -> 0 e. ( 0 ... N ) ) |
16 |
|
eqcom |
|- ( ( x cyclShift 0 ) = x <-> x = ( x cyclShift 0 ) ) |
17 |
16
|
biimpi |
|- ( ( x cyclShift 0 ) = x -> x = ( x cyclShift 0 ) ) |
18 |
|
oveq2 |
|- ( n = 0 -> ( x cyclShift n ) = ( x cyclShift 0 ) ) |
19 |
18
|
rspceeqv |
|- ( ( 0 e. ( 0 ... N ) /\ x = ( x cyclShift 0 ) ) -> E. n e. ( 0 ... N ) x = ( x cyclShift n ) ) |
20 |
15 17 19
|
syl2anr |
|- ( ( ( x cyclShift 0 ) = x /\ N e. NN ) -> E. n e. ( 0 ... N ) x = ( x cyclShift n ) ) |
21 |
20
|
ex |
|- ( ( x cyclShift 0 ) = x -> ( N e. NN -> E. n e. ( 0 ... N ) x = ( x cyclShift n ) ) ) |
22 |
12 21
|
syl |
|- ( x e. Word ( Vtx ` G ) -> ( N e. NN -> E. n e. ( 0 ... N ) x = ( x cyclShift n ) ) ) |
23 |
10 11 22
|
sylc |
|- ( x e. ( N ClWWalksN G ) -> E. n e. ( 0 ... N ) x = ( x cyclShift n ) ) |
24 |
23 1
|
eleq2s |
|- ( x e. W -> E. n e. ( 0 ... N ) x = ( x cyclShift n ) ) |
25 |
24
|
pm4.71i |
|- ( x e. W <-> ( x e. W /\ E. n e. ( 0 ... N ) x = ( x cyclShift n ) ) ) |
26 |
6 8 25
|
3bitr4ri |
|- ( x e. W <-> x .~ x ) |