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 e. ( ClWWalks ` G ) /\ w e. ( ClWWalks ` G ) /\ E. n e. ( 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 e. ( ClWWalks ` G ) /\ w e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }
2 vex 
 |-  x e. _V
3 vex 
 |-  y e. _V
4 vex 
 |-  z e. _V
5 1 erclwwlkeqlen 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x .~ y -> ( # ` x ) = ( # ` y ) ) )
6 5 3adant3 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ y -> ( # ` x ) = ( # ` y ) ) )
7 1 erclwwlkeqlen 
 |-  ( ( y e. _V /\ z e. _V ) -> ( y .~ z -> ( # ` y ) = ( # ` z ) ) )
8 7 3adant1 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( y .~ z -> ( # ` y ) = ( # ` z ) ) )
9 1 erclwwlkeq 
 |-  ( ( y e. _V /\ z e. _V ) -> ( y .~ z <-> ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) ) )
10 9 3adant1 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( y .~ z <-> ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) ) )
11 1 erclwwlkeq 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x .~ y <-> ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) ) )
12 11 3adant3 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ y <-> ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) ) )
13 simpr1 
 |-  ( ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) ) /\ ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) ) -> x e. ( ClWWalks ` G ) )
14 simplr2 
 |-  ( ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) ) /\ ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) ) -> z e. ( 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 
 |-  ( E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) <-> E. m e. ( 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 
 |-  ( E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) <-> E. k e. ( 0 ... ( # ` z ) ) y = ( z cyclShift k ) )
21 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
22 21 clwwlkbp 
 |-  ( z e. ( ClWWalks ` G ) -> ( G e. _V /\ z e. Word ( Vtx ` G ) /\ z =/= (/) ) )
23 22 simp2d 
 |-  ( z e. ( ClWWalks ` G ) -> z e. Word ( Vtx ` G ) )
24 23 ad2antlr 
 |-  ( ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) /\ z e. ( ClWWalks ` G ) ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> z e. Word ( Vtx ` G ) )
25 simpr 
 |-  ( ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) /\ z e. ( ClWWalks ` G ) ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) )
26 24 25 cshwcsh2id 
 |-  ( ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) /\ z e. ( ClWWalks ` G ) ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( ( ( m e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift m ) ) /\ ( k e. ( 0 ... ( # ` z ) ) /\ y = ( z cyclShift k ) ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) )
27 26 exp5l 
 |-  ( ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) /\ z e. ( ClWWalks ` G ) ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( m e. ( 0 ... ( # ` y ) ) -> ( x = ( y cyclShift m ) -> ( k e. ( 0 ... ( # ` z ) ) -> ( y = ( z cyclShift k ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) ) ) ) )
28 27 imp41 
 |-  ( ( ( ( ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) /\ z e. ( ClWWalks ` G ) ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) /\ m e. ( 0 ... ( # ` y ) ) ) /\ x = ( y cyclShift m ) ) /\ k e. ( 0 ... ( # ` z ) ) ) -> ( y = ( z cyclShift k ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) )
29 28 rexlimdva 
 |-  ( ( ( ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) /\ z e. ( ClWWalks ` G ) ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) /\ m e. ( 0 ... ( # ` y ) ) ) /\ x = ( y cyclShift m ) ) -> ( E. k e. ( 0 ... ( # ` z ) ) y = ( z cyclShift k ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) )
30 29 rexlimdva2 
 |-  ( ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) /\ z e. ( ClWWalks ` G ) ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( E. m e. ( 0 ... ( # ` y ) ) x = ( y cyclShift m ) -> ( E. k e. ( 0 ... ( # ` z ) ) y = ( z cyclShift k ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) ) )
31 20 30 syl7bi 
 |-  ( ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) /\ z e. ( ClWWalks ` G ) ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( E. m e. ( 0 ... ( # ` y ) ) x = ( y cyclShift m ) -> ( E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) ) )
32 17 31 biimtrid 
 |-  ( ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) /\ z e. ( ClWWalks ` G ) ) /\ ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) -> ( E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) ) )
33 32 exp31 
 |-  ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) -> ( z e. ( ClWWalks ` G ) -> ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) -> ( E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) ) ) ) )
34 33 com15 
 |-  ( E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) -> ( z e. ( ClWWalks ` G ) -> ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) -> ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) ) ) ) )
35 34 impcom 
 |-  ( ( z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) -> ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) -> ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) ) ) )
36 35 3adant1 
 |-  ( ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) -> ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) -> ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) ) ) )
37 36 impcom 
 |-  ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) ) -> ( E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) -> ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) ) )
38 37 com13 
 |-  ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) -> ( E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) -> ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) ) )
39 38 3impia 
 |-  ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) -> ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) )
40 39 impcom 
 |-  ( ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) ) /\ ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) ) -> E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) )
41 13 14 40 3jca 
 |-  ( ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) ) /\ ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) ) -> ( x e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) )
42 1 erclwwlkeq 
 |-  ( ( x e. _V /\ z e. _V ) -> ( x .~ z <-> ( x e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) ) )
43 42 3adant2 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ z <-> ( x e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) x = ( z cyclShift n ) ) ) )
44 41 43 syl5ibrcom 
 |-  ( ( ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) /\ ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) ) /\ ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) ) -> ( ( x e. _V /\ y e. _V /\ z e. _V ) -> x .~ z ) )
45 44 exp31 
 |-  ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) -> ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) -> ( ( x e. _V /\ y e. _V /\ z e. _V ) -> x .~ z ) ) ) )
46 45 com24 
 |-  ( ( ( # ` y ) = ( # ` z ) /\ ( # ` x ) = ( # ` y ) ) -> ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) -> ( ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) -> x .~ z ) ) ) )
47 46 ex 
 |-  ( ( # ` y ) = ( # ` z ) -> ( ( # ` x ) = ( # ` y ) -> ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) -> ( ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) -> x .~ z ) ) ) ) )
48 47 com4t 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) -> ( ( # ` y ) = ( # ` z ) -> ( ( # ` x ) = ( # ` y ) -> ( ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) -> x .~ z ) ) ) ) )
49 12 48 sylbid 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ y -> ( ( # ` y ) = ( # ` z ) -> ( ( # ` x ) = ( # ` y ) -> ( ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) -> x .~ z ) ) ) ) )
50 49 com25 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( ( y e. ( ClWWalks ` G ) /\ z e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` z ) ) y = ( z cyclShift n ) ) -> ( ( # ` y ) = ( # ` z ) -> ( ( # ` x ) = ( # ` y ) -> ( x .~ y -> x .~ z ) ) ) ) )
51 10 50 sylbid 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( y .~ z -> ( ( # ` y ) = ( # ` z ) -> ( ( # ` x ) = ( # ` y ) -> ( x .~ y -> x .~ z ) ) ) ) )
52 8 51 mpdd 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( y .~ z -> ( ( # ` x ) = ( # ` y ) -> ( x .~ y -> x .~ z ) ) ) )
53 52 com24 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ y -> ( ( # ` x ) = ( # ` y ) -> ( y .~ z -> x .~ z ) ) ) )
54 6 53 mpdd 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( x .~ y -> ( y .~ z -> x .~ z ) ) )
55 54 impd 
 |-  ( ( x e. _V /\ y e. _V /\ z e. _V ) -> ( ( x .~ y /\ y .~ z ) -> x .~ z ) )
56 2 3 4 55 mp3an 
 |-  ( ( x .~ y /\ y .~ z ) -> x .~ z )