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 e. ( ClWWalks ` G ) /\ w e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }
Assertion erclwwlksym 
|- ( x .~ y -> y .~ x )

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 1 erclwwlkeqlen 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x .~ y -> ( # ` x ) = ( # ` y ) ) )
3 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 ) ) ) )
4 simpl2 
 |-  ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) /\ ( # ` x ) = ( # ` y ) ) -> y e. ( ClWWalks ` G ) )
5 simpl1 
 |-  ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) /\ ( # ` x ) = ( # ` y ) ) -> x e. ( ClWWalks ` G ) )
6 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
7 6 clwwlkbp 
 |-  ( y e. ( ClWWalks ` G ) -> ( G e. _V /\ y e. Word ( Vtx ` G ) /\ y =/= (/) ) )
8 7 simp2d 
 |-  ( y e. ( ClWWalks ` G ) -> y e. Word ( Vtx ` G ) )
9 8 ad2antlr 
 |-  ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) /\ ( # ` x ) = ( # ` y ) ) -> y e. Word ( Vtx ` G ) )
10 simpr 
 |-  ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) /\ ( # ` x ) = ( # ` y ) ) -> ( # ` x ) = ( # ` y ) )
11 9 10 cshwcshid 
 |-  ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) /\ ( # ` x ) = ( # ` y ) ) -> ( ( n e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift n ) ) -> E. m e. ( 0 ... ( # ` x ) ) y = ( x cyclShift m ) ) )
12 11 expd 
 |-  ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) /\ ( # ` x ) = ( # ` y ) ) -> ( n e. ( 0 ... ( # ` y ) ) -> ( x = ( y cyclShift n ) -> E. m e. ( 0 ... ( # ` x ) ) y = ( x cyclShift m ) ) ) )
13 12 rexlimdv 
 |-  ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) /\ ( # ` x ) = ( # ` y ) ) -> ( E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) -> E. m e. ( 0 ... ( # ` x ) ) y = ( x cyclShift m ) ) )
14 13 ex 
 |-  ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) -> ( ( # ` x ) = ( # ` y ) -> ( E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) -> E. m e. ( 0 ... ( # ` x ) ) y = ( x cyclShift m ) ) ) )
15 14 com23 
 |-  ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) ) -> ( E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) -> ( ( # ` x ) = ( # ` y ) -> E. m e. ( 0 ... ( # ` x ) ) y = ( x cyclShift m ) ) ) )
16 15 3impia 
 |-  ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) -> ( ( # ` x ) = ( # ` y ) -> E. m e. ( 0 ... ( # ` x ) ) y = ( x cyclShift m ) ) )
17 16 imp 
 |-  ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) /\ ( # ` x ) = ( # ` y ) ) -> E. m e. ( 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 
 |-  ( E. n e. ( 0 ... ( # ` x ) ) y = ( x cyclShift n ) <-> E. m e. ( 0 ... ( # ` x ) ) y = ( x cyclShift m ) )
21 17 20 sylibr 
 |-  ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) /\ ( # ` x ) = ( # ` y ) ) -> E. n e. ( 0 ... ( # ` x ) ) y = ( x cyclShift n ) )
22 4 5 21 3jca 
 |-  ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) /\ ( # ` x ) = ( # ` y ) ) -> ( y e. ( ClWWalks ` G ) /\ x e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` x ) ) y = ( x cyclShift n ) ) )
23 1 erclwwlkeq 
 |-  ( ( y e. _V /\ x e. _V ) -> ( y .~ x <-> ( y e. ( ClWWalks ` G ) /\ x e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` x ) ) y = ( x cyclShift n ) ) ) )
24 23 ancoms 
 |-  ( ( x e. _V /\ y e. _V ) -> ( y .~ x <-> ( y e. ( ClWWalks ` G ) /\ x e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` x ) ) y = ( x cyclShift n ) ) ) )
25 22 24 imbitrrid 
 |-  ( ( x e. _V /\ y e. _V ) -> ( ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) /\ ( # ` x ) = ( # ` y ) ) -> y .~ x ) )
26 25 expd 
 |-  ( ( x e. _V /\ y e. _V ) -> ( ( x e. ( ClWWalks ` G ) /\ y e. ( ClWWalks ` G ) /\ E. n e. ( 0 ... ( # ` y ) ) x = ( y cyclShift n ) ) -> ( ( # ` x ) = ( # ` y ) -> y .~ x ) ) )
27 3 26 sylbid 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x .~ y -> ( ( # ` x ) = ( # ` y ) -> y .~ x ) ) )
28 2 27 mpdd 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x .~ y -> y .~ x ) )
29 28 el2v 
 |-  ( x .~ y -> y .~ x )