Metamath Proof Explorer


Theorem erclwwlknsym

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

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 erclwwlknsym x ˙ y y ˙ 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 1 2 erclwwlkneqlen x V y V x ˙ y x = y
4 1 2 erclwwlkneq x V y V x ˙ y x W y W n 0 N x = y cyclShift n
5 simpl2 x W y W n 0 N x = y cyclShift n x = y y W
6 simpl1 x W y W n 0 N x = y cyclShift n x = y x W
7 eqid Vtx G = Vtx G
8 7 clwwlknbp x N ClWWalksN G x Word Vtx G x = N
9 eqcom x = N N = x
10 9 biimpi x = N N = x
11 8 10 simpl2im x N ClWWalksN G N = x
12 11 1 eleq2s x W N = x
13 12 adantr x W y W N = x
14 13 adantr x W y W x = y N = x
15 7 clwwlknwrd y N ClWWalksN G y Word Vtx G
16 15 1 eleq2s y W y Word Vtx G
17 16 adantl x W y W y Word Vtx G
18 17 adantr x W y W x = y y Word Vtx G
19 18 adantl N = x x W y W x = y y Word Vtx G
20 simprr N = x x W y W x = y x = y
21 19 20 cshwcshid N = x x W y W x = y n 0 y x = y cyclShift n m 0 x y = x cyclShift m
22 oveq2 N = x 0 N = 0 x
23 oveq2 x = y 0 x = 0 y
24 23 adantl x W y W x = y 0 x = 0 y
25 22 24 sylan9eq N = x x W y W x = y 0 N = 0 y
26 25 eleq2d N = x x W y W x = y n 0 N n 0 y
27 26 anbi1d N = x x W y W x = y n 0 N x = y cyclShift n n 0 y x = y cyclShift n
28 22 adantr N = x x W y W x = y 0 N = 0 x
29 28 rexeqdv N = x x W y W x = y m 0 N y = x cyclShift m m 0 x y = x cyclShift m
30 21 27 29 3imtr4d N = x x W y W x = y n 0 N x = y cyclShift n m 0 N y = x cyclShift m
31 14 30 mpancom x W y W x = y n 0 N x = y cyclShift n m 0 N y = x cyclShift m
32 31 expd x W y W x = y n 0 N x = y cyclShift n m 0 N y = x cyclShift m
33 32 rexlimdv x W y W x = y n 0 N x = y cyclShift n m 0 N y = x cyclShift m
34 33 ex x W y W x = y n 0 N x = y cyclShift n m 0 N y = x cyclShift m
35 34 com23 x W y W n 0 N x = y cyclShift n x = y m 0 N y = x cyclShift m
36 35 3impia x W y W n 0 N x = y cyclShift n x = y m 0 N y = x cyclShift m
37 36 imp x W y W n 0 N x = y cyclShift n x = y m 0 N y = x cyclShift m
38 oveq2 n = m x cyclShift n = x cyclShift m
39 38 eqeq2d n = m y = x cyclShift n y = x cyclShift m
40 39 cbvrexvw n 0 N y = x cyclShift n m 0 N y = x cyclShift m
41 37 40 sylibr x W y W n 0 N x = y cyclShift n x = y n 0 N y = x cyclShift n
42 5 6 41 3jca x W y W n 0 N x = y cyclShift n x = y y W x W n 0 N y = x cyclShift n
43 1 2 erclwwlkneq y V x V y ˙ x y W x W n 0 N y = x cyclShift n
44 43 ancoms x V y V y ˙ x y W x W n 0 N y = x cyclShift n
45 42 44 syl5ibr x V y V x W y W n 0 N x = y cyclShift n x = y y ˙ x
46 45 expd x V y V x W y W n 0 N x = y cyclShift n x = y y ˙ x
47 4 46 sylbid x V y V x ˙ y x = y y ˙ x
48 3 47 mpdd x V y V x ˙ y y ˙ x
49 48 el2v x ˙ y y ˙ x