numclwwlk3lem2

Description: Lemma 1 for numclwwlk3 : The number of closed vertices of a fixed length N on a fixed vertex V is the sum of the number of closed walks of length N at V with the last but one vertex being V and the set of closed walks of length N at V with the last but one vertex not being V . (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 1-Jun-2021) (Revised by AV, 1-May-2022)

	Ref	Expression
Hypotheses	numclwwlk3lem2.c	$⊢ C = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
	numclwwlk3lem2.h	$⊢ H = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) \neq v\})$
Assertion	numclwwlk3lem2	$⊢ ((G \in FinUSGraph \land X \in V) \land N \in ℤ_{\geq 2}) \to \|X ClWWalksNOn (G) N\| = \|X H N\| + \|X C N\|$

Proof

Step	Hyp	Ref	Expression
1		numclwwlk3lem2.c	$⊢ C = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
2		numclwwlk3lem2.h	$⊢ H = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) \neq v\})$
3	1 2	numclwwlk3lem2lem	$⊢ (X \in V \land N \in ℤ_{\geq 2}) \to X ClWWalksNOn (G) N = (X H N) \cup (X C N)$
4	3	adantll	$⊢ ((G \in FinUSGraph \land X \in V) \land N \in ℤ_{\geq 2}) \to X ClWWalksNOn (G) N = (X H N) \cup (X C N)$
5	4	fveq2d	$⊢ ((G \in FinUSGraph \land X \in V) \land N \in ℤ_{\geq 2}) \to \|X ClWWalksNOn (G) N\| = \|(X H N) \cup (X C N)\|$
6	2	numclwwlkovh0	$⊢ (X \in V \land N \in ℤ_{\geq 2}) \to X H N = \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) \neq X\}$
7	6	adantll	$⊢ ((G \in FinUSGraph \land X \in V) \land N \in ℤ_{\geq 2}) \to X H N = \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) \neq X\}$
8		eqid	$⊢ Vtx (G) = Vtx (G)$
9	8	fusgrvtxfi	$⊢ G \in FinUSGraph \to Vtx (G) \in Fin$
10	9	ad2antrr	$⊢ ((G \in FinUSGraph \land X \in V) \land N \in ℤ_{\geq 2}) \to Vtx (G) \in Fin$
11	8	clwwlknonfin	$⊢ Vtx (G) \in Fin \to X ClWWalksNOn (G) N \in Fin$
12		rabfi	$⊢ X ClWWalksNOn (G) N \in Fin \to \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) \neq X\} \in Fin$
13	10 11 12	3syl	$⊢ ((G \in FinUSGraph \land X \in V) \land N \in ℤ_{\geq 2}) \to \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) \neq X\} \in Fin$
14	7 13	eqeltrd	$⊢ ((G \in FinUSGraph \land X \in V) \land N \in ℤ_{\geq 2}) \to X H N \in Fin$
15	1	2clwwlk	$⊢ (X \in V \land N \in ℤ_{\geq 2}) \to X C N = \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}$
16	15	adantll	$⊢ ((G \in FinUSGraph \land X \in V) \land N \in ℤ_{\geq 2}) \to X C N = \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}$
17		rabfi	$⊢ X ClWWalksNOn (G) N \in Fin \to \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\} \in Fin$
18	10 11 17	3syl	$⊢ ((G \in FinUSGraph \land X \in V) \land N \in ℤ_{\geq 2}) \to \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\} \in Fin$
19	16 18	eqeltrd	$⊢ ((G \in FinUSGraph \land X \in V) \land N \in ℤ_{\geq 2}) \to X C N \in Fin$
20	7 16	ineq12d	$⊢ ((G \in FinUSGraph \land X \in V) \land N \in ℤ_{\geq 2}) \to (X H N) \cap (X C N) = \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) \neq X\} \cap \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\}$
21		inrab	$⊢ \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) \neq X\} \cap \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\} = \{w \in (X ClWWalksNOn (G) N) \| (w (N - 2) \neq X \land w (N - 2) = X)\}$
22		exmid	$⊢ (w (N - 2) = X \lor \neg w (N - 2) = X)$
23		ianor	$⊢ \neg (w (N - 2) \neq X \land w (N - 2) = X) \leftrightarrow (\neg w (N - 2) \neq X \lor \neg w (N - 2) = X)$
24		nne	$⊢ \neg w (N - 2) \neq X \leftrightarrow w (N - 2) = X$
25	24	orbi1i	$⊢ (\neg w (N - 2) \neq X \lor \neg w (N - 2) = X) \leftrightarrow (w (N - 2) = X \lor \neg w (N - 2) = X)$
26	23 25	bitri	$⊢ \neg (w (N - 2) \neq X \land w (N - 2) = X) \leftrightarrow (w (N - 2) = X \lor \neg w (N - 2) = X)$
27	22 26	mpbir	$⊢ \neg (w (N - 2) \neq X \land w (N - 2) = X)$
28	27	rgenw	$⊢ \forall w \in (X ClWWalksNOn (G) N) \neg (w (N - 2) \neq X \land w (N - 2) = X)$
29		rabeq0	$⊢ \{w \in (X ClWWalksNOn (G) N) \| (w (N - 2) \neq X \land w (N - 2) = X)\} = \emptyset \leftrightarrow \forall w \in (X ClWWalksNOn (G) N) \neg (w (N - 2) \neq X \land w (N - 2) = X)$
30	28 29	mpbir	$⊢ \{w \in (X ClWWalksNOn (G) N) \| (w (N - 2) \neq X \land w (N - 2) = X)\} = \emptyset$
31	21 30	eqtri	$⊢ \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) \neq X\} \cap \{w \in (X ClWWalksNOn (G) N) \| w (N - 2) = X\} = \emptyset$
32	20 31	eqtrdi	$⊢ ((G \in FinUSGraph \land X \in V) \land N \in ℤ_{\geq 2}) \to (X H N) \cap (X C N) = \emptyset$
33		hashun	$⊢ (X H N \in Fin \land X C N \in Fin \land (X H N) \cap (X C N) = \emptyset) \to \|(X H N) \cup (X C N)\| = \|X H N\| + \|X C N\|$
34	14 19 32 33	syl3anc	$⊢ ((G \in FinUSGraph \land X \in V) \land N \in ℤ_{\geq 2}) \to \|(X H N) \cup (X C N)\| = \|X H N\| + \|X C N\|$
35	5 34	eqtrd	$⊢ ((G \in FinUSGraph \land X \in V) \land N \in ℤ_{\geq 2}) \to \|X ClWWalksNOn (G) N\| = \|X H N\| + \|X C N\|$

Metamath Proof Explorer

Theorem numclwwlk3lem2

Proof