clwwlknscsh

Description: The set of cyclical shifts of a word representing a closed walk is the set of closed walks represented by cyclical shifts of a word. (Contributed by Alexander van der Vekens, 15-Jun-2018) (Revised by AV, 30-Apr-2021)

		Ref	Expression
	Assertion	clwwlknscsh	$⊢ (N \in ℕ_{0} \land W \in (N ClWWalksN G)) \to \{y \in (N ClWWalksN G) \| \exists n \in (0 \dots N) y = W cyclShift n\} = \{y \in Word Vtx (G) \| \exists n \in (0 \dots N) y = W cyclShift n\}$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ y = x \to (y = W cyclShift n \leftrightarrow x = W cyclShift n)$
2	1	rexbidv	$⊢ y = x \to (\exists n \in (0 \dots N) y = W cyclShift n \leftrightarrow \exists n \in (0 \dots N) x = W cyclShift n)$
3	2	cbvrabv	$⊢ \{y \in (N ClWWalksN G) \| \exists n \in (0 \dots N) y = W cyclShift n\} = \{x \in (N ClWWalksN G) \| \exists n \in (0 \dots N) x = W cyclShift n\}$
4		eqid	$⊢ Vtx (G) = Vtx (G)$
5	4	clwwlknwrd	$⊢ w \in (N ClWWalksN G) \to w \in Word Vtx (G)$
6	5	ad2antrl	$⊢ ((N \in ℕ_{0} \land W \in (N ClWWalksN G)) \land (w \in (N ClWWalksN G) \land \exists n \in (0 \dots N) w = W cyclShift n)) \to w \in Word Vtx (G)$
7		simprr	$⊢ ((N \in ℕ_{0} \land W \in (N ClWWalksN G)) \land (w \in (N ClWWalksN G) \land \exists n \in (0 \dots N) w = W cyclShift n)) \to \exists n \in (0 \dots N) w = W cyclShift n$
8	6 7	jca	$⊢ ((N \in ℕ_{0} \land W \in (N ClWWalksN G)) \land (w \in (N ClWWalksN G) \land \exists n \in (0 \dots N) w = W cyclShift n)) \to (w \in Word Vtx (G) \land \exists n \in (0 \dots N) w = W cyclShift n)$
9		simprr	$⊢ ((w \in Word Vtx (G) \land n \in (0 \dots N)) \land (N \in ℕ_{0} \land W \in (N ClWWalksN G))) \to W \in (N ClWWalksN G)$
10		simpllr	$⊢ (((w \in Word Vtx (G) \land n \in (0 \dots N)) \land (N \in ℕ_{0} \land W \in (N ClWWalksN G))) \land w = W cyclShift n) \to n \in (0 \dots N)$
11		clwwnisshclwwsn	$⊢ (W \in (N ClWWalksN G) \land n \in (0 \dots N)) \to W cyclShift n \in (N ClWWalksN G)$
12	9 10 11	syl2an2r	$⊢ (((w \in Word Vtx (G) \land n \in (0 \dots N)) \land (N \in ℕ_{0} \land W \in (N ClWWalksN G))) \land w = W cyclShift n) \to W cyclShift n \in (N ClWWalksN G)$
13		eleq1	$⊢ w = W cyclShift n \to (w \in (N ClWWalksN G) \leftrightarrow W cyclShift n \in (N ClWWalksN G))$
14	13	adantl	$⊢ (((w \in Word Vtx (G) \land n \in (0 \dots N)) \land (N \in ℕ_{0} \land W \in (N ClWWalksN G))) \land w = W cyclShift n) \to (w \in (N ClWWalksN G) \leftrightarrow W cyclShift n \in (N ClWWalksN G))$
15	12 14	mpbird	$⊢ (((w \in Word Vtx (G) \land n \in (0 \dots N)) \land (N \in ℕ_{0} \land W \in (N ClWWalksN G))) \land w = W cyclShift n) \to w \in (N ClWWalksN G)$
16	15	exp31	$⊢ (w \in Word Vtx (G) \land n \in (0 \dots N)) \to ((N \in ℕ_{0} \land W \in (N ClWWalksN G)) \to (w = W cyclShift n \to w \in (N ClWWalksN G)))$
17	16	com23	$⊢ (w \in Word Vtx (G) \land n \in (0 \dots N)) \to (w = W cyclShift n \to ((N \in ℕ_{0} \land W \in (N ClWWalksN G)) \to w \in (N ClWWalksN G)))$
18	17	rexlimdva	$⊢ w \in Word Vtx (G) \to (\exists n \in (0 \dots N) w = W cyclShift n \to ((N \in ℕ_{0} \land W \in (N ClWWalksN G)) \to w \in (N ClWWalksN G)))$
19	18	imp	$⊢ (w \in Word Vtx (G) \land \exists n \in (0 \dots N) w = W cyclShift n) \to ((N \in ℕ_{0} \land W \in (N ClWWalksN G)) \to w \in (N ClWWalksN G))$
20	19	impcom	$⊢ ((N \in ℕ_{0} \land W \in (N ClWWalksN G)) \land (w \in Word Vtx (G) \land \exists n \in (0 \dots N) w = W cyclShift n)) \to w \in (N ClWWalksN G)$
21		simprr	$⊢ ((N \in ℕ_{0} \land W \in (N ClWWalksN G)) \land (w \in Word Vtx (G) \land \exists n \in (0 \dots N) w = W cyclShift n)) \to \exists n \in (0 \dots N) w = W cyclShift n$
22	20 21	jca	$⊢ ((N \in ℕ_{0} \land W \in (N ClWWalksN G)) \land (w \in Word Vtx (G) \land \exists n \in (0 \dots N) w = W cyclShift n)) \to (w \in (N ClWWalksN G) \land \exists n \in (0 \dots N) w = W cyclShift n)$
23	8 22	impbida	$⊢ (N \in ℕ_{0} \land W \in (N ClWWalksN G)) \to ((w \in (N ClWWalksN G) \land \exists n \in (0 \dots N) w = W cyclShift n) \leftrightarrow (w \in Word Vtx (G) \land \exists n \in (0 \dots N) w = W cyclShift n))$
24		eqeq1	$⊢ x = w \to (x = W cyclShift n \leftrightarrow w = W cyclShift n)$
25	24	rexbidv	$⊢ x = w \to (\exists n \in (0 \dots N) x = W cyclShift n \leftrightarrow \exists n \in (0 \dots N) w = W cyclShift n)$
26	25	elrab	$⊢ w \in \{x \in (N ClWWalksN G) \| \exists n \in (0 \dots N) x = W cyclShift n\} \leftrightarrow (w \in (N ClWWalksN G) \land \exists n \in (0 \dots N) w = W cyclShift n)$
27		eqeq1	$⊢ y = w \to (y = W cyclShift n \leftrightarrow w = W cyclShift n)$
28	27	rexbidv	$⊢ y = w \to (\exists n \in (0 \dots N) y = W cyclShift n \leftrightarrow \exists n \in (0 \dots N) w = W cyclShift n)$
29	28	elrab	$⊢ w \in \{y \in Word Vtx (G) \| \exists n \in (0 \dots N) y = W cyclShift n\} \leftrightarrow (w \in Word Vtx (G) \land \exists n \in (0 \dots N) w = W cyclShift n)$
30	23 26 29	3bitr4g	$⊢ (N \in ℕ_{0} \land W \in (N ClWWalksN G)) \to (w \in \{x \in (N ClWWalksN G) \| \exists n \in (0 \dots N) x = W cyclShift n\} \leftrightarrow w \in \{y \in Word Vtx (G) \| \exists n \in (0 \dots N) y = W cyclShift n\})$
31	30	eqrdv	$⊢ (N \in ℕ_{0} \land W \in (N ClWWalksN G)) \to \{x \in (N ClWWalksN G) \| \exists n \in (0 \dots N) x = W cyclShift n\} = \{y \in Word Vtx (G) \| \exists n \in (0 \dots N) y = W cyclShift n\}$
32	3 31	syl5eq	$⊢ (N \in ℕ_{0} \land W \in (N ClWWalksN G)) \to \{y \in (N ClWWalksN G) \| \exists n \in (0 \dots N) y = W cyclShift n\} = \{y \in Word Vtx (G) \| \exists n \in (0 \dots N) y = W cyclShift n\}$

Metamath Proof Explorer

Theorem clwwlknscsh

Proof