hashecclwwlkn1

Description: The size of every equivalence class of the equivalence relation over the set of closed walks (defined as words) with a fixed length which is a prime number is 1 or equals this length. (Contributed by Alexander van der Vekens, 17-Jun-2018) (Revised by AV, 1-May-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	hashecclwwlkn1	$⊢ (N \in ℙ \land U \in (W / \underset{˙}{\sim})) \to (\|U\| = 1 \lor \|U\| = N)$

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	eclclwwlkn1	$⊢ U \in (W / \underset{˙}{\sim}) \to (U \in (W / \underset{˙}{\sim}) \leftrightarrow \exists x \in W U = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\})$
4		rabeq	$⊢ W = N ClWWalksN G \to \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} = \{y \in (N ClWWalksN G) \| \exists n \in (0 \dots N) y = x cyclShift n\}$
5	1 4	mp1i	$⊢ (N \in ℙ \land x \in W) \to \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} = \{y \in (N ClWWalksN G) \| \exists n \in (0 \dots N) y = x cyclShift n\}$
6		prmnn	$⊢ N \in ℙ \to N \in ℕ$
7	6	nnnn0d	$⊢ N \in ℙ \to N \in ℕ_{0}$
8	1	eleq2i	$⊢ x \in W \leftrightarrow x \in (N ClWWalksN G)$
9	8	biimpi	$⊢ x \in W \to x \in (N ClWWalksN G)$
10		clwwlknscsh	$⊢ (N \in ℕ_{0} \land x \in (N ClWWalksN G)) \to \{y \in (N ClWWalksN G) \| \exists n \in (0 \dots N) y = x cyclShift n\} = \{y \in Word Vtx (G) \| \exists n \in (0 \dots N) y = x cyclShift n\}$
11	7 9 10	syl2an	$⊢ (N \in ℙ \land x \in W) \to \{y \in (N ClWWalksN G) \| \exists n \in (0 \dots N) y = x cyclShift n\} = \{y \in Word Vtx (G) \| \exists n \in (0 \dots N) y = x cyclShift n\}$
12	5 11	eqtrd	$⊢ (N \in ℙ \land x \in W) \to \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} = \{y \in Word Vtx (G) \| \exists n \in (0 \dots N) y = x cyclShift n\}$
13	12	eqeq2d	$⊢ (N \in ℙ \land x \in W) \to (U = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \leftrightarrow U = \{y \in Word Vtx (G) \| \exists n \in (0 \dots N) y = x cyclShift n\})$
14		simpll	$⊢ ((x \in Word Vtx (G) \land \|x\| = N) \land N \in ℕ) \to x \in Word Vtx (G)$
15		elnnne0	$⊢ N \in ℕ \leftrightarrow (N \in ℕ_{0} \land N \neq 0)$
16		eqeq1	$⊢ N = \|x\| \to (N = 0 \leftrightarrow \|x\| = 0)$
17	16	eqcoms	$⊢ \|x\| = N \to (N = 0 \leftrightarrow \|x\| = 0)$
18		hasheq0	$⊢ x \in Word Vtx (G) \to (\|x\| = 0 \leftrightarrow x = \emptyset)$
19	17 18	sylan9bbr	$⊢ (x \in Word Vtx (G) \land \|x\| = N) \to (N = 0 \leftrightarrow x = \emptyset)$
20	19	necon3bid	$⊢ (x \in Word Vtx (G) \land \|x\| = N) \to (N \neq 0 \leftrightarrow x \neq \emptyset)$
21	20	biimpcd	$⊢ N \neq 0 \to ((x \in Word Vtx (G) \land \|x\| = N) \to x \neq \emptyset)$
22	15 21	simplbiim	$⊢ N \in ℕ \to ((x \in Word Vtx (G) \land \|x\| = N) \to x \neq \emptyset)$
23	22	impcom	$⊢ ((x \in Word Vtx (G) \land \|x\| = N) \land N \in ℕ) \to x \neq \emptyset$
24		simplr	$⊢ ((x \in Word Vtx (G) \land \|x\| = N) \land N \in ℕ) \to \|x\| = N$
25	24	eqcomd	$⊢ ((x \in Word Vtx (G) \land \|x\| = N) \land N \in ℕ) \to N = \|x\|$
26	14 23 25	3jca	$⊢ ((x \in Word Vtx (G) \land \|x\| = N) \land N \in ℕ) \to (x \in Word Vtx (G) \land x \neq \emptyset \land N = \|x\|)$
27	26	ex	$⊢ (x \in Word Vtx (G) \land \|x\| = N) \to (N \in ℕ \to (x \in Word Vtx (G) \land x \neq \emptyset \land N = \|x\|))$
28		eqid	$⊢ Vtx (G) = Vtx (G)$
29	28	clwwlknbp	$⊢ x \in (N ClWWalksN G) \to (x \in Word Vtx (G) \land \|x\| = N)$
30	27 29	syl11	$⊢ N \in ℕ \to (x \in (N ClWWalksN G) \to (x \in Word Vtx (G) \land x \neq \emptyset \land N = \|x\|))$
31	8 30	biimtrid	$⊢ N \in ℕ \to (x \in W \to (x \in Word Vtx (G) \land x \neq \emptyset \land N = \|x\|))$
32	6 31	syl	$⊢ N \in ℙ \to (x \in W \to (x \in Word Vtx (G) \land x \neq \emptyset \land N = \|x\|))$
33	32	imp	$⊢ (N \in ℙ \land x \in W) \to (x \in Word Vtx (G) \land x \neq \emptyset \land N = \|x\|)$
34		scshwfzeqfzo	$⊢ (x \in Word Vtx (G) \land x \neq \emptyset \land N = \|x\|) \to \{y \in Word Vtx (G) \| \exists n \in (0 \dots N) y = x cyclShift n\} = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\}$
35	33 34	syl	$⊢ (N \in ℙ \land x \in W) \to \{y \in Word Vtx (G) \| \exists n \in (0 \dots N) y = x cyclShift n\} = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\}$
36	35	eqeq2d	$⊢ (N \in ℙ \land x \in W) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 \dots N) y = x cyclShift n\} \leftrightarrow U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\})$
37		oveq2	$⊢ n = m \to x cyclShift n = x cyclShift m$
38	37	eqeq2d	$⊢ n = m \to (y = x cyclShift n \leftrightarrow y = x cyclShift m)$
39	38	cbvrexvw	$⊢ \exists n \in (0 ..^\|x\|) y = x cyclShift n \leftrightarrow \exists m \in (0 ..^\|x\|) y = x cyclShift m$
40		eqeq1	$⊢ y = u \to (y = x cyclShift m \leftrightarrow u = x cyclShift m)$
41		eqcom	$⊢ u = x cyclShift m \leftrightarrow x cyclShift m = u$
42	40 41	bitrdi	$⊢ y = u \to (y = x cyclShift m \leftrightarrow x cyclShift m = u)$
43	42	rexbidv	$⊢ y = u \to (\exists m \in (0 ..^\|x\|) y = x cyclShift m \leftrightarrow \exists m \in (0 ..^\|x\|) x cyclShift m = u)$
44	39 43	bitrid	$⊢ y = u \to (\exists n \in (0 ..^\|x\|) y = x cyclShift n \leftrightarrow \exists m \in (0 ..^\|x\|) x cyclShift m = u)$
45	44	cbvrabv	$⊢ \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} = \{u \in Word Vtx (G) \| \exists m \in (0 ..^\|x\|) x cyclShift m = u\}$
46	45	cshwshash	$⊢ (x \in Word Vtx (G) \land \|x\| \in ℙ) \to (\|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\| = \|x\| \lor \|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\| = 1)$
47	46	adantr	$⊢ ((x \in Word Vtx (G) \land \|x\| \in ℙ) \land U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}) \to (\|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\| = \|x\| \lor \|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\| = 1)$
48	47	orcomd	$⊢ ((x \in Word Vtx (G) \land \|x\| \in ℙ) \land U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}) \to (\|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\| = 1 \lor \|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\| = \|x\|)$
49		fveqeq2	$⊢ U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to (\|U\| = 1 \leftrightarrow \|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\| = 1)$
50		fveqeq2	$⊢ U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to (\|U\| = \|x\| \leftrightarrow \|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\| = \|x\|)$
51	49 50	orbi12d	$⊢ U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to ((\|U\| = 1 \lor \|U\| = \|x\|) \leftrightarrow (\|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\| = 1 \lor \|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\| = \|x\|))$
52	51	adantl	$⊢ ((x \in Word Vtx (G) \land \|x\| \in ℙ) \land U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}) \to ((\|U\| = 1 \lor \|U\| = \|x\|) \leftrightarrow (\|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\| = 1 \lor \|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\| = \|x\|))$
53	48 52	mpbird	$⊢ ((x \in Word Vtx (G) \land \|x\| \in ℙ) \land U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}) \to (\|U\| = 1 \lor \|U\| = \|x\|)$
54	53	ex	$⊢ (x \in Word Vtx (G) \land \|x\| \in ℙ) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = \|x\|))$
55	54	ex	$⊢ x \in Word Vtx (G) \to (\|x\| \in ℙ \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = \|x\|)))$
56	55	adantr	$⊢ (x \in Word Vtx (G) \land \|x\| = N) \to (\|x\| \in ℙ \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = \|x\|)))$
57		eleq1	$⊢ N = \|x\| \to (N \in ℙ \leftrightarrow \|x\| \in ℙ)$
58		oveq2	$⊢ N = \|x\| \to (0 ..^N) = (0 ..^\|x\|)$
59	58	rexeqdv	$⊢ N = \|x\| \to (\exists n \in (0 ..^N) y = x cyclShift n \leftrightarrow \exists n \in (0 ..^\|x\|) y = x cyclShift n)$
60	59	rabbidv	$⊢ N = \|x\| \to \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}$
61	60	eqeq2d	$⊢ N = \|x\| \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \leftrightarrow U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\})$
62		eqeq2	$⊢ N = \|x\| \to (\|U\| = N \leftrightarrow \|U\| = \|x\|)$
63	62	orbi2d	$⊢ N = \|x\| \to ((\|U\| = 1 \lor \|U\| = N) \leftrightarrow (\|U\| = 1 \lor \|U\| = \|x\|))$
64	61 63	imbi12d	$⊢ N = \|x\| \to ((U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = N)) \leftrightarrow (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = \|x\|)))$
65	57 64	imbi12d	$⊢ N = \|x\| \to ((N \in ℙ \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = N))) \leftrightarrow (\|x\| \in ℙ \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = \|x\|))))$
66	65	eqcoms	$⊢ \|x\| = N \to ((N \in ℙ \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = N))) \leftrightarrow (\|x\| \in ℙ \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = \|x\|))))$
67	66	adantl	$⊢ (x \in Word Vtx (G) \land \|x\| = N) \to ((N \in ℙ \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = N))) \leftrightarrow (\|x\| \in ℙ \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = \|x\|))))$
68	56 67	mpbird	$⊢ (x \in Word Vtx (G) \land \|x\| = N) \to (N \in ℙ \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = N)))$
69	29 68	syl	$⊢ x \in (N ClWWalksN G) \to (N \in ℙ \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = N)))$
70	69 1	eleq2s	$⊢ x \in W \to (N \in ℙ \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = N)))$
71	70	impcom	$⊢ (N \in ℙ \land x \in W) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = N))$
72	36 71	sylbid	$⊢ (N \in ℙ \land x \in W) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 \dots N) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = N))$
73	13 72	sylbid	$⊢ (N \in ℙ \land x \in W) \to (U = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = N))$
74	73	rexlimdva	$⊢ N \in ℙ \to (\exists x \in W U = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to (\|U\| = 1 \lor \|U\| = N))$
75	74	com12	$⊢ \exists x \in W U = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to (N \in ℙ \to (\|U\| = 1 \lor \|U\| = N))$
76	3 75	syl6bi	$⊢ U \in (W / \underset{˙}{\sim}) \to (U \in (W / \underset{˙}{\sim}) \to (N \in ℙ \to (\|U\| = 1 \lor \|U\| = N)))$
77	76	pm2.43i	$⊢ U \in (W / \underset{˙}{\sim}) \to (N \in ℙ \to (\|U\| = 1 \lor \|U\| = N))$
78	77	impcom	$⊢ (N \in ℙ \land U \in (W / \underset{˙}{\sim})) \to (\|U\| = 1 \lor \|U\| = N)$

Metamath Proof Explorer

Theorem hashecclwwlkn1

Proof