erclwwlknref

Description: .~ is a reflexive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 26-Mar-2018) (Revised by AV, 30-Apr-2021) (Proof shortened by AV, 23-Mar-2022)

	Ref	Expression
Hypotheses	erclwwlkn.w	$⊢ W = N ClWWalksN G$
	erclwwlkn.r	$⊢ \underset{˙}{\sim} = \{⟨t, u⟩ \| (t \in W \land u \in W \land \exists n \in (0 \dots N) t = u cyclShift n)\}$
Assertion	erclwwlknref	$⊢ x \in W \leftrightarrow x \underset{˙}{\sim} x$

Proof

Step	Hyp	Ref	Expression
1		erclwwlkn.w	$⊢ W = N ClWWalksN G$
2		erclwwlkn.r	$⊢ \underset{˙}{\sim} = \{⟨t, u⟩ \| (t \in W \land u \in W \land \exists n \in (0 \dots N) t = u cyclShift n)\}$
3		df-3an	$⊢ (x \in W \land x \in W \land \exists n \in (0 \dots N) x = x cyclShift n) \leftrightarrow ((x \in W \land x \in W) \land \exists n \in (0 \dots N) x = x cyclShift n)$
4		anidm	$⊢ (x \in W \land x \in W) \leftrightarrow x \in W$
5	4	anbi1i	$⊢ ((x \in W \land x \in W) \land \exists n \in (0 \dots N) x = x cyclShift n) \leftrightarrow (x \in W \land \exists n \in (0 \dots N) x = x cyclShift n)$
6	3 5	bitri	$⊢ (x \in W \land x \in W \land \exists n \in (0 \dots N) x = x cyclShift n) \leftrightarrow (x \in W \land \exists n \in (0 \dots N) x = x cyclShift n)$
7	1 2	erclwwlkneq	$⊢ (x \in V \land x \in V) \to (x \underset{˙}{\sim} x \leftrightarrow (x \in W \land x \in W \land \exists n \in (0 \dots N) x = x cyclShift n))$
8	7	el2v	$⊢ x \underset{˙}{\sim} x \leftrightarrow (x \in W \land x \in W \land \exists n \in (0 \dots N) x = x cyclShift n)$
9		eqid	$⊢ Vtx (G) = Vtx (G)$
10	9	clwwlknwrd	$⊢ x \in (N ClWWalksN G) \to x \in Word Vtx (G)$
11		clwwlknnn	$⊢ x \in (N ClWWalksN G) \to N \in ℕ$
12		cshw0	$⊢ x \in Word Vtx (G) \to x cyclShift 0 = x$
13		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
14		0elfz	$⊢ N \in ℕ_{0} \to 0 \in (0 \dots N)$
15	13 14	syl	$⊢ N \in ℕ \to 0 \in (0 \dots N)$
16		eqcom	$⊢ x cyclShift 0 = x \leftrightarrow x = x cyclShift 0$
17	16	biimpi	$⊢ x cyclShift 0 = x \to x = x cyclShift 0$
18		oveq2	$⊢ n = 0 \to x cyclShift n = x cyclShift 0$
19	18	rspceeqv	$⊢ (0 \in (0 \dots N) \land x = x cyclShift 0) \to \exists n \in (0 \dots N) x = x cyclShift n$
20	15 17 19	syl2anr	$⊢ (x cyclShift 0 = x \land N \in ℕ) \to \exists n \in (0 \dots N) x = x cyclShift n$
21	20	ex	$⊢ x cyclShift 0 = x \to (N \in ℕ \to \exists n \in (0 \dots N) x = x cyclShift n)$
22	12 21	syl	$⊢ x \in Word Vtx (G) \to (N \in ℕ \to \exists n \in (0 \dots N) x = x cyclShift n)$
23	10 11 22	sylc	$⊢ x \in (N ClWWalksN G) \to \exists n \in (0 \dots N) x = x cyclShift n$
24	23 1	eleq2s	$⊢ x \in W \to \exists n \in (0 \dots N) x = x cyclShift n$
25	24	pm4.71i	$⊢ x \in W \leftrightarrow (x \in W \land \exists n \in (0 \dots N) x = x cyclShift n)$
26	6 8 25	3bitr4ri	$⊢ x \in W \leftrightarrow x \underset{˙}{\sim} x$

Metamath Proof Explorer

Theorem erclwwlknref

Proof