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 e. W /\ u e. W /\ E. n e. ( 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 e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
3 1 2 erclwwlkneqlen 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x .~ y -> ( # ` x ) = ( # ` y ) ) )
4 1 2 erclwwlkneq 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x .~ y <-> ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) ) )
5 simpl2 
 |-  ( ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) /\ ( # ` x ) = ( # ` y ) ) -> y e. W )
6 simpl1 
 |-  ( ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) /\ ( # ` x ) = ( # ` y ) ) -> x e. W )
7 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
8 7 clwwlknbp 
 |-  ( x e. ( N ClWWalksN G ) -> ( x e. Word ( Vtx ` G ) /\ ( # ` x ) = N ) )
9 eqcom 
 |-  ( ( # ` x ) = N <-> N = ( # ` x ) )
10 9 biimpi 
 |-  ( ( # ` x ) = N -> N = ( # ` x ) )
11 8 10 simpl2im 
 |-  ( x e. ( N ClWWalksN G ) -> N = ( # ` x ) )
12 11 1 eleq2s 
 |-  ( x e. W -> N = ( # ` x ) )
13 12 adantr 
 |-  ( ( x e. W /\ y e. W ) -> N = ( # ` x ) )
14 13 adantr 
 |-  ( ( ( x e. W /\ y e. W ) /\ ( # ` x ) = ( # ` y ) ) -> N = ( # ` x ) )
15 7 clwwlknwrd 
 |-  ( y e. ( N ClWWalksN G ) -> y e. Word ( Vtx ` G ) )
16 15 1 eleq2s 
 |-  ( y e. W -> y e. Word ( Vtx ` G ) )
17 16 adantl 
 |-  ( ( x e. W /\ y e. W ) -> y e. Word ( Vtx ` G ) )
18 17 adantr 
 |-  ( ( ( x e. W /\ y e. W ) /\ ( # ` x ) = ( # ` y ) ) -> y e. Word ( Vtx ` G ) )
19 18 adantl 
 |-  ( ( N = ( # ` x ) /\ ( ( x e. W /\ y e. W ) /\ ( # ` x ) = ( # ` y ) ) ) -> y e. Word ( Vtx ` G ) )
20 simprr 
 |-  ( ( N = ( # ` x ) /\ ( ( x e. W /\ y e. W ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( # ` x ) = ( # ` y ) )
21 19 20 cshwcshid 
 |-  ( ( N = ( # ` x ) /\ ( ( x e. W /\ y e. W ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( ( n e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift n ) ) -> E. m e. ( 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 e. W /\ y e. W ) /\ ( # ` x ) = ( # ` y ) ) -> ( 0 ... ( # ` x ) ) = ( 0 ... ( # ` y ) ) )
25 22 24 sylan9eq 
 |-  ( ( N = ( # ` x ) /\ ( ( x e. W /\ y e. W ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( 0 ... N ) = ( 0 ... ( # ` y ) ) )
26 25 eleq2d 
 |-  ( ( N = ( # ` x ) /\ ( ( x e. W /\ y e. W ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( n e. ( 0 ... N ) <-> n e. ( 0 ... ( # ` y ) ) ) )
27 26 anbi1d 
 |-  ( ( N = ( # ` x ) /\ ( ( x e. W /\ y e. W ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( ( n e. ( 0 ... N ) /\ x = ( y cyclShift n ) ) <-> ( n e. ( 0 ... ( # ` y ) ) /\ x = ( y cyclShift n ) ) ) )
28 22 adantr 
 |-  ( ( N = ( # ` x ) /\ ( ( x e. W /\ y e. W ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( 0 ... N ) = ( 0 ... ( # ` x ) ) )
29 28 rexeqdv 
 |-  ( ( N = ( # ` x ) /\ ( ( x e. W /\ y e. W ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( E. m e. ( 0 ... N ) y = ( x cyclShift m ) <-> E. m e. ( 0 ... ( # ` x ) ) y = ( x cyclShift m ) ) )
30 21 27 29 3imtr4d 
 |-  ( ( N = ( # ` x ) /\ ( ( x e. W /\ y e. W ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( ( n e. ( 0 ... N ) /\ x = ( y cyclShift n ) ) -> E. m e. ( 0 ... N ) y = ( x cyclShift m ) ) )
31 14 30 mpancom 
 |-  ( ( ( x e. W /\ y e. W ) /\ ( # ` x ) = ( # ` y ) ) -> ( ( n e. ( 0 ... N ) /\ x = ( y cyclShift n ) ) -> E. m e. ( 0 ... N ) y = ( x cyclShift m ) ) )
32 31 expd 
 |-  ( ( ( x e. W /\ y e. W ) /\ ( # ` x ) = ( # ` y ) ) -> ( n e. ( 0 ... N ) -> ( x = ( y cyclShift n ) -> E. m e. ( 0 ... N ) y = ( x cyclShift m ) ) ) )
33 32 rexlimdv 
 |-  ( ( ( x e. W /\ y e. W ) /\ ( # ` x ) = ( # ` y ) ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> E. m e. ( 0 ... N ) y = ( x cyclShift m ) ) )
34 33 ex 
 |-  ( ( x e. W /\ y e. W ) -> ( ( # ` x ) = ( # ` y ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> E. m e. ( 0 ... N ) y = ( x cyclShift m ) ) ) )
35 34 com23 
 |-  ( ( x e. W /\ y e. W ) -> ( E. n e. ( 0 ... N ) x = ( y cyclShift n ) -> ( ( # ` x ) = ( # ` y ) -> E. m e. ( 0 ... N ) y = ( x cyclShift m ) ) ) )
36 35 3impia 
 |-  ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) -> ( ( # ` x ) = ( # ` y ) -> E. m e. ( 0 ... N ) y = ( x cyclShift m ) ) )
37 36 imp 
 |-  ( ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) /\ ( # ` x ) = ( # ` y ) ) -> E. m e. ( 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 
 |-  ( E. n e. ( 0 ... N ) y = ( x cyclShift n ) <-> E. m e. ( 0 ... N ) y = ( x cyclShift m ) )
41 37 40 sylibr 
 |-  ( ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) /\ ( # ` x ) = ( # ` y ) ) -> E. n e. ( 0 ... N ) y = ( x cyclShift n ) )
42 5 6 41 3jca 
 |-  ( ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) /\ ( # ` x ) = ( # ` y ) ) -> ( y e. W /\ x e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) )
43 1 2 erclwwlkneq 
 |-  ( ( y e. _V /\ x e. _V ) -> ( y .~ x <-> ( y e. W /\ x e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) ) )
44 43 ancoms 
 |-  ( ( x e. _V /\ y e. _V ) -> ( y .~ x <-> ( y e. W /\ x e. W /\ E. n e. ( 0 ... N ) y = ( x cyclShift n ) ) ) )
45 42 44 imbitrrid 
 |-  ( ( x e. _V /\ y e. _V ) -> ( ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) /\ ( # ` x ) = ( # ` y ) ) -> y .~ x ) )
46 45 expd 
 |-  ( ( x e. _V /\ y e. _V ) -> ( ( x e. W /\ y e. W /\ E. n e. ( 0 ... N ) x = ( y cyclShift n ) ) -> ( ( # ` x ) = ( # ` y ) -> y .~ x ) ) )
47 4 46 sylbid 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x .~ y -> ( ( # ` x ) = ( # ` y ) -> y .~ x ) ) )
48 3 47 mpdd 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x .~ y -> y .~ x ) )
49 48 el2v 
 |-  ( x .~ y -> y .~ x )