erclwwlkntr

Description: .~ is a transitive 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	erclwwlkntr	$⊢ (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z) \to x \underset{˙}{\sim} z$

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		vex	$⊢ x \in V$
4		vex	$⊢ y \in V$
5		vex	$⊢ z \in V$
6	1 2	erclwwlkneqlen	$⊢ (x \in V \land y \in V) \to (x \underset{˙}{\sim} y \to \|x\| = \|y\|)$
7	6	3adant3	$⊢ (x \in V \land y \in V \land z \in V) \to (x \underset{˙}{\sim} y \to \|x\| = \|y\|)$
8	1 2	erclwwlkneqlen	$⊢ (y \in V \land z \in V) \to (y \underset{˙}{\sim} z \to \|y\| = \|z\|)$
9	8	3adant1	$⊢ (x \in V \land y \in V \land z \in V) \to (y \underset{˙}{\sim} z \to \|y\| = \|z\|)$
10	1 2	erclwwlkneq	$⊢ (y \in V \land z \in V) \to (y \underset{˙}{\sim} z \leftrightarrow (y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n))$
11	10	3adant1	$⊢ (x \in V \land y \in V \land z \in V) \to (y \underset{˙}{\sim} z \leftrightarrow (y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n))$
12	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))$
13	12	3adant3	$⊢ (x \in V \land y \in V \land z \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))$
14		simpr1	$⊢ (((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n)) \land (x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n)) \to x \in W$
15		simplr2	$⊢ (((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n)) \land (x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n)) \to z \in W$
16		oveq2	$⊢ n = m \to y cyclShift n = y cyclShift m$
17	16	eqeq2d	$⊢ n = m \to (x = y cyclShift n \leftrightarrow x = y cyclShift m)$
18	17	cbvrexvw	$⊢ \exists n \in (0 \dots N) x = y cyclShift n \leftrightarrow \exists m \in (0 \dots N) x = y cyclShift m$
19		oveq2	$⊢ n = k \to z cyclShift n = z cyclShift k$
20	19	eqeq2d	$⊢ n = k \to (y = z cyclShift n \leftrightarrow y = z cyclShift k)$
21	20	cbvrexvw	$⊢ \exists n \in (0 \dots N) y = z cyclShift n \leftrightarrow \exists k \in (0 \dots N) y = z cyclShift k$
22		eqid	$⊢ Vtx (G) = Vtx (G)$
23	22	clwwlknbp	$⊢ z \in (N ClWWalksN G) \to (z \in Word Vtx (G) \land \|z\| = N)$
24		eqcom	$⊢ \|z\| = N \leftrightarrow N = \|z\|$
25	24	biimpi	$⊢ \|z\| = N \to N = \|z\|$
26	23 25	simpl2im	$⊢ z \in (N ClWWalksN G) \to N = \|z\|$
27	26 1	eleq2s	$⊢ z \in W \to N = \|z\|$
28	27	ad2antlr	$⊢ (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \to N = \|z\|$
29	23	simpld	$⊢ z \in (N ClWWalksN G) \to z \in Word Vtx (G)$
30	29 1	eleq2s	$⊢ z \in W \to z \in Word Vtx (G)$
31	30	ad2antlr	$⊢ (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \to z \in Word Vtx (G)$
32	31	adantl	$⊢ (N = \|z\| \land (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|))) \to z \in Word Vtx (G)$
33		simprr	$⊢ (N = \|z\| \land (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|))) \to (\|y\| = \|z\| \land \|x\| = \|y\|)$
34	32 33	cshwcsh2id	$⊢ (N = \|z\| \land (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|))) \to (((m \in (0 \dots \|y\|) \land x = y cyclShift m) \land (k \in (0 \dots \|z\|) \land y = z cyclShift k)) \to \exists n \in (0 \dots \|z\|) x = z cyclShift n)$
35		oveq2	$⊢ N = \|z\| \to (0 \dots N) = (0 \dots \|z\|)$
36		oveq2	$⊢ \|z\| = \|y\| \to (0 \dots \|z\|) = (0 \dots \|y\|)$
37	36	eqcoms	$⊢ \|y\| = \|z\| \to (0 \dots \|z\|) = (0 \dots \|y\|)$
38	37	adantr	$⊢ (\|y\| = \|z\| \land \|x\| = \|y\|) \to (0 \dots \|z\|) = (0 \dots \|y\|)$
39	38	adantl	$⊢ (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \to (0 \dots \|z\|) = (0 \dots \|y\|)$
40	35 39	sylan9eq	$⊢ (N = \|z\| \land (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|))) \to (0 \dots N) = (0 \dots \|y\|)$
41	40	eleq2d	$⊢ (N = \|z\| \land (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|))) \to (m \in (0 \dots N) \leftrightarrow m \in (0 \dots \|y\|))$
42	41	anbi1d	$⊢ (N = \|z\| \land (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|))) \to ((m \in (0 \dots N) \land x = y cyclShift m) \leftrightarrow (m \in (0 \dots \|y\|) \land x = y cyclShift m))$
43	35	eleq2d	$⊢ N = \|z\| \to (k \in (0 \dots N) \leftrightarrow k \in (0 \dots \|z\|))$
44	43	anbi1d	$⊢ N = \|z\| \to ((k \in (0 \dots N) \land y = z cyclShift k) \leftrightarrow (k \in (0 \dots \|z\|) \land y = z cyclShift k))$
45	44	adantr	$⊢ (N = \|z\| \land (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|))) \to ((k \in (0 \dots N) \land y = z cyclShift k) \leftrightarrow (k \in (0 \dots \|z\|) \land y = z cyclShift k))$
46	42 45	anbi12d	$⊢ (N = \|z\| \land (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|))) \to (((m \in (0 \dots N) \land x = y cyclShift m) \land (k \in (0 \dots N) \land y = z cyclShift k)) \leftrightarrow ((m \in (0 \dots \|y\|) \land x = y cyclShift m) \land (k \in (0 \dots \|z\|) \land y = z cyclShift k)))$
47	35	rexeqdv	$⊢ N = \|z\| \to (\exists n \in (0 \dots N) x = z cyclShift n \leftrightarrow \exists n \in (0 \dots \|z\|) x = z cyclShift n)$
48	47	adantr	$⊢ (N = \|z\| \land (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|))) \to (\exists n \in (0 \dots N) x = z cyclShift n \leftrightarrow \exists n \in (0 \dots \|z\|) x = z cyclShift n)$
49	34 46 48	3imtr4d	$⊢ (N = \|z\| \land (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|))) \to (((m \in (0 \dots N) \land x = y cyclShift m) \land (k \in (0 \dots N) \land y = z cyclShift k)) \to \exists n \in (0 \dots N) x = z cyclShift n)$
50	28 49	mpancom	$⊢ (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \to (((m \in (0 \dots N) \land x = y cyclShift m) \land (k \in (0 \dots N) \land y = z cyclShift k)) \to \exists n \in (0 \dots N) x = z cyclShift n)$
51	50	exp5l	$⊢ (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \to (m \in (0 \dots N) \to (x = y cyclShift m \to (k \in (0 \dots N) \to (y = z cyclShift k \to \exists n \in (0 \dots N) x = z cyclShift n))))$
52	51	imp41	$⊢ ((((((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \land m \in (0 \dots N)) \land x = y cyclShift m) \land k \in (0 \dots N)) \to (y = z cyclShift k \to \exists n \in (0 \dots N) x = z cyclShift n)$
53	52	rexlimdva	$⊢ (((((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \land m \in (0 \dots N)) \land x = y cyclShift m) \to (\exists k \in (0 \dots N) y = z cyclShift k \to \exists n \in (0 \dots N) x = z cyclShift n)$
54	53	ex	$⊢ ((((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \land m \in (0 \dots N)) \to (x = y cyclShift m \to (\exists k \in (0 \dots N) y = z cyclShift k \to \exists n \in (0 \dots N) x = z cyclShift n))$
55	54	rexlimdva	$⊢ (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \to (\exists m \in (0 \dots N) x = y cyclShift m \to (\exists k \in (0 \dots N) y = z cyclShift k \to \exists n \in (0 \dots N) x = z cyclShift n))$
56	21 55	syl7bi	$⊢ (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \to (\exists m \in (0 \dots N) x = y cyclShift m \to (\exists n \in (0 \dots N) y = z cyclShift n \to \exists n \in (0 \dots N) x = z cyclShift n))$
57	18 56	syl5bi	$⊢ (((x \in W \land y \in W) \land z \in W) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \to (\exists n \in (0 \dots N) x = y cyclShift n \to (\exists n \in (0 \dots N) y = z cyclShift n \to \exists n \in (0 \dots N) x = z cyclShift n))$
58	57	exp31	$⊢ (x \in W \land y \in W) \to (z \in W \to ((\|y\| = \|z\| \land \|x\| = \|y\|) \to (\exists n \in (0 \dots N) x = y cyclShift n \to (\exists n \in (0 \dots N) y = z cyclShift n \to \exists n \in (0 \dots N) x = z cyclShift n))))$
59	58	com15	$⊢ \exists n \in (0 \dots N) y = z cyclShift n \to (z \in W \to ((\|y\| = \|z\| \land \|x\| = \|y\|) \to (\exists n \in (0 \dots N) x = y cyclShift n \to ((x \in W \land y \in W) \to \exists n \in (0 \dots N) x = z cyclShift n))))$
60	59	impcom	$⊢ (z \in W \land \exists n \in (0 \dots N) y = z cyclShift n) \to ((\|y\| = \|z\| \land \|x\| = \|y\|) \to (\exists n \in (0 \dots N) x = y cyclShift n \to ((x \in W \land y \in W) \to \exists n \in (0 \dots N) x = z cyclShift n)))$
61	60	3adant1	$⊢ (y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n) \to ((\|y\| = \|z\| \land \|x\| = \|y\|) \to (\exists n \in (0 \dots N) x = y cyclShift n \to ((x \in W \land y \in W) \to \exists n \in (0 \dots N) x = z cyclShift n)))$
62	61	impcom	$⊢ ((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n)) \to (\exists n \in (0 \dots N) x = y cyclShift n \to ((x \in W \land y \in W) \to \exists n \in (0 \dots N) x = z cyclShift n))$
63	62	com13	$⊢ (x \in W \land y \in W) \to (\exists n \in (0 \dots N) x = y cyclShift n \to (((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n)) \to \exists n \in (0 \dots N) x = z cyclShift n))$
64	63	3impia	$⊢ (x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n) \to (((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n)) \to \exists n \in (0 \dots N) x = z cyclShift n)$
65	64	impcom	$⊢ (((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n)) \land (x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n)) \to \exists n \in (0 \dots N) x = z cyclShift n$
66	14 15 65	3jca	$⊢ (((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n)) \land (x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n)) \to (x \in W \land z \in W \land \exists n \in (0 \dots N) x = z cyclShift n)$
67	1 2	erclwwlkneq	$⊢ (x \in V \land z \in V) \to (x \underset{˙}{\sim} z \leftrightarrow (x \in W \land z \in W \land \exists n \in (0 \dots N) x = z cyclShift n))$
68	67	3adant2	$⊢ (x \in V \land y \in V \land z \in V) \to (x \underset{˙}{\sim} z \leftrightarrow (x \in W \land z \in W \land \exists n \in (0 \dots N) x = z cyclShift n))$
69	66 68	syl5ibrcom	$⊢ (((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n)) \land (x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n)) \to ((x \in V \land y \in V \land z \in V) \to x \underset{˙}{\sim} z)$
70	69	exp31	$⊢ (\|y\| = \|z\| \land \|x\| = \|y\|) \to ((y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n) \to ((x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n) \to ((x \in V \land y \in V \land z \in V) \to x \underset{˙}{\sim} z)))$
71	70	com24	$⊢ (\|y\| = \|z\| \land \|x\| = \|y\|) \to ((x \in V \land y \in V \land z \in V) \to ((x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n) \to ((y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n) \to x \underset{˙}{\sim} z)))$
72	71	ex	$⊢ \|y\| = \|z\| \to (\|x\| = \|y\| \to ((x \in V \land y \in V \land z \in V) \to ((x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n) \to ((y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n) \to x \underset{˙}{\sim} z))))$
73	72	com4t	$⊢ (x \in V \land y \in V \land z \in V) \to ((x \in W \land y \in W \land \exists n \in (0 \dots N) x = y cyclShift n) \to (\|y\| = \|z\| \to (\|x\| = \|y\| \to ((y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n) \to x \underset{˙}{\sim} z))))$
74	13 73	sylbid	$⊢ (x \in V \land y \in V \land z \in V) \to (x \underset{˙}{\sim} y \to (\|y\| = \|z\| \to (\|x\| = \|y\| \to ((y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n) \to x \underset{˙}{\sim} z))))$
75	74	com25	$⊢ (x \in V \land y \in V \land z \in V) \to ((y \in W \land z \in W \land \exists n \in (0 \dots N) y = z cyclShift n) \to (\|y\| = \|z\| \to (\|x\| = \|y\| \to (x \underset{˙}{\sim} y \to x \underset{˙}{\sim} z))))$
76	11 75	sylbid	$⊢ (x \in V \land y \in V \land z \in V) \to (y \underset{˙}{\sim} z \to (\|y\| = \|z\| \to (\|x\| = \|y\| \to (x \underset{˙}{\sim} y \to x \underset{˙}{\sim} z))))$
77	9 76	mpdd	$⊢ (x \in V \land y \in V \land z \in V) \to (y \underset{˙}{\sim} z \to (\|x\| = \|y\| \to (x \underset{˙}{\sim} y \to x \underset{˙}{\sim} z)))$
78	77	com24	$⊢ (x \in V \land y \in V \land z \in V) \to (x \underset{˙}{\sim} y \to (\|x\| = \|y\| \to (y \underset{˙}{\sim} z \to x \underset{˙}{\sim} z)))$
79	7 78	mpdd	$⊢ (x \in V \land y \in V \land z \in V) \to (x \underset{˙}{\sim} y \to (y \underset{˙}{\sim} z \to x \underset{˙}{\sim} z))$
80	79	impd	$⊢ (x \in V \land y \in V \land z \in V) \to ((x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z) \to x \underset{˙}{\sim} z)$
81	3 4 5 80	mp3an	$⊢ (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z) \to x \underset{˙}{\sim} z$

Metamath Proof Explorer

Theorem erclwwlkntr

Proof