Theorem erclwwlk

Description: .~ is an equivalence 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	⊢ ∼ = { ⟨ 𝑢 , 𝑤 ⟩ ∣ ( 𝑢 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 𝑢 = ( 𝑤 cyclShift 𝑛 ) ) }
Assertion	erclwwlk	⊢ ∼ Er ( ClWWalks ‘ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		erclwwlk.r	⊢ ∼ = { ⟨ 𝑢 , 𝑤 ⟩ ∣ ( 𝑢 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 𝑢 = ( 𝑤 cyclShift 𝑛 ) ) }
2	1	erclwwlkrel	⊢ Rel ∼
3	1	erclwwlksym	⊢ ( 𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥 )
4	1	erclwwlktr	⊢ ( ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) → 𝑥 ∼ 𝑧 )
5	1	erclwwlkref	⊢ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ↔ 𝑥 ∼ 𝑥 )
6	2 3 4 5	iseri	⊢ ∼ Er ( ClWWalks ‘ 𝐺 )