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	$⊢ \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	erclwwlksym	$⊢ x \underset{˙}{\sim} y \to y \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	1	erclwwlkeqlen	$⊢ (x \in V \land y \in V) \to (x \underset{˙}{\sim} y \to \|x\| = \|y\|)$
3	1	erclwwlkeq	$⊢ (x \in V \land y \in V) \to (x \underset{˙}{\sim} y \leftrightarrow (x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n))$
4		simpl2	$⊢ ((x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n) \land \|x\| = \|y\|) \to y \in ClWWalks (G)$
5		simpl1	$⊢ ((x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n) \land \|x\| = \|y\|) \to x \in ClWWalks (G)$
6		eqid	$⊢ Vtx (G) = Vtx (G)$
7	6	clwwlkbp	$⊢ y \in ClWWalks (G) \to (G \in V \land y \in Word Vtx (G) \land y \neq \emptyset)$
8	7	simp2d	$⊢ y \in ClWWalks (G) \to y \in Word Vtx (G)$
9	8	ad2antlr	$⊢ ((x \in ClWWalks (G) \land y \in ClWWalks (G)) \land \|x\| = \|y\|) \to y \in Word Vtx (G)$
10		simpr	$⊢ ((x \in ClWWalks (G) \land y \in ClWWalks (G)) \land \|x\| = \|y\|) \to \|x\| = \|y\|$
11	9 10	cshwcshid	$⊢ ((x \in ClWWalks (G) \land y \in ClWWalks (G)) \land \|x\| = \|y\|) \to ((n \in (0 \dots \|y\|) \land x = y cyclShift n) \to \exists m \in (0 \dots \|x\|) y = x cyclShift m)$
12	11	expd	$⊢ ((x \in ClWWalks (G) \land y \in ClWWalks (G)) \land \|x\| = \|y\|) \to (n \in (0 \dots \|y\|) \to (x = y cyclShift n \to \exists m \in (0 \dots \|x\|) y = x cyclShift m))$
13	12	rexlimdv	$⊢ ((x \in ClWWalks (G) \land y \in ClWWalks (G)) \land \|x\| = \|y\|) \to (\exists n \in (0 \dots \|y\|) x = y cyclShift n \to \exists m \in (0 \dots \|x\|) y = x cyclShift m)$
14	13	ex	$⊢ (x \in ClWWalks (G) \land y \in ClWWalks (G)) \to (\|x\| = \|y\| \to (\exists n \in (0 \dots \|y\|) x = y cyclShift n \to \exists m \in (0 \dots \|x\|) y = x cyclShift m))$
15	14	com23	$⊢ (x \in ClWWalks (G) \land y \in ClWWalks (G)) \to (\exists n \in (0 \dots \|y\|) x = y cyclShift n \to (\|x\| = \|y\| \to \exists m \in (0 \dots \|x\|) y = x cyclShift m))$
16	15	3impia	$⊢ (x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n) \to (\|x\| = \|y\| \to \exists m \in (0 \dots \|x\|) y = x cyclShift m)$
17	16	imp	$⊢ ((x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n) \land \|x\| = \|y\|) \to \exists m \in (0 \dots \|x\|) y = x cyclShift m$
18		oveq2	$⊢ n = m \to x cyclShift n = x cyclShift m$
19	18	eqeq2d	$⊢ n = m \to (y = x cyclShift n \leftrightarrow y = x cyclShift m)$
20	19	cbvrexvw	$⊢ \exists n \in (0 \dots \|x\|) y = x cyclShift n \leftrightarrow \exists m \in (0 \dots \|x\|) y = x cyclShift m$
21	17 20	sylibr	$⊢ ((x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n) \land \|x\| = \|y\|) \to \exists n \in (0 \dots \|x\|) y = x cyclShift n$
22	4 5 21	3jca	$⊢ ((x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n) \land \|x\| = \|y\|) \to (y \in ClWWalks (G) \land x \in ClWWalks (G) \land \exists n \in (0 \dots \|x\|) y = x cyclShift n)$
23	1	erclwwlkeq	$⊢ (y \in V \land x \in V) \to (y \underset{˙}{\sim} x \leftrightarrow (y \in ClWWalks (G) \land x \in ClWWalks (G) \land \exists n \in (0 \dots \|x\|) y = x cyclShift n))$
24	23	ancoms	$⊢ (x \in V \land y \in V) \to (y \underset{˙}{\sim} x \leftrightarrow (y \in ClWWalks (G) \land x \in ClWWalks (G) \land \exists n \in (0 \dots \|x\|) y = x cyclShift n))$
25	22 24	syl5ibr	$⊢ (x \in V \land y \in V) \to (((x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n) \land \|x\| = \|y\|) \to y \underset{˙}{\sim} x)$
26	25	expd	$⊢ (x \in V \land y \in V) \to ((x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n) \to (\|x\| = \|y\| \to y \underset{˙}{\sim} x))$
27	3 26	sylbid	$⊢ (x \in V \land y \in V) \to (x \underset{˙}{\sim} y \to (\|x\| = \|y\| \to y \underset{˙}{\sim} x))$
28	2 27	mpdd	$⊢ (x \in V \land y \in V) \to (x \underset{˙}{\sim} y \to y \underset{˙}{\sim} x)$
29	28	el2v	$⊢ x \underset{˙}{\sim} y \to y \underset{˙}{\sim} x$

Metamath Proof Explorer

Theorem erclwwlksym

Proof