erclwwlknsym

Description: .~ is a symmetric 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
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	erclwwlknsym	$⊢ x \underset{˙}{\sim} y \to y \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	1 2	erclwwlkneqlen	$⊢ (x \in V \land y \in V) \to (x \underset{˙}{\sim} y \to \|x\| = \|y\|)$
4	1 2	erclwwlkneq	$⊢ (x \in V \land y \in V) \to (x \underset{˙}{\sim} y \leftrightarrow (x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n))$
5		simpl2	$⊢ ((x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n) \land \|x\| = \|y\|) \to y \in W$
6		simpl1	$⊢ ((x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n) \land \|x\| = \|y\|) \to x \in W$
7		eqid	$⊢ Vtx (G) = Vtx (G)$
8	7	clwwlknbp	$⊢ x \in (N ClWWalksN G) \to (x \in Word Vtx (G) \land \|x\| = N)$
9		eqcom	$⊢ \|x\| = N \leftrightarrow N = \|x\|$
10	9	biimpi	$⊢ \|x\| = N \to N = \|x\|$
11	8 10	simpl2im	$⊢ x \in (N ClWWalksN G) \to N = \|x\|$
12	11 1	eleq2s	$⊢ x \in W \to N = \|x\|$
13	12	adantr	$⊢ (x \in W \land y \in W) \to N = \|x\|$
14	13	adantr	$⊢ ((x \in W \land y \in W) \land \|x\| = \|y\|) \to N = \|x\|$
15	7	clwwlknwrd	$⊢ y \in (N ClWWalksN G) \to y \in Word Vtx (G)$
16	15 1	eleq2s	$⊢ y \in W \to y \in Word Vtx (G)$
17	16	adantl	$⊢ (x \in W \land y \in W) \to y \in Word Vtx (G)$
18	17	adantr	$⊢ ((x \in W \land y \in W) \land \|x\| = \|y\|) \to y \in Word Vtx (G)$
19	18	adantl	$⊢ (N = \|x\| \land ((x \in W \land y \in W) \land \|x\| = \|y\|)) \to y \in Word Vtx (G)$
20		simprr	$⊢ (N = \|x\| \land ((x \in W \land y \in W) \land \|x\| = \|y\|)) \to \|x\| = \|y\|$
21	19 20	cshwcshid	$⊢ (N = \|x\| \land ((x \in W \land y \in W) \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)$
22		oveq2	$⊢ N = \|x\| \to (0 \dots N) = (0 \dots \|x\|)$
23		oveq2	$⊢ \|x\| = \|y\| \to (0 \dots \|x\|) = (0 \dots \|y\|)$
24	23	adantl	$⊢ ((x \in W \land y \in W) \land \|x\| = \|y\|) \to (0 \dots \|x\|) = (0 \dots \|y\|)$
25	22 24	sylan9eq	$⊢ (N = \|x\| \land ((x \in W \land y \in W) \land \|x\| = \|y\|)) \to (0 \dots N) = (0 \dots \|y\|)$
26	25	eleq2d	$⊢ (N = \|x\| \land ((x \in W \land y \in W) \land \|x\| = \|y\|)) \to (n \in (0 \dots N) \leftrightarrow n \in (0 \dots \|y\|))$
27	26	anbi1d	$⊢ (N = \|x\| \land ((x \in W \land y \in W) \land \|x\| = \|y\|)) \to ((n \in (0 \dots N) \land x = y cyclShift n) \leftrightarrow (n \in (0 \dots \|y\|) \land x = y cyclShift n))$
28	22	adantr	$⊢ (N = \|x\| \land ((x \in W \land y \in W) \land \|x\| = \|y\|)) \to (0 \dots N) = (0 \dots \|x\|)$
29	28	rexeqdv	$⊢ (N = \|x\| \land ((x \in W \land y \in W) \land \|x\| = \|y\|)) \to (\exists m \in (0 \dots N) y = x cyclShift m \leftrightarrow \exists m \in (0 \dots \|x\|) y = x cyclShift m)$
30	21 27 29	3imtr4d	$⊢ (N = \|x\| \land ((x \in W \land y \in W) \land \|x\| = \|y\|)) \to ((n \in (0 \dots N) \land x = y cyclShift n) \to \exists m \in (0 \dots N) y = x cyclShift m)$
31	14 30	mpancom	$⊢ ((x \in W \land y \in W) \land \|x\| = \|y\|) \to ((n \in (0 \dots N) \land x = y cyclShift n) \to \exists m \in (0 \dots N) y = x cyclShift m)$
32	31	expd	$⊢ ((x \in W \land y \in W) \land \|x\| = \|y\|) \to (n \in (0 \dots N) \to (x = y cyclShift n \to \exists m \in (0 \dots N) y = x cyclShift m))$
33	32	rexlimdv	$⊢ ((x \in W \land y \in W) \land \|x\| = \|y\|) \to (\exists n \in (0 \dots N) x = y cyclShift n \to \exists m \in (0 \dots N) y = x cyclShift m)$
34	33	ex	$⊢ (x \in W \land y \in W) \to (\|x\| = \|y\| \to (\exists n \in (0 \dots N) x = y cyclShift n \to \exists m \in (0 \dots N) y = x cyclShift m))$
35	34	com23	$⊢ (x \in W \land y \in W) \to (\exists n \in (0 \dots N) x = y cyclShift n \to (\|x\| = \|y\| \to \exists m \in (0 \dots N) y = x cyclShift m))$
36	35	3impia	$⊢ (x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n) \to (\|x\| = \|y\| \to \exists m \in (0 \dots N) y = x cyclShift m)$
37	36	imp	$⊢ ((x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n) \land \|x\| = \|y\|) \to \exists m \in (0 \dots N) y = x cyclShift m$
38		oveq2	$⊢ n = m \to x cyclShift n = x cyclShift m$
39	38	eqeq2d	$⊢ n = m \to (y = x cyclShift n \leftrightarrow y = x cyclShift m)$
40	39	cbvrexvw	$⊢ \exists n \in (0 \dots N) y = x cyclShift n \leftrightarrow \exists m \in (0 \dots N) y = x cyclShift m$
41	37 40	sylibr	$⊢ ((x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n) \land \|x\| = \|y\|) \to \exists n \in (0 \dots N) y = x cyclShift n$
42	5 6 41	3jca	$⊢ ((x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n) \land \|x\| = \|y\|) \to (y \in W \land x \in W \land \exists n \in (0 \dots N) y = x cyclShift n)$
43	1 2	erclwwlkneq	$⊢ (y \in V \land x \in V) \to (y \underset{˙}{\sim} x \leftrightarrow (y \in W \land x \in W \land \exists n \in (0 \dots N) y = x cyclShift n))$
44	43	ancoms	$⊢ (x \in V \land y \in V) \to (y \underset{˙}{\sim} x \leftrightarrow (y \in W \land x \in W \land \exists n \in (0 \dots N) y = x cyclShift n))$
45	42 44	imbitrrid	$⊢ (x \in V \land y \in V) \to (((x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n) \land \|x\| = \|y\|) \to y \underset{˙}{\sim} x)$
46	45	expd	$⊢ (x \in V \land y \in V) \to ((x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n) \to (\|x\| = \|y\| \to y \underset{˙}{\sim} x))$
47	4 46	sylbid	$⊢ (x \in V \land y \in V) \to (x \underset{˙}{\sim} y \to (\|x\| = \|y\| \to y \underset{˙}{\sim} x))$
48	3 47	mpdd	$⊢ (x \in V \land y \in V) \to (x \underset{˙}{\sim} y \to y \underset{˙}{\sim} x)$
49	48	el2v	$⊢ x \underset{˙}{\sim} y \to y \underset{˙}{\sim} x$

Metamath Proof Explorer

Theorem erclwwlknsym

Proof