erclwwlkref

Description: .~ is a reflexive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 25-Mar-2018) (Revised by AV, 29-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	erclwwlkref	$⊢ x \in ClWWalks (G) \leftrightarrow x \underset{˙}{\sim} x$

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		anidm	$⊢ (x \in ClWWalks (G) \land x \in ClWWalks (G)) \leftrightarrow x \in ClWWalks (G)$
3	2	anbi1i	$⊢ ((x \in ClWWalks (G) \land x \in ClWWalks (G)) \land \exists n \in (0 \dots \|x\|) x = x cyclShift n) \leftrightarrow (x \in ClWWalks (G) \land \exists n \in (0 \dots \|x\|) x = x cyclShift n)$
4		df-3an	$⊢ (x \in ClWWalks (G) \land x \in ClWWalks (G) \land \exists n \in (0 \dots \|x\|) x = x cyclShift n) \leftrightarrow ((x \in ClWWalks (G) \land x \in ClWWalks (G)) \land \exists n \in (0 \dots \|x\|) x = x cyclShift n)$
5		eqid	$⊢ Vtx (G) = Vtx (G)$
6	5	clwwlkbp	$⊢ x \in ClWWalks (G) \to (G \in V \land x \in Word Vtx (G) \land x \neq \emptyset)$
7		cshw0	$⊢ x \in Word Vtx (G) \to x cyclShift 0 = x$
8		0nn0	$⊢ 0 \in ℕ_{0}$
9	8	a1i	$⊢ x \in Word Vtx (G) \to 0 \in ℕ_{0}$
10		lencl	$⊢ x \in Word Vtx (G) \to \|x\| \in ℕ_{0}$
11		hashge0	$⊢ x \in Word Vtx (G) \to 0 \leq \|x\|$
12		elfz2nn0	$⊢ 0 \in (0 \dots \|x\|) \leftrightarrow (0 \in ℕ_{0} \land \|x\| \in ℕ_{0} \land 0 \leq \|x\|)$
13	9 10 11 12	syl3anbrc	$⊢ x \in Word Vtx (G) \to 0 \in (0 \dots \|x\|)$
14		eqcom	$⊢ x cyclShift 0 = x \leftrightarrow x = x cyclShift 0$
15	14	biimpi	$⊢ x cyclShift 0 = x \to x = x cyclShift 0$
16		oveq2	$⊢ n = 0 \to x cyclShift n = x cyclShift 0$
17	16	rspceeqv	$⊢ (0 \in (0 \dots \|x\|) \land x = x cyclShift 0) \to \exists n \in (0 \dots \|x\|) x = x cyclShift n$
18	13 15 17	syl2an	$⊢ (x \in Word Vtx (G) \land x cyclShift 0 = x) \to \exists n \in (0 \dots \|x\|) x = x cyclShift n$
19	7 18	mpdan	$⊢ x \in Word Vtx (G) \to \exists n \in (0 \dots \|x\|) x = x cyclShift n$
20	19	3ad2ant2	$⊢ (G \in V \land x \in Word Vtx (G) \land x \neq \emptyset) \to \exists n \in (0 \dots \|x\|) x = x cyclShift n$
21	6 20	syl	$⊢ x \in ClWWalks (G) \to \exists n \in (0 \dots \|x\|) x = x cyclShift n$
22	21	pm4.71i	$⊢ x \in ClWWalks (G) \leftrightarrow (x \in ClWWalks (G) \land \exists n \in (0 \dots \|x\|) x = x cyclShift n)$
23	3 4 22	3bitr4ri	$⊢ x \in ClWWalks (G) \leftrightarrow (x \in ClWWalks (G) \land x \in ClWWalks (G) \land \exists n \in (0 \dots \|x\|) x = x cyclShift n)$
24	1	erclwwlkeq	$⊢ (x \in V \land x \in V) \to (x \underset{˙}{\sim} x \leftrightarrow (x \in ClWWalks (G) \land x \in ClWWalks (G) \land \exists n \in (0 \dots \|x\|) x = x cyclShift n))$
25	24	el2v	$⊢ x \underset{˙}{\sim} x \leftrightarrow (x \in ClWWalks (G) \land x \in ClWWalks (G) \land \exists n \in (0 \dots \|x\|) x = x cyclShift n)$
26	23 25	bitr4i	$⊢ x \in ClWWalks (G) \leftrightarrow x \underset{˙}{\sim} x$

Metamath Proof Explorer

Theorem erclwwlkref

Proof