This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ \underset{˙}{\sim} = \{⟨u, w⟩ \| (u \in ClWWalks (G) \land w \in ClWWalks (G) \land \exists n \in (0 \dots \|w\|) u = w cyclShift n)\}$
	Assertion	erclwwlk	$⊢ \underset{˙}{\sim} Er ClWWalks (G)$

Proof

Step	Hyp	Ref	Expression
1		erclwwlk.r	$⊢ \underset{˙}{\sim} = \{⟨u, w⟩ \| (u \in ClWWalks (G) \land w \in ClWWalks (G) \land \exists n \in (0 \dots \|w\|) u = w cyclShift n)\}$
2	1	erclwwlkrel	$⊢ Rel \underset{˙}{\sim}$
3	1	erclwwlksym	$⊢ x \underset{˙}{\sim} y \to y \underset{˙}{\sim} x$
4	1	erclwwlktr	$⊢ (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z) \to x \underset{˙}{\sim} z$
5	1	erclwwlkref	$⊢ x \in ClWWalks (G) \leftrightarrow x \underset{˙}{\sim} x$
6	2 3 4 5	iseri	$⊢ \underset{˙}{\sim} Er ClWWalks (G)$