clwwlknclwwlkdifnum

Description: In a K-regular graph, the size of the set A 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 B of closed walks of length N anchored at this vertex X . (Contributed by Alexander van der Vekens, 30-Sep-2018) (Revised by AV, 7-May-2021) (Revised by AV, 8-Mar-2022) (Proof shortened by AV, 16-Mar-2022)

	Ref	Expression
Hypotheses	clwwlknclwwlkdif.a	$⊢ A = \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\}$
	clwwlknclwwlkdif.b	$⊢ B = X (N WWalksNOn G) X$
	clwwlknclwwlkdifnum.v	$⊢ V = Vtx (G)$
Assertion	clwwlknclwwlkdifnum	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ_{0})) \to \|A\| = K^{N} - \|B\|$

Proof

Step	Hyp	Ref	Expression
1		clwwlknclwwlkdif.a	$⊢ A = \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\}$
2		clwwlknclwwlkdif.b	$⊢ B = X (N WWalksNOn G) X$
3		clwwlknclwwlkdifnum.v	$⊢ V = Vtx (G)$
4		eqid	$⊢ \{w \in (N WWalksN G) \| w (0) = X\} = \{w \in (N WWalksN G) \| w (0) = X\}$
5	1 2 4	clwwlknclwwlkdif	$⊢ A = \{w \in (N WWalksN G) \| w (0) = X\} ∖ B$
6	5	fveq2i	$⊢ \|A\| = \|\{w \in (N WWalksN G) \| w (0) = X\} ∖ B\|$
7	6	a1i	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ_{0})) \to \|A\| = \|\{w \in (N WWalksN G) \| w (0) = X\} ∖ B\|$
8	3	eleq1i	$⊢ V \in Fin \leftrightarrow Vtx (G) \in Fin$
9	8	biimpi	$⊢ V \in Fin \to Vtx (G) \in Fin$
10	9	adantl	$⊢ (G RegUSGraph K \land V \in Fin) \to Vtx (G) \in Fin$
11	10	adantr	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ_{0})) \to Vtx (G) \in Fin$
12		wwlksnfi	$⊢ Vtx (G) \in Fin \to N WWalksN G \in Fin$
13		rabfi	$⊢ N WWalksN G \in Fin \to \{w \in (N WWalksN G) \| w (0) = X\} \in Fin$
14	11 12 13	3syl	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ_{0})) \to \{w \in (N WWalksN G) \| w (0) = X\} \in Fin$
15	3	iswwlksnon	$⊢ X (N WWalksNOn G) X = \{w \in (N WWalksN G) \| (w (0) = X \land w (N) = X)\}$
16		ancom	$⊢ (w (0) = X \land w (N) = X) \leftrightarrow (w (N) = X \land w (0) = X)$
17	16	rabbii	$⊢ \{w \in (N WWalksN G) \| (w (0) = X \land w (N) = X)\} = \{w \in (N WWalksN G) \| (w (N) = X \land w (0) = X)\}$
18	15 17	eqtri	$⊢ X (N WWalksNOn G) X = \{w \in (N WWalksN G) \| (w (N) = X \land w (0) = X)\}$
19	18	a1i	$⊢ (X \in V \land N \in ℕ_{0}) \to X (N WWalksNOn G) X = \{w \in (N WWalksN G) \| (w (N) = X \land w (0) = X)\}$
20	2 19	eqtrid	$⊢ (X \in V \land N \in ℕ_{0}) \to B = \{w \in (N WWalksN G) \| (w (N) = X \land w (0) = X)\}$
21		simpr	$⊢ (w (N) = X \land w (0) = X) \to w (0) = X$
22	21	a1i	$⊢ w \in (N WWalksN G) \to ((w (N) = X \land w (0) = X) \to w (0) = X)$
23	22	ss2rabi	$⊢ \{w \in (N WWalksN G) \| (w (N) = X \land w (0) = X)\} \subseteq \{w \in (N WWalksN G) \| w (0) = X\}$
24	20 23	eqsstrdi	$⊢ (X \in V \land N \in ℕ_{0}) \to B \subseteq \{w \in (N WWalksN G) \| w (0) = X\}$
25	24	adantl	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ_{0})) \to B \subseteq \{w \in (N WWalksN G) \| w (0) = X\}$
26		hashssdif	$⊢ (\{w \in (N WWalksN G) \| w (0) = X\} \in Fin \land B \subseteq \{w \in (N WWalksN G) \| w (0) = X\}) \to \|\{w \in (N WWalksN G) \| w (0) = X\} ∖ B\| = \|\{w \in (N WWalksN G) \| w (0) = X\}\| - \|B\|$
27	14 25 26	syl2anc	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ_{0})) \to \|\{w \in (N WWalksN G) \| w (0) = X\} ∖ B\| = \|\{w \in (N WWalksN G) \| w (0) = X\}\| - \|B\|$
28		simpl	$⊢ (G RegUSGraph K \land V \in Fin) \to G RegUSGraph K$
29	28	adantr	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ_{0})) \to G RegUSGraph K$
30		simpr	$⊢ (G RegUSGraph K \land V \in Fin) \to V \in Fin$
31	30	adantr	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ_{0})) \to V \in Fin$
32		simpl	$⊢ (X \in V \land N \in ℕ_{0}) \to X \in V$
33	32	adantl	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ_{0})) \to X \in V$
34		simpr	$⊢ (X \in V \land N \in ℕ_{0}) \to N \in ℕ_{0}$
35	34	adantl	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ_{0})) \to N \in ℕ_{0}$
36	3	rusgrnumwwlkg	$⊢ (G RegUSGraph K \land (V \in Fin \land X \in V \land N \in ℕ_{0})) \to \|\{w \in (N WWalksN G) \| w (0) = X\}\| = K^{N}$
37	29 31 33 35 36	syl13anc	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ_{0})) \to \|\{w \in (N WWalksN G) \| w (0) = X\}\| = K^{N}$
38	37	oveq1d	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ_{0})) \to \|\{w \in (N WWalksN G) \| w (0) = X\}\| - \|B\| = K^{N} - \|B\|$
39	7 27 38	3eqtrd	$⊢ ((G RegUSGraph K \land V \in Fin) \land (X \in V \land N \in ℕ_{0})) \to \|A\| = K^{N} - \|B\|$

Metamath Proof Explorer

Theorem clwwlknclwwlkdifnum

Proof