Metamath Proof Explorer

Theorem erclwwlknref

Description: .~ is a reflexive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 26-Mar-2018) (Revised by AV, 30-Apr-2021) (Proof shortened by AV, 23-Mar-2022)

Ref Expression
Hypotheses erclwwlkn.w 
|- W = ( N ClWWalksN G )
erclwwlkn.r 
|- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
Assertion erclwwlknref 
|- ( x e. W <-> x .~ x )

Proof

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 )