eleclclwwlknlem2

		Ref	Expression
	Hypothesis	erclwwlkn1.w	$⊢ W = N ClWWalksN G$
	Assertion	eleclclwwlknlem2	$⊢ ((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \to (\exists m \in (0 \dots N) Y = x cyclShift m \leftrightarrow \exists n \in (0 \dots N) Y = X cyclShift n)$

Proof

Step	Hyp	Ref	Expression
1		erclwwlkn1.w	$⊢ W = N ClWWalksN G$
2		simpl	$⊢ (k \in (0 \dots N) \land X = x cyclShift k) \to k \in (0 \dots N)$
3	2	anim1i	$⊢ ((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \to (k \in (0 \dots N) \land (X \in W \land x \in W))$
4	3	adantr	$⊢ (((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \land \exists m \in (0 \dots N) Y = x cyclShift m) \to (k \in (0 \dots N) \land (X \in W \land x \in W))$
5		simpr	$⊢ (k \in (0 \dots N) \land X = x cyclShift k) \to X = x cyclShift k$
6	5	adantr	$⊢ ((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \to X = x cyclShift k$
7	6	anim1i	$⊢ (((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \land \exists m \in (0 \dots N) Y = x cyclShift m) \to (X = x cyclShift k \land \exists m \in (0 \dots N) Y = x cyclShift m)$
8	1	eleclclwwlknlem1	$⊢ (k \in (0 \dots N) \land (X \in W \land x \in W)) \to ((X = x cyclShift k \land \exists m \in (0 \dots N) Y = x cyclShift m) \to \exists n \in (0 \dots N) Y = X cyclShift n)$
9	4 7 8	sylc	$⊢ (((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \land \exists m \in (0 \dots N) Y = x cyclShift m) \to \exists n \in (0 \dots N) Y = X cyclShift n$
10		eqid	$⊢ Vtx (G) = Vtx (G)$
11	10	clwwlknbp	$⊢ x \in (N ClWWalksN G) \to (x \in Word Vtx (G) \land \|x\| = N)$
12	11 1	eleq2s	$⊢ x \in W \to (x \in Word Vtx (G) \land \|x\| = N)$
13		fznn0sub2	$⊢ k \in (0 \dots N) \to N - k \in (0 \dots N)$
14		oveq1	$⊢ \|x\| = N \to \|x\| - k = N - k$
15	14	eleq1d	$⊢ \|x\| = N \to (\|x\| - k \in (0 \dots N) \leftrightarrow N - k \in (0 \dots N))$
16	13 15	imbitrrid	$⊢ \|x\| = N \to (k \in (0 \dots N) \to \|x\| - k \in (0 \dots N))$
17	16	adantl	$⊢ (x \in Word Vtx (G) \land \|x\| = N) \to (k \in (0 \dots N) \to \|x\| - k \in (0 \dots N))$
18	12 17	syl	$⊢ x \in W \to (k \in (0 \dots N) \to \|x\| - k \in (0 \dots N))$
19	18	adantl	$⊢ (X \in W \land x \in W) \to (k \in (0 \dots N) \to \|x\| - k \in (0 \dots N))$
20	19	com12	$⊢ k \in (0 \dots N) \to ((X \in W \land x \in W) \to \|x\| - k \in (0 \dots N))$
21	20	adantr	$⊢ (k \in (0 \dots N) \land X = x cyclShift k) \to ((X \in W \land x \in W) \to \|x\| - k \in (0 \dots N))$
22	21	imp	$⊢ ((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \to \|x\| - k \in (0 \dots N)$
23	22	adantr	$⊢ (((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \land \exists n \in (0 \dots N) Y = X cyclShift n) \to \|x\| - k \in (0 \dots N)$
24		simpr	$⊢ ((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \to (X \in W \land x \in W)$
25	24	ancomd	$⊢ ((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \to (x \in W \land X \in W)$
26	25	adantr	$⊢ (((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \land \exists n \in (0 \dots N) Y = X cyclShift n) \to (x \in W \land X \in W)$
27	23 26	jca	$⊢ (((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \land \exists n \in (0 \dots N) Y = X cyclShift n) \to (\|x\| - k \in (0 \dots N) \land (x \in W \land X \in W))$
28		simpll	$⊢ ((x \in Word Vtx (G) \land \|x\| = N) \land k \in (0 \dots N)) \to x \in Word Vtx (G)$
29		oveq2	$⊢ N = \|x\| \to (0 \dots N) = (0 \dots \|x\|)$
30	29	eleq2d	$⊢ N = \|x\| \to (k \in (0 \dots N) \leftrightarrow k \in (0 \dots \|x\|))$
31	30	eqcoms	$⊢ \|x\| = N \to (k \in (0 \dots N) \leftrightarrow k \in (0 \dots \|x\|))$
32	31	adantl	$⊢ (x \in Word Vtx (G) \land \|x\| = N) \to (k \in (0 \dots N) \leftrightarrow k \in (0 \dots \|x\|))$
33	32	biimpa	$⊢ ((x \in Word Vtx (G) \land \|x\| = N) \land k \in (0 \dots N)) \to k \in (0 \dots \|x\|)$
34	28 33	jca	$⊢ ((x \in Word Vtx (G) \land \|x\| = N) \land k \in (0 \dots N)) \to (x \in Word Vtx (G) \land k \in (0 \dots \|x\|))$
35	34	ex	$⊢ (x \in Word Vtx (G) \land \|x\| = N) \to (k \in (0 \dots N) \to (x \in Word Vtx (G) \land k \in (0 \dots \|x\|)))$
36	12 35	syl	$⊢ x \in W \to (k \in (0 \dots N) \to (x \in Word Vtx (G) \land k \in (0 \dots \|x\|)))$
37	36	adantl	$⊢ (X \in W \land x \in W) \to (k \in (0 \dots N) \to (x \in Word Vtx (G) \land k \in (0 \dots \|x\|)))$
38	37	com12	$⊢ k \in (0 \dots N) \to ((X \in W \land x \in W) \to (x \in Word Vtx (G) \land k \in (0 \dots \|x\|)))$
39	38	adantr	$⊢ (k \in (0 \dots N) \land X = x cyclShift k) \to ((X \in W \land x \in W) \to (x \in Word Vtx (G) \land k \in (0 \dots \|x\|)))$
40	39	imp	$⊢ ((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \to (x \in Word Vtx (G) \land k \in (0 \dots \|x\|))$
41	5	eqcomd	$⊢ (k \in (0 \dots N) \land X = x cyclShift k) \to x cyclShift k = X$
42	41	adantr	$⊢ ((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \to x cyclShift k = X$
43		oveq1	$⊢ X = x cyclShift k \to X cyclShift (\|x\| - k) = (x cyclShift k) cyclShift (\|x\| - k)$
44	43	eqcoms	$⊢ x cyclShift k = X \to X cyclShift (\|x\| - k) = (x cyclShift k) cyclShift (\|x\| - k)$
45		elfzelz	$⊢ k \in (0 \dots \|x\|) \to k \in ℤ$
46		2cshwid	$⊢ (x \in Word Vtx (G) \land k \in ℤ) \to (x cyclShift k) cyclShift (\|x\| - k) = x$
47	45 46	sylan2	$⊢ (x \in Word Vtx (G) \land k \in (0 \dots \|x\|)) \to (x cyclShift k) cyclShift (\|x\| - k) = x$
48	44 47	sylan9eqr	$⊢ ((x \in Word Vtx (G) \land k \in (0 \dots \|x\|)) \land x cyclShift k = X) \to X cyclShift (\|x\| - k) = x$
49	40 42 48	syl2anc	$⊢ ((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \to X cyclShift (\|x\| - k) = x$
50	49	eqcomd	$⊢ ((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \to x = X cyclShift (\|x\| - k)$
51	50	anim1i	$⊢ (((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \land \exists n \in (0 \dots N) Y = X cyclShift n) \to (x = X cyclShift (\|x\| - k) \land \exists n \in (0 \dots N) Y = X cyclShift n)$
52	1	eleclclwwlknlem1	$⊢ (\|x\| - k \in (0 \dots N) \land (x \in W \land X \in W)) \to ((x = X cyclShift (\|x\| - k) \land \exists n \in (0 \dots N) Y = X cyclShift n) \to \exists m \in (0 \dots N) Y = x cyclShift m)$
53	27 51 52	sylc	$⊢ (((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \land \exists n \in (0 \dots N) Y = X cyclShift n) \to \exists m \in (0 \dots N) Y = x cyclShift m$
54	9 53	impbida	$⊢ ((k \in (0 \dots N) \land X = x cyclShift k) \land (X \in W \land x \in W)) \to (\exists m \in (0 \dots N) Y = x cyclShift m \leftrightarrow \exists n \in (0 \dots N) Y = X cyclShift n)$

Metamath Proof Explorer

Theorem eleclclwwlknlem2

Proof