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 ⊢ 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
erclwwlkn.r ⊢ ∼ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) }
Assertion erclwwlknsym ( 𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥 )

Proof

Step Hyp Ref Expression
1 erclwwlkn.w ⊢ 𝑊 = ( 𝑁 ClWWalksN 𝐺 )
2 erclwwlkn.r ⊢ ∼ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑡 = ( 𝑢 cyclShift 𝑛 ) ) }
3 1 2 erclwwlkneqlen ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ∼ 𝑦 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) )
4 1 2 erclwwlkneq ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ∼ 𝑦 ↔ ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) )
5 simpl2 ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → 𝑦 ∈ 𝑊 )
6 simpl1 ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → 𝑥 ∈ 𝑊 )
7 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
8 7 clwwlknbp ⊢ ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑥 ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑥 ) = 𝑁 ) )
9 eqcom ⊢ ( ( ♯ ‘ 𝑥 ) = 𝑁 ↔ 𝑁 = ( ♯ ‘ 𝑥 ) )
10 9 biimpi ⊢ ( ( ♯ ‘ 𝑥 ) = 𝑁 → 𝑁 = ( ♯ ‘ 𝑥 ) )
11 8 10 simpl2im ⊢ ( 𝑥 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑁 = ( ♯ ‘ 𝑥 ) )
12 11 1 eleq2s ⊢ ( 𝑥 ∈ 𝑊 → 𝑁 = ( ♯ ‘ 𝑥 ) )
13 12 adantr ⊢ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) → 𝑁 = ( ♯ ‘ 𝑥 ) )
14 13 adantr ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → 𝑁 = ( ♯ ‘ 𝑥 ) )
15 7 clwwlknwrd ⊢ ( 𝑦 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) )
16 15 1 eleq2s ⊢ ( 𝑦 ∈ 𝑊 → 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) )
17 16 adantl ⊢ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) → 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) )
18 17 adantr ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) )
19 18 adantl ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑥 ) ∧ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) )
20 simprr ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑥 ) ∧ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
21 19 20 cshwcshid ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑥 ) ∧ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ∃ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) )
22 oveq2 ⊢ ( 𝑁 = ( ♯ ‘ 𝑥 ) → ( 0 ... 𝑁 ) = ( 0 ... ( ♯ ‘ 𝑥 ) ) )
23 oveq2 ⊢ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( 0 ... ( ♯ ‘ 𝑥 ) ) = ( 0 ... ( ♯ ‘ 𝑦 ) ) )
24 23 adantl ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( 0 ... ( ♯ ‘ 𝑥 ) ) = ( 0 ... ( ♯ ‘ 𝑦 ) ) )
25 22 24 sylan9eq ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑥 ) ∧ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( 0 ... 𝑁 ) = ( 0 ... ( ♯ ‘ 𝑦 ) ) )
26 25 eleq2d ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑥 ) ∧ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( 𝑛 ∈ ( 0 ... 𝑁 ) ↔ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) )
27 26 anbi1d ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑥 ) ∧ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ( 𝑛 ∈ ( 0 ... 𝑁 ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ↔ ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) )
28 22 adantr ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑥 ) ∧ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( 0 ... 𝑁 ) = ( 0 ... ( ♯ ‘ 𝑥 ) ) )
29 28 rexeqdv ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑥 ) ∧ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ↔ ∃ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) )
30 21 27 29 3imtr4d ⊢ ( ( 𝑁 = ( ♯ ‘ 𝑥 ) ∧ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ( 𝑛 ∈ ( 0 ... 𝑁 ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) )
31 14 30 mpancom ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ( 𝑛 ∈ ( 0 ... 𝑁 ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) )
32 31 expd ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( 𝑛 ∈ ( 0 ... 𝑁 ) → ( 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) ) )
33 32 rexlimdv ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) )
34 33 ex ⊢ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) ) )
35 34 com23 ⊢ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ) → ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) ) )
36 35 3impia ⊢ ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) )
37 36 imp ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) )
38 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑥 cyclShift 𝑛 ) = ( 𝑥 cyclShift 𝑚 ) )
39 38 eqeq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) )
40 39 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ ∃ 𝑚 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) )
41 37 40 sylibr ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) )
42 5 6 41 3jca ⊢ ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( 𝑦 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) )
43 1 2 erclwwlkneq ⊢ ( ( 𝑦 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑦 ∼ 𝑥 ↔ ( 𝑦 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ) )
44 43 ancoms ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑦 ∼ 𝑥 ↔ ( 𝑦 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ) )
45 42 44 syl5ibr ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → 𝑦 ∼ 𝑥 ) )
46 45 expd ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( ( 𝑥 ∈ 𝑊 ∧ 𝑦 ∈ 𝑊 ∧ ∃ 𝑛 ∈ ( 0 ... 𝑁 ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → 𝑦 ∼ 𝑥 ) ) )
47 4 46 sylbid ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ∼ 𝑦 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → 𝑦 ∼ 𝑥 ) ) )
48 3 47 mpdd ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥 ) )
49 48 el2v ⊢ ( 𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥 )