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 ⊢ ∼ = { ⟨ 𝑢 , 𝑤 ⟩ ∣ ( 𝑢 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 𝑢 = ( 𝑤 cyclShift 𝑛 ) ) }
Assertion erclwwlksym ( 𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥 )

Proof

Step Hyp Ref Expression
1 erclwwlk.r ⊢ ∼ = { ⟨ 𝑢 , 𝑤 ⟩ ∣ ( 𝑢 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 𝑢 = ( 𝑤 cyclShift 𝑛 ) ) }
2 1 erclwwlkeqlen ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ∼ 𝑦 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) )
3 1 erclwwlkeq ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ∼ 𝑦 ↔ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) )
4 simpl2 ⊢ ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) )
5 simpl1 ⊢ ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) )
6 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
7 6 clwwlkbp ⊢ ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑦 ≠ ∅ ) )
8 7 simp2d ⊢ ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) → 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) )
9 8 ad2antlr ⊢ ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → 𝑦 ∈ Word ( Vtx ‘ 𝐺 ) )
10 simpr ⊢ ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
11 9 10 cshwcshid ⊢ ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ∃ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) )
12 11 expd ⊢ ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ∃ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) ) )
13 12 rexlimdv ⊢ ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ∃ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) )
14 13 ex ⊢ ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ∃ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) ) )
15 14 com23 ⊢ ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ∃ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) ) )
16 15 3impia ⊢ ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ∃ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) )
17 16 imp ⊢ ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ∃ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) )
18 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑥 cyclShift 𝑛 ) = ( 𝑥 cyclShift 𝑚 ) )
19 18 eqeq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ 𝑦 = ( 𝑥 cyclShift 𝑚 ) ) )
20 19 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ↔ ∃ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑚 ) )
21 17 20 sylibr ⊢ ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) )
22 4 5 21 3jca ⊢ ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) )
23 1 erclwwlkeq ⊢ ( ( 𝑦 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑦 ∼ 𝑥 ↔ ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ) )
24 23 ancoms ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑦 ∼ 𝑥 ↔ ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑥 ) ) 𝑦 = ( 𝑥 cyclShift 𝑛 ) ) ) )
25 22 24 imbitrrid ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → 𝑦 ∼ 𝑥 ) )
26 25 expd ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → 𝑦 ∼ 𝑥 ) ) )
27 3 26 sylbid ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ∼ 𝑦 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → 𝑦 ∼ 𝑥 ) ) )
28 2 27 mpdd ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥 ) )
29 28 el2v ⊢ ( 𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥 )