Metamath Proof Explorer


Theorem erclwwlkref

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

Ref Expression
Hypothesis erclwwlk.r
|- .~ = { <. u , w >. | ( u e. ( ClWWalks ` G ) /\ w e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }
Assertion erclwwlkref
|- ( x e. ( ClWWalks ` G ) <-> x .~ x )

Proof

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 )