umgrhashecclwwlk

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 equals this length (in an undirected simple graph). (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	umgrhashecclwwlk	$⊢ (G \in UMGraph \land N \in ℙ) \to (U \in (W / \underset{˙}{\sim}) \to \|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	$⊢ ((G \in UMGraph \land 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	7	adantl	$⊢ (G \in UMGraph \land N \in ℙ) \to N \in ℕ_{0}$
9	1	eleq2i	$⊢ x \in W \leftrightarrow x \in (N ClWWalksN G)$
10	9	biimpi	$⊢ x \in W \to x \in (N ClWWalksN G)$
11		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\}$
12	8 10 11	syl2an	$⊢ ((G \in UMGraph \land 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\}$
13	5 12	eqtrd	$⊢ ((G \in UMGraph \land 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\}$
14	13	eqeq2d	$⊢ ((G \in UMGraph \land 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\})$
15	6	adantl	$⊢ (G \in UMGraph \land N \in ℙ) \to N \in ℕ$
16		simpll	$⊢ ((x \in Word Vtx (G) \land \|x\| = N) \land N \in ℕ) \to x \in Word Vtx (G)$
17		elnnne0	$⊢ N \in ℕ \leftrightarrow (N \in ℕ_{0} \land N \neq 0)$
18		eqeq1	$⊢ N = \|x\| \to (N = 0 \leftrightarrow \|x\| = 0)$
19	18	eqcoms	$⊢ \|x\| = N \to (N = 0 \leftrightarrow \|x\| = 0)$
20		hasheq0	$⊢ x \in Word Vtx (G) \to (\|x\| = 0 \leftrightarrow x = \emptyset)$
21	19 20	sylan9bbr	$⊢ (x \in Word Vtx (G) \land \|x\| = N) \to (N = 0 \leftrightarrow x = \emptyset)$
22	21	necon3bid	$⊢ (x \in Word Vtx (G) \land \|x\| = N) \to (N \neq 0 \leftrightarrow x \neq \emptyset)$
23	22	biimpcd	$⊢ N \neq 0 \to ((x \in Word Vtx (G) \land \|x\| = N) \to x \neq \emptyset)$
24	17 23	simplbiim	$⊢ N \in ℕ \to ((x \in Word Vtx (G) \land \|x\| = N) \to x \neq \emptyset)$
25	24	impcom	$⊢ ((x \in Word Vtx (G) \land \|x\| = N) \land N \in ℕ) \to x \neq \emptyset$
26		simplr	$⊢ ((x \in Word Vtx (G) \land \|x\| = N) \land N \in ℕ) \to \|x\| = N$
27	26	eqcomd	$⊢ ((x \in Word Vtx (G) \land \|x\| = N) \land N \in ℕ) \to N = \|x\|$
28	16 25 27	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\|)$
29	28	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\|))$
30		eqid	$⊢ Vtx (G) = Vtx (G)$
31	30	clwwlknbp	$⊢ x \in (N ClWWalksN G) \to (x \in Word Vtx (G) \land \|x\| = N)$
32	29 31	syl11	$⊢ N \in ℕ \to (x \in (N ClWWalksN G) \to (x \in Word Vtx (G) \land x \neq \emptyset \land N = \|x\|))$
33	9 32	syl5bi	$⊢ N \in ℕ \to (x \in W \to (x \in Word Vtx (G) \land x \neq \emptyset \land N = \|x\|))$
34	15 33	syl	$⊢ (G \in UMGraph \land N \in ℙ) \to (x \in W \to (x \in Word Vtx (G) \land x \neq \emptyset \land N = \|x\|))$
35	34	imp	$⊢ ((G \in UMGraph \land N \in ℙ) \land x \in W) \to (x \in Word Vtx (G) \land x \neq \emptyset \land N = \|x\|)$
36		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\}$
37	35 36	syl	$⊢ ((G \in UMGraph \land 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\}$
38	37	eqeq2d	$⊢ ((G \in UMGraph \land 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\})$
39		fveq2	$⊢ U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to \|U\| = \|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\|$
40		simprl	$⊢ ((x \in Word Vtx (G) \land x \in (\|x\| ClWWalksN G)) \land (G \in UMGraph \land \|x\| \in ℙ)) \to G \in UMGraph$
41		prmuz2	$⊢ \|x\| \in ℙ \to \|x\| \in ℤ_{\geq 2}$
42	41	adantl	$⊢ (G \in UMGraph \land \|x\| \in ℙ) \to \|x\| \in ℤ_{\geq 2}$
43	42	adantl	$⊢ ((x \in Word Vtx (G) \land x \in (\|x\| ClWWalksN G)) \land (G \in UMGraph \land \|x\| \in ℙ)) \to \|x\| \in ℤ_{\geq 2}$
44		simplr	$⊢ ((x \in Word Vtx (G) \land x \in (\|x\| ClWWalksN G)) \land (G \in UMGraph \land \|x\| \in ℙ)) \to x \in (\|x\| ClWWalksN G)$
45		umgr2cwwkdifex	$⊢ (G \in UMGraph \land \|x\| \in ℤ_{\geq 2} \land x \in (\|x\| ClWWalksN G)) \to \exists i \in (0 ..^\|x\|) x (i) \neq x (0)$
46	40 43 44 45	syl3anc	$⊢ ((x \in Word Vtx (G) \land x \in (\|x\| ClWWalksN G)) \land (G \in UMGraph \land \|x\| \in ℙ)) \to \exists i \in (0 ..^\|x\|) x (i) \neq x (0)$
47		oveq2	$⊢ n = m \to x cyclShift n = x cyclShift m$
48	47	eqeq2d	$⊢ n = m \to (y = x cyclShift n \leftrightarrow y = x cyclShift m)$
49	48	cbvrexvw	$⊢ \exists n \in (0 ..^\|x\|) y = x cyclShift n \leftrightarrow \exists m \in (0 ..^\|x\|) y = x cyclShift m$
50		eqeq1	$⊢ y = u \to (y = x cyclShift m \leftrightarrow u = x cyclShift m)$
51		eqcom	$⊢ u = x cyclShift m \leftrightarrow x cyclShift m = u$
52	50 51	bitrdi	$⊢ y = u \to (y = x cyclShift m \leftrightarrow x cyclShift m = u)$
53	52	rexbidv	$⊢ y = u \to (\exists m \in (0 ..^\|x\|) y = x cyclShift m \leftrightarrow \exists m \in (0 ..^\|x\|) x cyclShift m = u)$
54	49 53	syl5bb	$⊢ y = u \to (\exists n \in (0 ..^\|x\|) y = x cyclShift n \leftrightarrow \exists m \in (0 ..^\|x\|) x cyclShift m = u)$
55	54	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\}$
56	55	cshwshashnsame	$⊢ (x \in Word Vtx (G) \land \|x\| \in ℙ) \to (\exists i \in (0 ..^\|x\|) x (i) \neq x (0) \to \|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\| = \|x\|)$
57	56	ad2ant2rl	$⊢ ((x \in Word Vtx (G) \land x \in (\|x\| ClWWalksN G)) \land (G \in UMGraph \land \|x\| \in ℙ)) \to (\exists i \in (0 ..^\|x\|) x (i) \neq x (0) \to \|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\| = \|x\|)$
58	46 57	mpd	$⊢ ((x \in Word Vtx (G) \land x \in (\|x\| ClWWalksN G)) \land (G \in UMGraph \land \|x\| \in ℙ)) \to \|\{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}\| = \|x\|$
59	39 58	sylan9eqr	$⊢ (((x \in Word Vtx (G) \land x \in (\|x\| ClWWalksN G)) \land (G \in UMGraph \land \|x\| \in ℙ)) \land U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\}) \to \|U\| = \|x\|$
60	59	exp41	$⊢ x \in Word Vtx (G) \to (x \in (\|x\| ClWWalksN G) \to ((G \in UMGraph \land \|x\| \in ℙ) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to \|U\| = \|x\|)))$
61	60	adantr	$⊢ (x \in Word Vtx (G) \land \|x\| = N) \to (x \in (\|x\| ClWWalksN G) \to ((G \in UMGraph \land \|x\| \in ℙ) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to \|U\| = \|x\|)))$
62		oveq1	$⊢ N = \|x\| \to N ClWWalksN G = \|x\| ClWWalksN G$
63	62	eleq2d	$⊢ N = \|x\| \to (x \in (N ClWWalksN G) \leftrightarrow x \in (\|x\| ClWWalksN G))$
64		eleq1	$⊢ N = \|x\| \to (N \in ℙ \leftrightarrow \|x\| \in ℙ)$
65	64	anbi2d	$⊢ N = \|x\| \to ((G \in UMGraph \land N \in ℙ) \leftrightarrow (G \in UMGraph \land \|x\| \in ℙ))$
66		oveq2	$⊢ N = \|x\| \to (0 ..^N) = (0 ..^\|x\|)$
67	66	rexeqdv	$⊢ N = \|x\| \to (\exists n \in (0 ..^N) y = x cyclShift n \leftrightarrow \exists n \in (0 ..^\|x\|) y = x cyclShift n)$
68	67	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\}$
69	68	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\})$
70		eqeq2	$⊢ N = \|x\| \to (\|U\| = N \leftrightarrow \|U\| = \|x\|)$
71	69 70	imbi12d	$⊢ N = \|x\| \to ((U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to \|U\| = N) \leftrightarrow (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to \|U\| = \|x\|))$
72	65 71	imbi12d	$⊢ N = \|x\| \to (((G \in UMGraph \land N \in ℙ) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to \|U\| = N)) \leftrightarrow ((G \in UMGraph \land \|x\| \in ℙ) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to \|U\| = \|x\|)))$
73	63 72	imbi12d	$⊢ N = \|x\| \to ((x \in (N ClWWalksN G) \to ((G \in UMGraph \land N \in ℙ) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to \|U\| = N))) \leftrightarrow (x \in (\|x\| ClWWalksN G) \to ((G \in UMGraph \land \|x\| \in ℙ) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to \|U\| = \|x\|))))$
74	73	eqcoms	$⊢ \|x\| = N \to ((x \in (N ClWWalksN G) \to ((G \in UMGraph \land N \in ℙ) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to \|U\| = N))) \leftrightarrow (x \in (\|x\| ClWWalksN G) \to ((G \in UMGraph \land \|x\| \in ℙ) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to \|U\| = \|x\|))))$
75	74	adantl	$⊢ (x \in Word Vtx (G) \land \|x\| = N) \to ((x \in (N ClWWalksN G) \to ((G \in UMGraph \land N \in ℙ) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to \|U\| = N))) \leftrightarrow (x \in (\|x\| ClWWalksN G) \to ((G \in UMGraph \land \|x\| \in ℙ) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^\|x\|) y = x cyclShift n\} \to \|U\| = \|x\|))))$
76	61 75	mpbird	$⊢ (x \in Word Vtx (G) \land \|x\| = N) \to (x \in (N ClWWalksN G) \to ((G \in UMGraph \land N \in ℙ) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to \|U\| = N)))$
77	31 76	mpcom	$⊢ x \in (N ClWWalksN G) \to ((G \in UMGraph \land N \in ℙ) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to \|U\| = N))$
78	77 1	eleq2s	$⊢ x \in W \to ((G \in UMGraph \land N \in ℙ) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to \|U\| = N))$
79	78	impcom	$⊢ ((G \in UMGraph \land N \in ℙ) \land x \in W) \to (U = \{y \in Word Vtx (G) \| \exists n \in (0 ..^N) y = x cyclShift n\} \to \|U\| = N)$
80	38 79	sylbid	$⊢ ((G \in UMGraph \land 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\| = N)$
81	14 80	sylbid	$⊢ ((G \in UMGraph \land N \in ℙ) \land x \in W) \to (U = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to \|U\| = N)$
82	81	rexlimdva	$⊢ (G \in UMGraph \land N \in ℙ) \to (\exists x \in W U = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to \|U\| = N)$
83	82	com12	$⊢ \exists x \in W U = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to ((G \in UMGraph \land N \in ℙ) \to \|U\| = N)$
84	3 83	syl6bi	$⊢ U \in (W / \underset{˙}{\sim}) \to (U \in (W / \underset{˙}{\sim}) \to ((G \in UMGraph \land N \in ℙ) \to \|U\| = N))$
85	84	pm2.43i	$⊢ U \in (W / \underset{˙}{\sim}) \to ((G \in UMGraph \land N \in ℙ) \to \|U\| = N)$
86	85	com12	$⊢ (G \in UMGraph \land N \in ℙ) \to (U \in (W / \underset{˙}{\sim}) \to \|U\| = N)$

Metamath Proof Explorer

Theorem umgrhashecclwwlk

Proof