Metamath Proof Explorer


Theorem erclwwlksym

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

Ref Expression
Hypothesis erclwwlk.r ˙ = u w | u ClWWalks G w ClWWalks G n 0 w u = w cyclShift n
Assertion erclwwlksym x ˙ y y ˙ x

Proof

Step Hyp Ref Expression
1 erclwwlk.r ˙ = u w | u ClWWalks G w ClWWalks G n 0 w u = w cyclShift n
2 1 erclwwlkeqlen x V y V x ˙ y x = y
3 1 erclwwlkeq x V y V x ˙ y x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n
4 simpl2 x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n x = y y ClWWalks G
5 simpl1 x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n x = y x ClWWalks G
6 eqid Vtx G = Vtx G
7 6 clwwlkbp y ClWWalks G G V y Word Vtx G y
8 7 simp2d y ClWWalks G y Word Vtx G
9 8 ad2antlr x ClWWalks G y ClWWalks G x = y y Word Vtx G
10 simpr x ClWWalks G y ClWWalks G x = y x = y
11 9 10 cshwcshid x ClWWalks G y ClWWalks G x = y n 0 y x = y cyclShift n m 0 x y = x cyclShift m
12 11 expd x ClWWalks G y ClWWalks G x = y n 0 y x = y cyclShift n m 0 x y = x cyclShift m
13 12 rexlimdv x ClWWalks G y ClWWalks G x = y n 0 y x = y cyclShift n m 0 x y = x cyclShift m
14 13 ex x ClWWalks G y ClWWalks G x = y n 0 y x = y cyclShift n m 0 x y = x cyclShift m
15 14 com23 x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n x = y m 0 x y = x cyclShift m
16 15 3impia x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n x = y m 0 x y = x cyclShift m
17 16 imp x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n x = y m 0 x y = x cyclShift m
18 oveq2 n = m x cyclShift n = x cyclShift m
19 18 eqeq2d n = m y = x cyclShift n y = x cyclShift m
20 19 cbvrexvw n 0 x y = x cyclShift n m 0 x y = x cyclShift m
21 17 20 sylibr x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n x = y n 0 x y = x cyclShift n
22 4 5 21 3jca x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n x = y y ClWWalks G x ClWWalks G n 0 x y = x cyclShift n
23 1 erclwwlkeq y V x V y ˙ x y ClWWalks G x ClWWalks G n 0 x y = x cyclShift n
24 23 ancoms x V y V y ˙ x y ClWWalks G x ClWWalks G n 0 x y = x cyclShift n
25 22 24 syl5ibr x V y V x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n x = y y ˙ x
26 25 expd x V y V x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n x = y y ˙ x
27 3 26 sylbid x V y V x ˙ y x = y y ˙ x
28 2 27 mpdd x V y V x ˙ y y ˙ x
29 28 el2v x ˙ y y ˙ x