Metamath Proof Explorer


Theorem erclwwlktr

Description: .~ is a transitive 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
Hypothesis erclwwlk.r ˙ = u w | u ClWWalks G w ClWWalks G n 0 w u = w cyclShift n
Assertion erclwwlktr x ˙ y y ˙ z x ˙ z

Proof

Step Hyp Ref Expression
1 erclwwlk.r ˙ = u w | u ClWWalks G w ClWWalks G n 0 w u = w cyclShift n
2 vex x V
3 vex y V
4 vex z V
5 1 erclwwlkeqlen x V y V x ˙ y x = y
6 5 3adant3 x V y V z V x ˙ y x = y
7 1 erclwwlkeqlen y V z V y ˙ z y = z
8 7 3adant1 x V y V z V y ˙ z y = z
9 1 erclwwlkeq y V z V y ˙ z y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n
10 9 3adant1 x V y V z V y ˙ z y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n
11 1 erclwwlkeq x V y V x ˙ y x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n
12 11 3adant3 x V y V z V x ˙ y x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n
13 simpr1 y = z x = y y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n x ClWWalks G
14 simplr2 y = z x = y y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n z ClWWalks G
15 oveq2 n = m y cyclShift n = y cyclShift m
16 15 eqeq2d n = m x = y cyclShift n x = y cyclShift m
17 16 cbvrexvw n 0 y x = y cyclShift n m 0 y x = y cyclShift m
18 oveq2 n = k z cyclShift n = z cyclShift k
19 18 eqeq2d n = k y = z cyclShift n y = z cyclShift k
20 19 cbvrexvw n 0 z y = z cyclShift n k 0 z y = z cyclShift k
21 eqid Vtx G = Vtx G
22 21 clwwlkbp z ClWWalks G G V z Word Vtx G z
23 22 simp2d z ClWWalks G z Word Vtx G
24 23 ad2antlr x ClWWalks G y ClWWalks G z ClWWalks G y = z x = y z Word Vtx G
25 simpr x ClWWalks G y ClWWalks G z ClWWalks G y = z x = y y = z x = y
26 24 25 cshwcsh2id x ClWWalks G y ClWWalks G z ClWWalks G y = z x = y m 0 y x = y cyclShift m k 0 z y = z cyclShift k n 0 z x = z cyclShift n
27 26 exp5l x ClWWalks G y ClWWalks G z ClWWalks G y = z x = y m 0 y x = y cyclShift m k 0 z y = z cyclShift k n 0 z x = z cyclShift n
28 27 imp41 x ClWWalks G y ClWWalks G z ClWWalks G y = z x = y m 0 y x = y cyclShift m k 0 z y = z cyclShift k n 0 z x = z cyclShift n
29 28 rexlimdva x ClWWalks G y ClWWalks G z ClWWalks G y = z x = y m 0 y x = y cyclShift m k 0 z y = z cyclShift k n 0 z x = z cyclShift n
30 29 rexlimdva2 x ClWWalks G y ClWWalks G z ClWWalks G y = z x = y m 0 y x = y cyclShift m k 0 z y = z cyclShift k n 0 z x = z cyclShift n
31 20 30 syl7bi x ClWWalks G y ClWWalks G z ClWWalks G y = z x = y m 0 y x = y cyclShift m n 0 z y = z cyclShift n n 0 z x = z cyclShift n
32 17 31 syl5bi x ClWWalks G y ClWWalks G z ClWWalks G y = z x = y n 0 y x = y cyclShift n n 0 z y = z cyclShift n n 0 z x = z cyclShift n
33 32 exp31 x ClWWalks G y ClWWalks G z ClWWalks G y = z x = y n 0 y x = y cyclShift n n 0 z y = z cyclShift n n 0 z x = z cyclShift n
34 33 com15 n 0 z y = z cyclShift n z ClWWalks G y = z x = y n 0 y x = y cyclShift n x ClWWalks G y ClWWalks G n 0 z x = z cyclShift n
35 34 impcom z ClWWalks G n 0 z y = z cyclShift n y = z x = y n 0 y x = y cyclShift n x ClWWalks G y ClWWalks G n 0 z x = z cyclShift n
36 35 3adant1 y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n y = z x = y n 0 y x = y cyclShift n x ClWWalks G y ClWWalks G n 0 z x = z cyclShift n
37 36 impcom y = z x = y y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n n 0 y x = y cyclShift n x ClWWalks G y ClWWalks G n 0 z x = z cyclShift n
38 37 com13 x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n y = z x = y y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n n 0 z x = z cyclShift n
39 38 3impia x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n y = z x = y y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n n 0 z x = z cyclShift n
40 39 impcom y = z x = y y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n n 0 z x = z cyclShift n
41 13 14 40 3jca y = z x = y y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n x ClWWalks G z ClWWalks G n 0 z x = z cyclShift n
42 1 erclwwlkeq x V z V x ˙ z x ClWWalks G z ClWWalks G n 0 z x = z cyclShift n
43 42 3adant2 x V y V z V x ˙ z x ClWWalks G z ClWWalks G n 0 z x = z cyclShift n
44 41 43 syl5ibrcom y = z x = y y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n x V y V z V x ˙ z
45 44 exp31 y = z x = y y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n x V y V z V x ˙ z
46 45 com24 y = z x = y x V y V z V x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n x ˙ z
47 46 ex y = z x = y x V y V z V x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n x ˙ z
48 47 com4t x V y V z V x ClWWalks G y ClWWalks G n 0 y x = y cyclShift n y = z x = y y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n x ˙ z
49 12 48 sylbid x V y V z V x ˙ y y = z x = y y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n x ˙ z
50 49 com25 x V y V z V y ClWWalks G z ClWWalks G n 0 z y = z cyclShift n y = z x = y x ˙ y x ˙ z
51 10 50 sylbid x V y V z V y ˙ z y = z x = y x ˙ y x ˙ z
52 8 51 mpdd x V y V z V y ˙ z x = y x ˙ y x ˙ z
53 52 com24 x V y V z V x ˙ y x = y y ˙ z x ˙ z
54 6 53 mpdd x V y V z V x ˙ y y ˙ z x ˙ z
55 54 impd x V y V z V x ˙ y y ˙ z x ˙ z
56 2 3 4 55 mp3an x ˙ y y ˙ z x ˙ z