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 )