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 W u W n 0 N t = u cyclShift n
Assertion erclwwlknref x W x ˙ x

Proof

Step Hyp Ref Expression
1 erclwwlkn.w W = N ClWWalksN G
2 erclwwlkn.r ˙ = t u | t W u W n 0 N t = u cyclShift n
3 df-3an x W x W n 0 N x = x cyclShift n x W x W n 0 N x = x cyclShift n
4 anidm x W x W x W
5 4 anbi1i x W x W n 0 N x = x cyclShift n x W n 0 N x = x cyclShift n
6 3 5 bitri x W x W n 0 N x = x cyclShift n x W n 0 N x = x cyclShift n
7 1 2 erclwwlkneq x V x V x ˙ x x W x W n 0 N x = x cyclShift n
8 7 el2v x ˙ x x W x W n 0 N x = x cyclShift n
9 eqid Vtx G = Vtx G
10 9 clwwlknwrd x N ClWWalksN G x Word Vtx G
11 clwwlknnn x N ClWWalksN G N
12 cshw0 x Word Vtx G x cyclShift 0 = x
13 nnnn0 N N 0
14 0elfz N 0 0 0 N
15 13 14 syl N 0 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 0 N x = x cyclShift 0 n 0 N x = x cyclShift n
20 15 17 19 syl2anr x cyclShift 0 = x N n 0 N x = x cyclShift n
21 20 ex x cyclShift 0 = x N n 0 N x = x cyclShift n
22 12 21 syl x Word Vtx G N n 0 N x = x cyclShift n
23 10 11 22 sylc x N ClWWalksN G n 0 N x = x cyclShift n
24 23 1 eleq2s x W n 0 N x = x cyclShift n
25 24 pm4.71i x W x W n 0 N x = x cyclShift n
26 6 8 25 3bitr4ri x W x ˙ x