numclwwlkqhash

Description: In a K-regular graph, the size of the set of walks of length N starting with a fixed vertex X and ending not at this vertex is the difference between K to the power of N and the size of the set of closed walks of length N on vertex X . (Contributed by Alexander van der Vekens, 30-Sep-2018) (Revised by AV, 30-May-2021) (Revised by AV, 5-Mar-2022) (Proof shortened by AV, 7-Jul-2022)

	Ref	Expression
Hypotheses	numclwwlk.v	$⊢ V = Vtx (G)$
	numclwwlk.q	$⊢ Q = (v \in V, n \in ℕ ⟼ \{w \in (n WWalksN G) \| (w (0) = v \land lastS (w) \neq v)\})$
Assertion	numclwwlkqhash	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ)) \to \|X Q N\| = K^{N} - \|X ClWWalksNOn (G) N\|$

Proof

Step	Hyp	Ref	Expression
1		numclwwlk.v	$⊢ V = Vtx (G)$
2		numclwwlk.q	$⊢ Q = (v \in V, n \in ℕ ⟼ \{w \in (n WWalksN G) \| (w (0) = v \land lastS (w) \neq v)\})$
3	1 2	numclwwlkovq	$⊢ (X \in V \land N \in ℕ) \to X Q N = \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\}$
4	3	adantl	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ)) \to X Q N = \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\}$
5	4	fveq2d	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ)) \to \|X Q N\| = \|\{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\}\|$
6		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
7		eqid	$⊢ \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\} = \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\}$
8		eqid	$⊢ X (N WWalksNOn G) X = X (N WWalksNOn G) X$
9	7 8 1	clwwlknclwwlkdifnum	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ_{0})) \to \|\{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\}\| = K^{N} - \|X (N WWalksNOn G) X\|$
10	6 9	sylanr2	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ)) \to \|\{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\}\| = K^{N} - \|X (N WWalksNOn G) X\|$
11	1	iswwlksnon	$⊢ X (N WWalksNOn G) X = \{w \in (N WWalksN G) \| (w (0) = X \land w (N) = X)\}$
12		wwlknlsw	$⊢ w \in (N WWalksN G) \to w (N) = lastS (w)$
13		eqcom	$⊢ w (0) = X \leftrightarrow X = w (0)$
14	13	biimpi	$⊢ w (0) = X \to X = w (0)$
15	12 14	eqeqan12d	$⊢ (w \in (N WWalksN G) \land w (0) = X) \to (w (N) = X \leftrightarrow lastS (w) = w (0))$
16	15	pm5.32da	$⊢ w \in (N WWalksN G) \to ((w (0) = X \land w (N) = X) \leftrightarrow (w (0) = X \land lastS (w) = w (0)))$
17	16	biancomd	$⊢ w \in (N WWalksN G) \to ((w (0) = X \land w (N) = X) \leftrightarrow (lastS (w) = w (0) \land w (0) = X))$
18	17	rabbiia	$⊢ \{w \in (N WWalksN G) \| (w (0) = X \land w (N) = X)\} = \{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\}$
19	11 18	eqtri	$⊢ X (N WWalksNOn G) X = \{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\}$
20	19	fveq2i	$⊢ \|X (N WWalksNOn G) X\| = \|\{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\}\|$
21	20	a1i	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ)) \to \|X (N WWalksNOn G) X\| = \|\{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\}\|$
22	21	oveq2d	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ)) \to K^{N} - \|X (N WWalksNOn G) X\| = K^{N} - \|\{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\}\|$
23	10 22	eqtrd	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ)) \to \|\{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\}\| = K^{N} - \|\{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\}\|$
24		ovex	$⊢ N WWalksN G \in V$
25	24	rabex	$⊢ \{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\} \in V$
26		clwwlkvbij	$⊢ (X \in V \land N \in ℕ) \to \exists f f : \{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N$
27	26	adantl	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ)) \to \exists f f : \{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N$
28		hasheqf1oi	$⊢ \{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\} \in V \to (\exists f f : \{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\} \underset{1-1 onto}{⟶} X ClWWalksNOn (G) N \to \|\{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\}\| = \|X ClWWalksNOn (G) N\|)$
29	25 27 28	mpsyl	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ)) \to \|\{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\}\| = \|X ClWWalksNOn (G) N\|$
30	29	oveq2d	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ)) \to K^{N} - \|\{w \in (N WWalksN G) \| (lastS (w) = w (0) \land w (0) = X)\}\| = K^{N} - \|X ClWWalksNOn (G) N\|$
31	5 23 30	3eqtrd	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ)) \to \|X Q N\| = K^{N} - \|X ClWWalksNOn (G) N\|$

Metamath Proof Explorer

Theorem numclwwlkqhash

Proof