erclwwlktr

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
	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	erclwwlktr	$⊢ (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z) \to x \underset{˙}{\sim} z$

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		vex	$⊢ x \in V$
3		vex	$⊢ y \in V$
4		vex	$⊢ z \in V$
5	1	erclwwlkeqlen	$⊢ (x \in V \land y \in V) \to (x \underset{˙}{\sim} y \to \|x\| = \|y\|)$
6	5	3adant3	$⊢ (x \in V \land y \in V \land z \in V) \to (x \underset{˙}{\sim} y \to \|x\| = \|y\|)$
7	1	erclwwlkeqlen	$⊢ (y \in V \land z \in V) \to (y \underset{˙}{\sim} z \to \|y\| = \|z\|)$
8	7	3adant1	$⊢ (x \in V \land y \in V \land z \in V) \to (y \underset{˙}{\sim} z \to \|y\| = \|z\|)$
9	1	erclwwlkeq	$⊢ (y \in V \land z \in V) \to (y \underset{˙}{\sim} z \leftrightarrow (y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n))$
10	9	3adant1	$⊢ (x \in V \land y \in V \land z \in V) \to (y \underset{˙}{\sim} z \leftrightarrow (y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n))$
11	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))$
12	11	3adant3	$⊢ (x \in V \land y \in V \land z \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))$
13		simpr1	$⊢ (((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n)) \land (x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n)) \to x \in ClWWalks (G)$
14		simplr2	$⊢ (((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n)) \land (x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n)) \to z \in ClWWalks (G)$
15		oveq2	$⊢ n = m \to y cyclShift n = y cyclShift m$
16	15	eqeq2d	$⊢ n = m \to (x = y cyclShift n \leftrightarrow x = y cyclShift m)$
17	16	cbvrexvw	$⊢ \exists n \in (0 \dots \|y\|) x = y cyclShift n \leftrightarrow \exists m \in (0 \dots \|y\|) x = y cyclShift m$
18		oveq2	$⊢ n = k \to z cyclShift n = z cyclShift k$
19	18	eqeq2d	$⊢ n = k \to (y = z cyclShift n \leftrightarrow y = z cyclShift k)$
20	19	cbvrexvw	$⊢ \exists n \in (0 \dots \|z\|) y = z cyclShift n \leftrightarrow \exists k \in (0 \dots \|z\|) y = z cyclShift k$
21		eqid	$⊢ Vtx (G) = Vtx (G)$
22	21	clwwlkbp	$⊢ z \in ClWWalks (G) \to (G \in V \land z \in Word Vtx (G) \land z \neq \emptyset)$
23	22	simp2d	$⊢ z \in ClWWalks (G) \to z \in Word Vtx (G)$
24	23	ad2antlr	$⊢ (((x \in ClWWalks (G) \land y \in ClWWalks (G)) \land z \in ClWWalks (G)) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \to z \in Word Vtx (G)$
25		simpr	$⊢ (((x \in ClWWalks (G) \land y \in ClWWalks (G)) \land z \in ClWWalks (G)) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \to (\|y\| = \|z\| \land \|x\| = \|y\|)$
26	24 25	cshwcsh2id	$⊢ (((x \in ClWWalks (G) \land y \in ClWWalks (G)) \land z \in ClWWalks (G)) \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)$
27	26	exp5l	$⊢ (((x \in ClWWalks (G) \land y \in ClWWalks (G)) \land z \in ClWWalks (G)) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \to (m \in (0 \dots \|y\|) \to (x = y cyclShift m \to (k \in (0 \dots \|z\|) \to (y = z cyclShift k \to \exists n \in (0 \dots \|z\|) x = z cyclShift n))))$
28	27	imp41	$⊢ ((((((x \in ClWWalks (G) \land y \in ClWWalks (G)) \land z \in ClWWalks (G)) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \land m \in (0 \dots \|y\|)) \land x = y cyclShift m) \land k \in (0 \dots \|z\|)) \to (y = z cyclShift k \to \exists n \in (0 \dots \|z\|) x = z cyclShift n)$
29	28	rexlimdva	$⊢ (((((x \in ClWWalks (G) \land y \in ClWWalks (G)) \land z \in ClWWalks (G)) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \land m \in (0 \dots \|y\|)) \land x = y cyclShift m) \to (\exists k \in (0 \dots \|z\|) y = z cyclShift k \to \exists n \in (0 \dots \|z\|) x = z cyclShift n)$
30	29	rexlimdva2	$⊢ (((x \in ClWWalks (G) \land y \in ClWWalks (G)) \land z \in ClWWalks (G)) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \to (\exists m \in (0 \dots \|y\|) x = y cyclShift m \to (\exists k \in (0 \dots \|z\|) y = z cyclShift k \to \exists n \in (0 \dots \|z\|) x = z cyclShift n))$
31	20 30	syl7bi	$⊢ (((x \in ClWWalks (G) \land y \in ClWWalks (G)) \land z \in ClWWalks (G)) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \to (\exists m \in (0 \dots \|y\|) x = y cyclShift m \to (\exists n \in (0 \dots \|z\|) y = z cyclShift n \to \exists n \in (0 \dots \|z\|) x = z cyclShift n))$
32	17 31	biimtrid	$⊢ (((x \in ClWWalks (G) \land y \in ClWWalks (G)) \land z \in ClWWalks (G)) \land (\|y\| = \|z\| \land \|x\| = \|y\|)) \to (\exists n \in (0 \dots \|y\|) x = y cyclShift n \to (\exists n \in (0 \dots \|z\|) y = z cyclShift n \to \exists n \in (0 \dots \|z\|) x = z cyclShift n))$
33	32	exp31	$⊢ (x \in ClWWalks (G) \land y \in ClWWalks (G)) \to (z \in ClWWalks (G) \to ((\|y\| = \|z\| \land \|x\| = \|y\|) \to (\exists n \in (0 \dots \|y\|) x = y cyclShift n \to (\exists n \in (0 \dots \|z\|) y = z cyclShift n \to \exists n \in (0 \dots \|z\|) x = z cyclShift n))))$
34	33	com15	$⊢ \exists n \in (0 \dots \|z\|) y = z cyclShift n \to (z \in ClWWalks (G) \to ((\|y\| = \|z\| \land \|x\| = \|y\|) \to (\exists n \in (0 \dots \|y\|) x = y cyclShift n \to ((x \in ClWWalks (G) \land y \in ClWWalks (G)) \to \exists n \in (0 \dots \|z\|) x = z cyclShift n))))$
35	34	impcom	$⊢ (z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n) \to ((\|y\| = \|z\| \land \|x\| = \|y\|) \to (\exists n \in (0 \dots \|y\|) x = y cyclShift n \to ((x \in ClWWalks (G) \land y \in ClWWalks (G)) \to \exists n \in (0 \dots \|z\|) x = z cyclShift n)))$
36	35	3adant1	$⊢ (y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n) \to ((\|y\| = \|z\| \land \|x\| = \|y\|) \to (\exists n \in (0 \dots \|y\|) x = y cyclShift n \to ((x \in ClWWalks (G) \land y \in ClWWalks (G)) \to \exists n \in (0 \dots \|z\|) x = z cyclShift n)))$
37	36	impcom	$⊢ ((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n)) \to (\exists n \in (0 \dots \|y\|) x = y cyclShift n \to ((x \in ClWWalks (G) \land y \in ClWWalks (G)) \to \exists n \in (0 \dots \|z\|) x = z cyclShift n))$
38	37	com13	$⊢ (x \in ClWWalks (G) \land y \in ClWWalks (G)) \to (\exists n \in (0 \dots \|y\|) x = y cyclShift n \to (((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n)) \to \exists n \in (0 \dots \|z\|) x = z cyclShift n))$
39	38	3impia	$⊢ (x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n) \to (((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n)) \to \exists n \in (0 \dots \|z\|) x = z cyclShift n)$
40	39	impcom	$⊢ (((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n)) \land (x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n)) \to \exists n \in (0 \dots \|z\|) x = z cyclShift n$
41	13 14 40	3jca	$⊢ (((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n)) \land (x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n)) \to (x \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) x = z cyclShift n)$
42	1	erclwwlkeq	$⊢ (x \in V \land z \in V) \to (x \underset{˙}{\sim} z \leftrightarrow (x \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) x = z cyclShift n))$
43	42	3adant2	$⊢ (x \in V \land y \in V \land z \in V) \to (x \underset{˙}{\sim} z \leftrightarrow (x \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) x = z cyclShift n))$
44	41 43	syl5ibrcom	$⊢ (((\|y\| = \|z\| \land \|x\| = \|y\|) \land (y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n)) \land (x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n)) \to ((x \in V \land y \in V \land z \in V) \to x \underset{˙}{\sim} z)$
45	44	exp31	$⊢ (\|y\| = \|z\| \land \|x\| = \|y\|) \to ((y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n) \to ((x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n) \to ((x \in V \land y \in V \land z \in V) \to x \underset{˙}{\sim} z)))$
46	45	com24	$⊢ (\|y\| = \|z\| \land \|x\| = \|y\|) \to ((x \in V \land y \in V \land z \in V) \to ((x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n) \to ((y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n) \to x \underset{˙}{\sim} z)))$
47	46	ex	$⊢ \|y\| = \|z\| \to (\|x\| = \|y\| \to ((x \in V \land y \in V \land z \in V) \to ((x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n) \to ((y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n) \to x \underset{˙}{\sim} z))))$
48	47	com4t	$⊢ (x \in V \land y \in V \land z \in V) \to ((x \in ClWWalks (G) \land y \in ClWWalks (G) \land \exists n \in (0 \dots \|y\|) x = y cyclShift n) \to (\|y\| = \|z\| \to (\|x\| = \|y\| \to ((y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n) \to x \underset{˙}{\sim} z))))$
49	12 48	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 ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n) \to x \underset{˙}{\sim} z))))$
50	49	com25	$⊢ (x \in V \land y \in V \land z \in V) \to ((y \in ClWWalks (G) \land z \in ClWWalks (G) \land \exists n \in (0 \dots \|z\|) y = z cyclShift n) \to (\|y\| = \|z\| \to (\|x\| = \|y\| \to (x \underset{˙}{\sim} y \to x \underset{˙}{\sim} z))))$
51	10 50	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))))$
52	8 51	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)))$
53	52	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)))$
54	6 53	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))$
55	54	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)$
56	2 3 4 55	mp3an	$⊢ (x \underset{˙}{\sim} y \land y \underset{˙}{\sim} z) \to x \underset{˙}{\sim} z$

Metamath Proof Explorer

Theorem erclwwlktr

Proof