This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )